Abstract
Model-checking is largely used in formal verification of hardware and software systems. The advantage of model checking is producing counterexamples when properties are not satisfied. Formal modeling specifies the system requirements and validates the model. These approaches are getting popular in industrial automation. Usually, it is used to check safety-critical systems, the failure of which may be catastrophic, e.g. The control systems of a nuclear power station may be checked using a model checker before being commissioned. Otherwise, it will cause huge damage. This paper presents an in-depth elaboration of some model checking techniques. It also presents a taxonomy and comprehensive review of the symbolic model checking in critical system design. Lastly, a case study is done to compare the detailed specifications of the model with different parameters.
I sincerely thank the Department of Computer Science and Engineering, University of Calcutta, India, for the assistance to pursue our research work.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Baier C, Katoen J-P (2008) Principles of model checking. The MIT Press, Cambridge. OCLC: ocn171152628
Huth M, Ryan M (2004) Logic in computer science: modelling and reasoning about systems, 2 edn. Cambridge University Press
Andersen HR (1997) An introduction to binary decision diagrams. Lecture notes, available online. IT University of Copenhagen, pp 5
Bryant RE (2018) Binary decision diagrams. In: Clarke EM, Henzinger TA, Veith H, Bloem R (eds) Handbook of model checking. Springer International Publishing, Cham, pp 191–217
Clarke EM, Lerda F (2007) Model checking: software and beyond. J. UCS 13(5):639–649
Fan J, Jiao J, Wu W, Zhao T (2015) A model-checking oriented modeling method for safety critical system. In: 2015 first international conference on reliability systems engineering (ICRSE)
Kim Y, Kim M, Kim T-H (2013) Statistical model checking for safety critical hybrid systems: an empirical evaluation. In: Biere A, Nahir A, Vos T (eds) Hardware and software: verification and testing, Lecture notes in computer science. Springer, Berlin, Heidelberg, pp 162–177
Angeletti D, Giunchiglia E, Narizzano M, Puddu A, Sabina Salvatore (2010) Using bounded model checking for coverage analysis of safety-critical software in an industrial setting. J Autom Reasoning 45(4):397–414
Hsiung Pao-Ann, Chen Yean-Ru, Lin Yen-Hung (2007) Model checking safety-critical systems using safecharts. IEEE Trans Comput 56(5):692–705
Buzhinsky I, Pakonen A (2019) Model-checking detailed fault-tolerant nuclear power plant safety functions. IEEE Access 7:162139–162156
Cai H, Wu WH, Zhang CD, Ho TK, Zhang ZM (2014) Modelling safety monitors of safety-critical railway systems by formal methods. In: 6th IET conference on railway condition monitoring (RCM 2014)
Gario M, Cimatti A, Mattarei C, Tonetta S, Rozier KY (2016) Model checking at scale: automated air traffic control design space exploration. In: Chaudhuri S, Farzan A (eds) Computer aided verification, Lecture notes in computer science. Springer International Publishing, Cham, pp 3–22
Miller SP, Cofer DD, Sha L, Meseguer J, Al-Nayeem A (2009) Implementing logical synchrony in integrated modular avionics. In: 2009 IEEE/AIAA 28th digital avionics systems conference. IEEE, pp 1–A
Jee E, Lee I, Sokolsky O (2010) Assurance cases in model-driven development of the pacemaker software. In: Margaria T, Steffen B (eds) Leveraging applications of formal methods, verification, and validation, lecture notes in computer science. Springer, Berlin, Heidelberg, pp 343–356
von Essen C, Giannakopoulou D (2014) Analyzing the next generation airborne collision avoidance system. In: Ábrahám E, Havelund K (eds) Tools and algorithms for the construction and analysis of systems
Guha S, Nag A, Karmakar R (2021) Model formal verification of safety-critical systems: a case-study in airbag systems. In: The proceedings of 20th international conference on intelligent systems design and applications (intelligent systems design and applications (ISDA) 2020). Springer International Publishing
Karmakar R, Sarkar BB, Chaki N (2019) System modeling using event-B: an insight. SSRN Scholarly Paper ID 3511455, Social Science Research Network, Rochester, NY
Karmakar R, Sarkar BB, Chaki N (2021) Event-b based formal modeling of a controller: a case study. In: Proceedings of international conference on frontiers in computing and systems
Karmakar R, Sarkar BB (2021) A prototype modeling of smart irrigation system using event-B. SN Comput Sci 2(1):36
Souri A, Rahmani AM, Navimipour NJ, Rezaei R (2019) A symbolic model checking approach in formal verification of distributed systems. Hum Centric Comput Inf Sci 9(1):4
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Karmakar, R. (2022). Symbolic Model Checking: A Comprehensive Review for Critical System Design. In: Tiwari, S., Trivedi, M.C., Kolhe, M.L., Mishra, K., Singh, B.K. (eds) Advances in Data and Information Sciences. Lecture Notes in Networks and Systems, vol 318. Springer, Singapore. https://doi.org/10.1007/978-981-16-5689-7_62
Download citation
DOI: https://doi.org/10.1007/978-981-16-5689-7_62
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-16-5688-0
Online ISBN: 978-981-16-5689-7
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)