A symbolic model checking approach in formal verification of distributed systems
Tóm tắt
Model checking is an influential method to verify complex interactions, concurrent and distributed systems. Model checking constructs a behavioral model of the system using formal concepts such as operations, states, events and actions. The model checkers suffer some weaknesses such as state space explosion problem that has high memory consumption and time complexity. Also, automating temporal logic is the main challenge to define critical specification rules in the model checking. To improve the model checking weaknesses, this paper presents Graphical Symbolic Modeling Toolkit (GSMT) to design and verify the behavioral models of distributed systems. A behavioral modeling framework is presented to design the system behavior in the forms of Kripke structure (KS) and Labeled Transition System (LTS). The behavioral models are created and edited using a graphical user interface platform in four layers that include a design layer, a modeling layer, a logic layer and a symbolic code layer. The GSMT generates a graphical modeling diagram visually for creating behavioral models of the system. Also, the temporal logic formulas are constructed according to some functional properties automatically. The executable code is generated according to the symbolic model verifier that user can choose the original model or reduced model with respect to a recursive reduced model. Finally, the generated code is executed using the NuSMV model checker for evaluating the constructed temporal logic formulas. The code generation time for transforming the behavioral model is compared to other model checking platforms. The proposed GSMT platform has outperformed evaluation than other platforms.
Từ khóa
Tài liệu tham khảo
Mitsch S, Passmore GO, Platzer A (2014) Collaborative verification-driven engineering of hybrid systems. Math Comput Sci 8:71–97
Li Y, Tao F, Cheng Y, Zhang X, Nee AYC (2017) Complex networks in advanced manufacturing systems. J Manuf Syst 43:409–421
Vakili A, Navimipour NJ (2017) Comprehensive and systematic review of the service composition mechanisms in the cloud environments. J Netw Comput Appl 81:24–36
Keshanchi B, Souri A, Navimipour NJ (2017) An improved genetic algorithm for task scheduling in the cloud environments using the priority queues: formal verification, simulation, and statistical testing. J Syst Softw 124:1–21
Higashino WA, Capretz MAM, Bittencourt LF (2016) CEPSim: modelling and simulation of complex event processing systems in cloud environments. Future Gener Comput Syst 65:122–139
Suh Y-K, Lee KY (2018) A survey of simulation provenance systems: modeling, capturing, querying, visualization, and advanced utilization. Hum Centric Comput Inf Sci 8:27
Dill DL (1998) What’s between simulation and formal verification? (extended abstract). In: Presented at the proceedings of the 35th annual design automation conference, San Francisco, California, USA
Li K, Liu L, Zhai J, Kosgoftaar TM, Shao M, Liu W (2017) Reliability evaluation model of component-based software based on complex network theory. Qual Reliab Eng Int 33(3):543–550
Khan W, Ullah H, Ahmad A, Sultan K, Alzahrani AJ, Khan SD et al (2018) CrashSafe: a formal model for proving crash-safety of Android applications. Hum Centric Comput Inf Sci 8:21
Kim J, Won Y (2017) Patch integrity verification method using dual electronic signatures. J Inf Process Syst 13
Hu K, Lei L, Tsai W-T (2016) Multi-tenant verification-as-a-service (VaaS) in a cloud. Simul Model Pract Theory 60:122–143
Jafari Navimipour N (2015) A formal approach for the specification and verification of a Trustworthy Human Resource Discovery mechanism in the Expert Cloud. Expert Syst Appl 42:6112–6131
Jafari Navimipour N, Habibizad Navin A, Rahmani AM, Hosseinzadeh M (2015) Behavioral modeling and automated verification of a Cloud-based framework to share the knowledge and skills of human resources. Comput Ind 68:65–77
Souri A (2016) Formal specification and verification of a data replication approach in distributed systems. Int J Next Gener Comput 7(1):18–37
Souri A, Jafari Navimipour N (2014) Behavioral modeling and formal verification of a resource discovery approach in Grid computing. Expert Syst Appl 41:3831–3849
Souri A, Norouzi M, Safarkhanlou A, Sardroud SHEH (2016) A dynamic data replication with consistency approach in data grids: modeling and verification. Balt J Mod Comput 4:546
Shen VRL, Wang Y-Y, Yu L-Y (2016) A novel blood pressure verification system for home care. Comput Stand Interfaces 44:42–53
Rezaee A, Rahmani AM, Movaghar A, Teshnehlab M (2014) Formal process algebraic modeling, verification, and analysis of an abstract Fuzzy Inference Cloud Service. J Supercomput 67:345–383
Ruiz MC, Cazorla D, Pérez D, Conejero J (2016) Formal performance evaluation of the Map/Reduce framework within cloud computing. J Supercomput 72:3136–3155
Hermanns H, Herzog U, Katoen J-P (2002) Process algebra for performance evaluation. Theoret Comput Sci 274:43–87
Tini S, Larsen KG, Gebler D (2017) Compositional bisimulation metric reasoning with probabilistic process calculi. Log Methods Comput Sci 12(4):2627
Chen X, Wang L (2017) Exploring fog computing based adaptive vehicular data scheduling policies through a compositional formal method-PEPA. IEEE Commun Lett. 2017
Challenger M, Mernik M, Kardas G, Kosar T (2016) Declarative specifications for the development of multi-agent systems. Comput Stand Interfaces 43:91–115
Hao F, Sim D-S, Park D-S, Seo H-S (2017) Similarity evaluation between graphs: a formal concept analysis approach. JIPS 13:1158–1167
Sardar MU, Hasan O, Shafique M, Henkel J (2017) Theorem proving based formal verification of distributed dynamic thermal management schemes. J Parallel Distrib Comput 100:157–171
Srikanth A, Sahin B, Harris WR (2017) Complexity verification using guided theorem enumeration. In: Proceedings of the 44th ACM SIGPLAN symposium on principles of programming languages, pp 639–652
Xue T, Ying S, Wu Q, Jia X, Hu X, Zhai X et al (2017) Verifying integrity of exception handling in service-oriented software. Int J Grid Util Comput 8:7–21
Copet PB, Marchetto G, Sisto R, Costa L (2017) Formal verification of LTE-UMTS and LTE–LTE handover procedures. Comput Stand Interfaces 50:92–106
Edmund J, Clarke M, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge
Leitner-Fischer F, Leue S (2013) Causality checking for complex system models. In: Giacobazzi R, Berdine J, Mastroeni I (eds) Proceedings of verification, model checking, and abstract interpretation: 14th international conference, VMCAI 2013, Rome, Italy, January 20–22, 2013. Springer Berlin Heidelberg, Berlin, pp 248–267
Merelli E, Paoletti N, Tesei L (2017) Adaptability checking in complex systems. Sci Comput Program 115–116:23–46
Baier C, Katoen J-P (2008) Principles of model checking (representation and mind series). The MIT Press, Cambridge
Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98:142–170
Souri A, Norouzi M (2015) A new probable decision making approach for verification of probabilistic real-time systems. In: 2015 6th IEEE international conference on software engineering and service science (ICSESS), pp 44–47
Cimatti A, Clarke E, Giunchiglia F, Roveri M (2000) NuSMV: a new symbolic model checker. Int J Softw Tools Technol Transfer 2:410–425
Sun J, Liu Y, Dong JS (2008) Model checking CSP revisited: introducing a process analysis toolkit. In: International symposium on leveraging applications of formal methods, verification and validation, pp 307–322
Bengtsson J, Larsen K, Larsson F, Pettersson P, Yi W (1995) UPPAAL—a tool suite for automatic verification of real-time systems. In: International hybrid systems workshop, pp 232–243
Podivinsky J, Cekan O, Lojda J, Zachariasova M, Krcma M, Kotasek Z (2017) Functional verification based platform for evaluating fault tolerance properties. Microprocess Microsyst 52:145–159
Wang S, Huang K (2016) Improving the efficiency of functional verification based on test prioritization. Microprocess Microsyst 41:1–11
Balasubramaniyan S, Srinivasan S, Buonopane F, Subathra B, Vain J, Ramaswamy S (2016) Design and verification of Cyber-Physical Systems using TrueTime, evolutionary optimization and UPPAAL. Microprocess Microsyst 42:37–48
Kaufmann P, Kronegger M, Pfandler A, Seidl M, Widl M (2015) Intra- and interdiagram consistency checking of behavioral multiview models. Comput Lang Syst Struct 44(Part A):72–88
López-Fernández JJ, Guerra E, de Lara J (2016) Combining unit and specification-based testing for meta-model validation and verification. Inf Syst 62:104–135
Amálio N, Glodt C (2015) A tool for visual and formal modelling of software designs. Sci Comput Program 98(Part 1):52–79
Holzmann GJ, Joshi R, Groce A (2008) New challenges in model checking. In: Grumberg O, Veith H (eds) 25 years of model checking: history, achievements, perspectives, Springer Berlin Heidelberg, Berlin, pp 65–76
Bozzano M, Villafiorita A (2006) The FSAP/NuSMV-SA safety analysis platform. Int J Softw Tools Technol Transfer 9:5
Głuchowski P (2016) NuSMV model verification of an airport traffic control system with deontic rules. In: Zamojski W, Mazurkiewicz J, Sugier J, Walkowiak T, Kacprzykj (eds) Dependability engineering and complex systems: proceedings of the eleventh international conference on dependability and complex systems DepCoS-RELCOMEX. June 27–July 1, 2016, Brunów, Poland, Springer International Publishing, Cham, pp 195–206
Safarkhanlou A, Souri A, Norouzi M, Sardroud SEH (2015) Formalizing and verification of an antivirus protection service using model checking. Procedia Comput Sci 57:1324–1331
Ngo VC, Legay A (2018) Formal verification of probabilistic SystemC models with statistical model checking. J Softw Evol Process 30:e1890
Li W, Hayes JH, Antoniol G, Guéhéneuc Y-G, Adams B (2016) Error leakage and wasted time: sensitivity and effort analysis of a requirements consistency checking process. J Softw Evol Process 28:1061–1080
Mercorio F (2013) Model checking for universal planning in deterministic and non-deterministic domains. AI Commun 26:257–259
Li J, Qeriqi A, Steffen M, Yu IC. Automatic translation from FBD-PLC-programs to NuSMV for model checking safety-critical control systems. 2016
Sharma PK, Ryu JH, Park KY, Park JH, Park JH (2018) Li-Fi based on security cloud framework for future IT environment. Hum Centric Comput Inf Sci 8:23
Castelluccia D, Mongiello M, Ruta M, Totaro R (2006) WAVer: a model checking-based tool to verify web application design. Electron Notes Theor Comput Sci 157:61–76
Abdelsadiq A (2013) A toolkit for model checking of electronic contracts
Caltais G, Leitner-Fischer F, Leue S, Weiser J (2016) SysML to NuSMV model transformation via object-orientation
Deb N, Chaki N, Ghose A (2016) Extracting finite state models from i* models. J Syst Softw 121:265–280
Meenakshi B, Bhatnagar A, Roy S (2006) Tool for translating Simulink models into input language of a model checker
Vinárek J, Ŝimko V, Hnĕtynka P (2015) Verification of use-cases with FOAM tool in context of cloud providers. In: 2015 41st euromicro conference on software engineering and advanced applications, pp 151–158
Simko V, Hauzar D, Hnetynka P, Bures T, Plasil F (2015) Formal verification of annotated textual use-cases. Comput J 58:1495–1529
Szwed P (2015) Verification of ArchiMate behavioral elements by model checking. In: Saeed K, Homenda W (eds) Computer information systems and industrial management: 14th IFIP TC 8 international conference, CISIM 2015, Warsaw, Poland, September 24–26, 2015, proceedings, Springer International Publishing, Cham, pp 132–144
Jiang Y, Qiu Z (2012) S2N: model transformation from SPIN to NuSMV. In: Presented at the PROCEEDINGS of the 19th international conference on Model Checking Software, Oxford, UK
Szpyrka M, Biernacka A, Biernacki J (2014) Methods of translation of petri nets to NuSMV language. In: CS&P, pp 245–256
Browne MC, Clarke EM, Grümberg O (1987) Characterizing Kripke structures in temporal logic. In: presented at the The International Joint Conference on theory and practice of software development on TAPSOFT ‘87, Pisa, Italy
Reniers MA, Willemse TAC (2011) Folk theorems on the correspondence between state-based and event-based systems. In: Černá I, Gyimóthy T, Hromkovič J, Jefferey K, Králović R, Vukolić M, et al. (eds) SOFSEM 2011: theory and practice of computer science: 37th conference on current trends in theory and practice of computer science, Nový Smokovec, Slovakia, January 22–28, 2011. Proceedings, Springer Berlin Heidelberg, Berlin, pp 494–505
Ghobaei-Arani M, Rahmanian AA, Souri A, Rahmani AM (2018) A moth-flame optimization algorithm for web service composition in cloud computing: simulation and verification. Softw Pract Exp 48:1865–1892
Souri A, Nourozi M, Rahmani AM, Navimipour NJ (2018) A model checking approach for user relationship management in the social network. Kybernetes. https://doi.org/10.1108/K-02-2018-0092092
Bouneb M, Saidouni DE, Ilie JM (2015) A reduced maximality labeled transition system generation for recursive Petri nets. Formal Aspects Comput 27:951–973
Sibay GE, Braberman V, Uchitel S, Kramer J (2013) Synthesizing modal transition systems from triggered scenarios. IEEE Trans Softw Eng 39:975–1001
Souri A, Rahmani AM, Jafari Navimipour N (2018) Formal verification approaches in the web service composition: a comprehensive analysis of the current challenges for future research. Int J Commun Syst 31:1–27
Zhao Y, Rozier KY (2014) Formal specification and verification of a coordination protocol for an automated air traffic control system. Sci Comput Program 96(Part 3):337–353
Bollig B (2016) On the minimization of (complete) ordered binary decision diagrams. Theory Comput Syst 59:532–559
Sharma A (2012) A two step perspective for Kripke structure reduction. arXiv preprint arXiv:1210.0408
Gradara S, Santone A, Villani ML, Vaglini G (2004) Model checking multithreaded programs by means of reduced models. Electron Notes Theor Comput Sci 110:55–74
Flanagan C, Godefroid P (2005) Dynamic partial-order reduction for model checking software. In: Presented at the proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, Long Beach, California, USA