{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T15:54:39Z","timestamp":1781020479450,"version":"3.54.1"},"reference-count":79,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2019,1,28]],"date-time":"2019-01-28T00:00:00Z","timestamp":1548633600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,1,28]],"date-time":"2019-01-28T00:00:00Z","timestamp":1548633600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Hum. Cent. Comput. Inf. Sci."],"published-print":{"date-parts":[[2019,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1186\/s13673-019-0165-x","type":"journal-article","created":{"date-parts":[[2019,1,28]],"date-time":"2019-01-28T13:03:32Z","timestamp":1548680612000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":40,"title":["A symbolic model checking approach in formal verification of distributed systems"],"prefix":"10.1186","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8314-9051","authenticated-orcid":false,"given":"Alireza","family":"Souri","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amir Masoud","family":"Rahmani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nima Jafari","family":"Navimipour","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Reza","family":"Rezaei","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,1,28]]},"reference":[{"key":"165_CR1","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/s11786-014-0176-y","volume":"8","author":"S Mitsch","year":"2014","unstructured":"Mitsch S, Passmore GO, Platzer A (2014) Collaborative verification-driven engineering of hybrid systems. Math Comput Sci 8:71\u201397","journal-title":"Math Comput Sci"},{"key":"165_CR2","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1016\/j.jmsy.2016.12.001","volume":"43","author":"Y Li","year":"2017","unstructured":"Li Y, Tao F, Cheng Y, Zhang X, Nee AYC (2017) Complex networks in advanced manufacturing systems. J Manuf Syst 43:409\u2013421","journal-title":"J Manuf Syst"},{"key":"165_CR3","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.jnca.2017.01.005","volume":"81","author":"A Vakili","year":"2017","unstructured":"Vakili A, Navimipour NJ (2017) Comprehensive and systematic review of the service composition mechanisms in the cloud environments. J Netw Comput Appl 81:24\u201336","journal-title":"J Netw Comput Appl"},{"key":"165_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jss.2016.07.006","volume":"124","author":"B Keshanchi","year":"2017","unstructured":"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\u201321","journal-title":"J Syst Softw"},{"key":"165_CR5","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1016\/j.ic.2010.11.012","volume":"209","author":"C Gla\u00dfer","year":"2011","unstructured":"Gla\u00dfer C, Pavan A, Travers S (2011) The fault tolerance of NP-hard problems. Inf Comput 209:443\u2013455","journal-title":"Inf Comput"},{"key":"165_CR6","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1016\/j.future.2015.10.023","volume":"65","author":"WA Higashino","year":"2016","unstructured":"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\u2013139","journal-title":"Future Gener Comput Syst"},{"key":"165_CR7","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1186\/s13673-018-0150-9","volume":"8","author":"Y-K Suh","year":"2018","unstructured":"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","journal-title":"Hum Centric Comput Inf Sci"},{"key":"165_CR8","doi-asserted-by":"crossref","unstructured":"Dill DL (1998) What\u2019s between simulation and formal verification? (extended abstract). In: Presented at the proceedings of the 35th annual design automation conference, San Francisco, California, USA","DOI":"10.1145\/277044.277138"},{"issue":"3","key":"165_CR9","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1002\/qre.2033","volume":"33","author":"K Li","year":"2017","unstructured":"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\u2013550","journal-title":"Qual Reliab Eng Int"},{"key":"165_CR10","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1186\/s13673-018-0144-7","volume":"8","author":"W Khan","year":"2018","unstructured":"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","journal-title":"Hum Centric Comput Inf Sci"},{"key":"165_CR11","unstructured":"Kim J, Won Y (2017) Patch integrity verification method using dual electronic signatures. J Inf Process Syst 13"},{"key":"165_CR12","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1016\/j.simpat.2015.09.003","volume":"60","author":"K Hu","year":"2016","unstructured":"Hu K, Lei L, Tsai W-T (2016) Multi-tenant verification-as-a-service (VaaS) in a cloud. Simul Model Pract Theory 60:122\u2013143","journal-title":"Simul Model Pract Theory"},{"key":"165_CR13","doi-asserted-by":"publisher","first-page":"6112","DOI":"10.1016\/j.eswa.2015.03.035","volume":"42","author":"N Jafari Navimipour","year":"2015","unstructured":"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\u20136131","journal-title":"Expert Syst Appl"},{"key":"165_CR14","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/j.compind.2014.12.007","volume":"68","author":"N Jafari Navimipour","year":"2015","unstructured":"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\u201377","journal-title":"Comput Ind"},{"issue":"1","key":"165_CR15","first-page":"18","volume":"7","author":"A Souri","year":"2016","unstructured":"Souri A (2016) Formal specification and verification of a data replication approach in distributed systems. Int J Next Gener Comput 7(1):18\u201337","journal-title":"Int J Next Gener Comput"},{"key":"165_CR16","doi-asserted-by":"publisher","first-page":"3831","DOI":"10.1016\/j.eswa.2013.11.042","volume":"41","author":"A Souri","year":"2014","unstructured":"Souri A, Jafari Navimipour N (2014) Behavioral modeling and formal verification of a resource discovery approach in Grid computing. Expert Syst Appl 41:3831\u20133849","journal-title":"Expert Syst Appl"},{"key":"165_CR17","first-page":"546","volume":"4","author":"A Souri","year":"2016","unstructured":"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","journal-title":"Balt J Mod Comput"},{"key":"165_CR18","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.csi.2015.09.008","volume":"44","author":"VRL Shen","year":"2016","unstructured":"Shen VRL, Wang Y-Y, Yu L-Y (2016) A novel blood pressure verification system for home care. Comput Stand Interfaces 44:42\u201353","journal-title":"Comput Stand Interfaces"},{"key":"165_CR19","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/s11227-013-1005-9","volume":"67","author":"A Rezaee","year":"2014","unstructured":"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\u2013383","journal-title":"J Supercomput"},{"key":"165_CR20","doi-asserted-by":"publisher","first-page":"3136","DOI":"10.1007\/s11227-015-1553-2","volume":"72","author":"MC Ruiz","year":"2016","unstructured":"Ruiz MC, Cazorla D, P\u00e9rez D, Conejero J (2016) Formal performance evaluation of the Map\/Reduce framework within cloud computing. J Supercomput 72:3136\u20133155","journal-title":"J Supercomput"},{"key":"165_CR21","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0304-3975(00)00305-4","volume":"274","author":"H Hermanns","year":"2002","unstructured":"Hermanns H, Herzog U, Katoen J-P (2002) Process algebra for performance evaluation. Theoret Comput Sci 274:43\u201387","journal-title":"Theoret Comput Sci"},{"issue":"4","key":"165_CR22","first-page":"2627","volume":"12","author":"S Tini","year":"2017","unstructured":"Tini S, Larsen KG, Gebler D (2017) Compositional bisimulation metric reasoning with probabilistic process calculi. Log Methods Comput Sci 12(4):2627","journal-title":"Log Methods Comput Sci"},{"key":"165_CR23","doi-asserted-by":"crossref","unstructured":"Chen X, Wang L (2017) Exploring fog computing based adaptive vehicular data scheduling policies through a compositional formal method-PEPA. IEEE Commun Lett. 2017","DOI":"10.1109\/LCOMM.2016.2647595"},{"key":"165_CR24","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.csi.2015.08.012","volume":"43","author":"M Challenger","year":"2016","unstructured":"Challenger M, Mernik M, Kardas G, Kosar T (2016) Declarative specifications for the development of multi-agent systems. Comput Stand Interfaces 43:91\u2013115","journal-title":"Comput Stand Interfaces"},{"key":"165_CR25","first-page":"1158","volume":"13","author":"F Hao","year":"2017","unstructured":"Hao F, Sim D-S, Park D-S, Seo H-S (2017) Similarity evaluation between graphs: a formal concept analysis approach. JIPS 13:1158\u20131167","journal-title":"JIPS"},{"key":"165_CR26","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/j.jpdc.2016.06.011","volume":"100","author":"MU Sardar","year":"2017","unstructured":"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\u2013171","journal-title":"J Parallel Distrib Comput"},{"key":"165_CR27","doi-asserted-by":"crossref","unstructured":"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\u2013652","DOI":"10.1145\/3009837.3009864"},{"key":"165_CR28","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1504\/IJGUC.2017.082133","volume":"8","author":"T Xue","year":"2017","unstructured":"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\u201321","journal-title":"Int J Grid Util Comput"},{"key":"165_CR29","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1016\/j.csi.2016.08.009","volume":"50","author":"PB Copet","year":"2017","unstructured":"Copet PB, Marchetto G, Sisto R, Costa L (2017) Formal verification of LTE-UMTS and LTE\u2013LTE handover procedures. Comput Stand Interfaces 50:92\u2013106","journal-title":"Comput Stand Interfaces"},{"key":"165_CR30","volume-title":"Model checking","author":"J Edmund","year":"1999","unstructured":"Edmund J, Clarke M, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge"},{"key":"165_CR31","doi-asserted-by":"crossref","unstructured":"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\u201322, 2013. Springer Berlin Heidelberg, Berlin, pp 248\u2013267","DOI":"10.1007\/978-3-642-35873-9_16"},{"key":"165_CR32","first-page":"23","volume":"115\u2013116","author":"E Merelli","year":"2017","unstructured":"Merelli E, Paoletti N, Tesei L (2017) Adaptability checking in complex systems. Sci Comput Program 115\u2013116:23\u201346","journal-title":"Sci Comput Program"},{"key":"165_CR33","volume-title":"Principles of model checking (representation and mind series)","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking (representation and mind series). The MIT Press, Cambridge"},{"key":"165_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"KL McMillan","year":"1993","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer Academic Publishers, Norwell"},{"key":"165_CR35","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98:142\u2013170","journal-title":"Inf Comput"},{"key":"165_CR36","doi-asserted-by":"crossref","unstructured":"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\u201347","DOI":"10.1109\/ICSESS.2015.7339003"},{"key":"165_CR37","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A Cimatti","year":"2000","unstructured":"Cimatti A, Clarke E, Giunchiglia F, Roveri M (2000) NuSMV: a new symbolic model checker. Int J Softw Tools Technol Transfer 2:410\u2013425","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"165_CR38","doi-asserted-by":"crossref","unstructured":"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\u2013322","DOI":"10.1007\/978-3-540-88479-8_22"},{"key":"165_CR39","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23:279\u2013295","journal-title":"IEEE Trans Softw Eng"},{"key":"165_CR40","doi-asserted-by":"crossref","unstructured":"Bengtsson J, Larsen K, Larsson F, Pettersson P, Yi W (1995) UPPAAL\u2014a tool suite for automatic verification of real-time systems. In: International hybrid systems workshop, pp 232\u2013243","DOI":"10.1007\/BFb0020949"},{"key":"165_CR41","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/j.micpro.2017.06.004","volume":"52","author":"J Podivinsky","year":"2017","unstructured":"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\u2013159","journal-title":"Microprocess Microsyst"},{"key":"165_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.micpro.2015.12.001","volume":"41","author":"S Wang","year":"2016","unstructured":"Wang S, Huang K (2016) Improving the efficiency of functional verification based on test prioritization. Microprocess Microsyst 41:1\u201311","journal-title":"Microprocess Microsyst"},{"key":"165_CR43","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.micpro.2015.12.006","volume":"42","author":"S Balasubramaniyan","year":"2016","unstructured":"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\u201348","journal-title":"Microprocess Microsyst"},{"issue":"Part A","key":"165_CR44","first-page":"72","volume":"44","author":"P Kaufmann","year":"2015","unstructured":"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\u201388","journal-title":"Comput Lang Syst Struct"},{"key":"165_CR45","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1016\/j.is.2016.06.008","volume":"62","author":"JJ L\u00f3pez-Fern\u00e1ndez","year":"2016","unstructured":"L\u00f3pez-Fern\u00e1ndez JJ, Guerra E, de Lara J (2016) Combining unit and specification-based testing for meta-model validation and verification. Inf Syst 62:104\u2013135","journal-title":"Inf Syst"},{"issue":"Part 1","key":"165_CR46","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.scico.2014.05.002","volume":"98","author":"N Am\u00e1lio","year":"2015","unstructured":"Am\u00e1lio N, Glodt C (2015) A tool for visual and formal modelling of software designs. Sci Comput Program 98(Part 1):52\u201379","journal-title":"Sci Comput Program"},{"key":"165_CR47","doi-asserted-by":"crossref","unstructured":"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\u201376","DOI":"10.1007\/978-3-540-69850-0_4"},{"key":"165_CR48","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10009-006-0001-2","volume":"9","author":"M Bozzano","year":"2006","unstructured":"Bozzano M, Villafiorita A (2006) The FSAP\/NuSMV-SA safety analysis platform. Int J Softw Tools Technol Transfer 9:5","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"165_CR49","doi-asserted-by":"crossref","unstructured":"G\u0142uchowski 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\u2013July 1, 2016, Brun\u00f3w, Poland, Springer International Publishing, Cham, pp 195\u2013206","DOI":"10.1007\/978-3-319-39639-2_17"},{"key":"165_CR50","doi-asserted-by":"publisher","first-page":"1324","DOI":"10.1016\/j.procs.2015.07.443","volume":"57","author":"A Safarkhanlou","year":"2015","unstructured":"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\u20131331","journal-title":"Procedia Comput Sci"},{"key":"165_CR51","doi-asserted-by":"publisher","first-page":"e1890","DOI":"10.1002\/smr.1890","volume":"30","author":"VC Ngo","year":"2018","unstructured":"Ngo VC, Legay A (2018) Formal verification of probabilistic SystemC models with statistical model checking. J Softw Evol Process 30:e1890","journal-title":"J Softw Evol Process"},{"key":"165_CR52","doi-asserted-by":"publisher","first-page":"1061","DOI":"10.1002\/smr.1819","volume":"28","author":"W Li","year":"2016","unstructured":"Li W, Hayes JH, Antoniol G, Gu\u00e9h\u00e9neuc 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\u20131080","journal-title":"J Softw Evol Process"},{"key":"165_CR53","doi-asserted-by":"crossref","first-page":"257","DOI":"10.3233\/AIC-130556","volume":"26","author":"F Mercorio","year":"2013","unstructured":"Mercorio F (2013) Model checking for universal planning in deterministic and non-deterministic domains. AI Commun 26:257\u2013259","journal-title":"AI Commun"},{"key":"165_CR54","unstructured":"Li J, Qeriqi A, Steffen M, Yu IC. Automatic translation from FBD-PLC-programs to NuSMV for model checking safety-critical control systems. 2016"},{"key":"165_CR55","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1186\/s13673-018-0146-5","volume":"8","author":"PK Sharma","year":"2018","unstructured":"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","journal-title":"Hum Centric Comput Inf Sci"},{"key":"165_CR56","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.entcs.2006.01.023","volume":"157","author":"D Castelluccia","year":"2006","unstructured":"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\u201376","journal-title":"Electron Notes Theor Comput Sci"},{"key":"165_CR57","unstructured":"Abdelsadiq A (2013) A toolkit for model checking of electronic contracts"},{"key":"165_CR58","doi-asserted-by":"crossref","unstructured":"Caltais G, Leitner-Fischer F, Leue S, Weiser J (2016) SysML to NuSMV model transformation via object-orientation","DOI":"10.1007\/978-3-319-51738-4_3"},{"key":"165_CR59","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/j.jss.2016.03.038","volume":"121","author":"N Deb","year":"2016","unstructured":"Deb N, Chaki N, Ghose A (2016) Extracting finite state models from i* models. J Syst Softw 121:265\u2013280","journal-title":"J Syst Softw"},{"key":"165_CR60","doi-asserted-by":"crossref","unstructured":"Meenakshi B, Bhatnagar A, Roy S (2006) Tool for translating Simulink models into input language of a model checker","DOI":"10.1007\/11901433_33"},{"key":"165_CR61","doi-asserted-by":"crossref","unstructured":"Vin\u00e1rek J, \u015cimko V, Hn\u0115tynka 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\u2013158","DOI":"10.1109\/SEAA.2015.39"},{"key":"165_CR62","doi-asserted-by":"publisher","first-page":"1495","DOI":"10.1093\/comjnl\/bxu068","volume":"58","author":"V Simko","year":"2015","unstructured":"Simko V, Hauzar D, Hnetynka P, Bures T, Plasil F (2015) Formal verification of annotated textual use-cases. Comput J 58:1495\u20131529","journal-title":"Comput J"},{"key":"165_CR63","doi-asserted-by":"crossref","unstructured":"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\u201326, 2015, proceedings, Springer International Publishing, Cham, pp 132\u2013144","DOI":"10.1007\/978-3-319-24369-6_11"},{"key":"165_CR64","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/978-3-642-31759-0_20"},{"key":"165_CR65","unstructured":"Szpyrka M, Biernacka A, Biernacki J (2014) Methods of translation of petri nets to NuSMV language. In: CS&P, pp 245\u2013256"},{"key":"165_CR66","doi-asserted-by":"crossref","unstructured":"Browne MC, Clarke EM, Gr\u00fcmberg 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 \u201887, Pisa, Italy","DOI":"10.21236\/ADA188620"},{"key":"165_CR67","unstructured":"Reniers MA, Willemse TAC (2011) Folk theorems on the correspondence between state-based and event-based systems. In: \u010cern\u00e1 I, Gyim\u00f3thy T, Hromkovi\u010d J, Jefferey K, Kr\u00e1lovi\u0107 R, Vukoli\u0107 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\u00fd Smokovec, Slovakia, January 22\u201328, 2011. Proceedings, Springer Berlin Heidelberg, Berlin, pp 494\u2013505"},{"key":"165_CR68","doi-asserted-by":"crossref","first-page":"1865","DOI":"10.1002\/spe.2598","volume":"48","author":"M Ghobaei-Arani","year":"2018","unstructured":"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\u20131892","journal-title":"Softw Pract Exp"},{"key":"165_CR69","doi-asserted-by":"publisher","DOI":"10.1108\/K-02-2018-0092092","author":"A Souri","year":"2018","unstructured":"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","journal-title":"Kybernetes"},{"key":"165_CR70","doi-asserted-by":"publisher","first-page":"951","DOI":"10.1007\/s00165-015-0341-3","volume":"27","author":"M Bouneb","year":"2015","unstructured":"Bouneb M, Saidouni DE, Ilie JM (2015) A reduced maximality labeled transition system generation for recursive Petri nets. Formal Aspects Comput 27:951\u2013973","journal-title":"Formal Aspects Comput"},{"key":"165_CR71","doi-asserted-by":"publisher","first-page":"975","DOI":"10.1109\/TSE.2012.62","volume":"39","author":"GE Sibay","year":"2013","unstructured":"Sibay GE, Braberman V, Uchitel S, Kramer J (2013) Synthesizing modal transition systems from triggered scenarios. IEEE Trans Softw Eng 39:975\u20131001","journal-title":"IEEE Trans Softw Eng"},{"key":"165_CR72","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1002\/dac.3808","volume":"31","author":"A Souri","year":"2018","unstructured":"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\u201327","journal-title":"Int J Commun Syst"},{"key":"165_CR73","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.cosrev.2010.06.002","volume":"5","author":"KY Rozier","year":"2011","unstructured":"Rozier KY (2011) Linear temporal logic symbolic model checking. Comput Sci Rev 5:163\u2013203","journal-title":"Comput Sci Rev"},{"issue":"Part 3","key":"165_CR74","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/j.scico.2014.04.002","volume":"96","author":"Y Zhao","year":"2014","unstructured":"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\u2013353","journal-title":"Sci Comput Program"},{"key":"165_CR75","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/s00224-015-9657-x","volume":"59","author":"B Bollig","year":"2016","unstructured":"Bollig B (2016) On the minimization of (complete) ordered binary decision diagrams. Theory Comput Syst 59:532\u2013559","journal-title":"Theory Comput Syst"},{"key":"165_CR76","unstructured":"Sharma A (2012) A two step perspective for Kripke structure reduction. arXiv preprint arXiv:1210.0408"},{"key":"165_CR77","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.entcs.2004.06.010","volume":"110","author":"S Gradara","year":"2004","unstructured":"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\u201374","journal-title":"Electron Notes Theor Comput Sci"},{"key":"165_CR78","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1145\/1040305.1040315"},{"key":"165_CR79","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1093\/comjnl\/bxs156","volume":"57","author":"MA Reniers","year":"2014","unstructured":"Reniers MA, Schoren R, Willemse TAC (2014) Results on embeddings between state-based and event-based systems. Comput. J 57:73\u201392","journal-title":"Comput. J"}],"container-title":["Human-centric Computing and Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s13673-019-0165-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1186\/s13673-019-0165-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s13673-019-0165-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,14]],"date-time":"2024-07-14T11:06:27Z","timestamp":1720955187000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1186\/s13673-019-0165-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,28]]},"references-count":79,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["165"],"URL":"https:\/\/doi.org\/10.1186\/s13673-019-0165-x","relation":{},"ISSN":["2192-1962"],"issn-type":[{"value":"2192-1962","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,28]]},"assertion":[{"value":"27 September 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 January 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 January 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"4"}}