Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is finding ways to make software more reliable. This review provides an overview of techniques developed over time in the field of software model checking to solve the problem of detecting errors in program code. In addition, the challenges posed by this technology are discussed and ways to mitigate them in future research and applications are proposed. A comprehensive examination of the various model verification methods used to detect program code errors is intended to lay the foundation for future research in this area.
References
[1]
Henzinger, T.A., Jhala, R., Majumdar, R. and Sutre G. (2002) Lazy Abstraction. Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, 16-18 January 2002, 58-70. https://doi.org/10.1145/503272.503279
[2]
Louden, K.C. (1993) Programming Languages Principles and Practice. URL.
[3]
Baier, C. and Katoen, J. (2008) Principle of Model Checking. MIT Press, Cambridge.
[4]
Aggarwal, K.K. and Yogesh, S. (2001) Software Engineering. 3rd Edition, New Age International Ltd, New Delhi.
[5]
Van-Hung, D. (2005) Model-Checking and the SPIN Model Checker. International Institute for Software Technology, Macau.
[6]
Mount, S. (2013) A Language-Independent Static Checking System for Coding Conventions. Ph.D. Thesis, University of Wolverhampton, Wolverhampton. https://www.semanticscholar.org/paper/A-language-independent-static-checking-system-for-Mount/a13e0e45b0c16ac8dda081666b9d2037c44e6b10
[7]
Li, Y., Jiang, X., Zhang, Y., Xie, T. and Zhang, L. (2017) An Empirical Study on the limitations of Static Code Analysis for Vulnerability Detection. IEEE Transactions on Software Engineering, 43, 462-477.
[8]
Abrial, J. (2009) Modelling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge.
[9]
Clarke, E.M. (2008) The Birth of Model Checking. In: Grumberg, O. and Veith, H., Eds., 25 Years of Model Checking, Springer, Berlin, 1-26.
[10]
Strunk, E.A., Aiello, M.A. and Knight, J.C. (2006) A Survey of Tools for Model Checking and Model-Based Development. Technical Report, Department of Computer Science, University of Virginia, Charlottesville.
[11]
Jhala, R. and Majumdar, R. (2009) Software Model Checking. ACM Computing Surveys, 41, 1-54. https://doi.org/10.1145/1592434.1592438
[12]
Ben-Ari, M. (2008) Principles of SPIN Model Checker. Springer-Verlag, London.
[13]
Valero, M. (2005) Modal Abstraction and Replication of Processes with Data. Springer, Berlin. https://pdfs.semanticscholar.org/804b/02fd88d199360b65fb6efe13e93e84428596.pdf
[14]
Queille, J.P. and Sifakis, J. (1982) Specification and Verification of Concurrent System in CESAR. In: Dezani-Ciancaglini, M. and Montanari, U. Eds., Programming 1982: International Symposium on Programming, Springer, Berlin, 337-351. https://link.springer.com/chapter/10.1007/3-540-11494-7_22 https://doi.org/10.1007/3-540-11494-7_22
[15]
Clarke, E.M., Emerson, E.A. and Sistla, A.P. (1986) Automatic Verification of Finite-StateConcurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8, 244-263. https://doi.org/10.1145/5397.5399
[16]
Esparza, J. (1994) Model Checking Using Net Unfolding. Science of Computer Programming, 23, 151-195. https://doi.org/10.1016/0167-6423(94)00019-0
[17]
McMillan, K.L. (1992) Symbolic Model Checking: An Approach to the State Explosion Problem. Ph.D. Thesis, Carnegie Mellon University, Pittsburgh, 1-212.
[18]
Yin, X. (2006) An Introduction to the SPIN Model Checker. Tools for Model Checking and Model-Based Development Project Report: Tool Description and Analysis.
[19]
Biere, A. (2008) Tutorial on Model Checking: Modelling and Verification in Computer Science. In: Horimoto, K., Regensburger, G., Rosenkranz, M. and Yoshida, H., Eds., AB 2008: Algebraic Biology, Lecture Notes in Computer Science, Springer, Berlin, 16-21. https://link.springer.com/chapter/10.1007/978-3-540-85101-1_2 https://doi.org/10.1007/978-3-540-85101-1_2
[20]
Khurshid, S., Pasareanu, C.S. and Visser, W. (2003) Generalized Symbolic Execution for Model Checking and Testing. In: Garavel, H. and Hatcliff, J., Eds., TACAS 2003: Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, 553-568. https://doi.org/10.1007/3-540-36577-X_40
[21]
Armando, A., Mantovani, J. and Platania, L. (2006) Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers. In: Valmari, A., Ed., SPIN 2006: Model Checking Software, Springer, Berlin, 146-162. https://doi.org/10.1007/11691617_9
[22]
Yang, Z., Wang, C., Gupta, A. and Ivančić, F. (2008) Model Checking Sequential Software Programs via Mixed Symbolic Analysis. ACM Transaction on Design Automation of Electronic System, 14, 1-26. https://doi.org/10.1145/1455229.1455239
[23]
Wehrle, M. and Kupferschmid, S. (2010) Context-Enhanced Directed Model Checking. In: Van De Pol, J. and Weber, M., Eds., SPIN 2010: Model Checking Software, Springer, Berlin, 88-105. https://doi.org/10.1007/978-3-642-16164-3_7 https://link.springer.com/chapter/10.1007/978-3-642-16164-3_7
[24]
Eyer, D. and Stahlbauer, A. (2013) BDD-Based Software Model Checking with CPACHECKER. In: Kučera, A., Henzinger, T.A., Nešetřil, J., Vojnar, T. and Antoš, D., Eds., MEMICS 2012: Mathematical and Engineering Methods in Computer Science, Springer, Berlin, 1-11. https://doi.org/10.1007/978-3-642-36046-6_1 https://link.springer.com/chapter/10.1007/978-3-642-36046-6_1
[25]
Noureddine, M. and Zaraket, F.A. (2016) Model Checking Software with First Order Logic Specifications Using AIG Solvers. IEEE Transactions on Software Engineering, 42, 741-763. https://scholar.google.com/citations?user=iLJ3TyQAAAAJ&hl=en https://doi.org/10.1109/TSE.2016.2520468
[26]
Cousot, P. (2001) Abstract Interpretation Based Formal Methods and Future Challenge. https://www.di.ens.fr/~cousot/publications.www/Cousot-LNCS2000-sv-sb.pdf
[27]
Abraham, E. and Kremer, G. (2017) Satisfiability Checking: Theory and Application. Springer International Publishing, New York.
[28]
Ball, T., Podelski, A. and Rajamani, S.K. (2000) Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T. and Yi, W., Eds., TACAS 2001: Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, 268-283. https://link.springer.com/chapter/10.1007/3-540-45319-9_19 https://doi.org/10.1007/3-540-45319-9_19
[29]
Ball, T., Majumdar, R., Millstein, T. and Rajamani, S.K. (2001) Automatic Predicate Abstraction of C Programs. Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, Snowbird, June 2001, 203-213. https://doi.org/10.1145/378795.378846
[30]
Flanagan, C. and Qadeer, S. (2002) Predicate Abstraction for Software Verification. Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming, Portland, 16-18 January 2002, 191-202. https://doi.org/10.1145/503272.503291
[31]
Fehnker, A., Brauer, J., Huuck, R. and Seefried, S. (2008) Goanna: Syntactic Software Model Checking. In: Cha, S., Choi, J.Y., Kim, M., Lee, I. and Viswanathan, M., Eds., ATVA 2008: Automated Technology for Verification and Analysis, Springer, Berlin, 216-221. https://link.springer.com/chapter/10.1007/978-3-540-88387-6_17
[32]
Griesmayer, A. (2007) Debugging Software from Verification to Repair. Ph.D. Thesis, Graz University of Technology, Austria, 1-108
[33]
Li, Y. (2014) Symbolic Abstraction with SMT Solvers. Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming, San Diego, 22-24 January 2014, 607-618. https://doi.org/10.1145/2535838.2535857
[34]
Lomuscio, A. and Michaliszyn, J. (2015) Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions. Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent, Istanbul, 4-8 May 2015, 189-198.
[35]
Clarke, E., Biere, A., Rami, R. and Zhu, Y. (2001) Bounded Model Checking Using Satisfiability Solving. Formal Method in System Design, 19, 7-34. https://doi.org/10.1023/A:1011276507260
[36]
Merz, F., Falke, S. and Sinz, C. (2012) LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. In: Joshi, R., Müller, P. and Podelski, A., Eds., VSTTE 2012: Verified Software: Theories, Tools, Experiments, Springer, Berlin, 146-161. https://doi.org/10.1007/978-3-642-27705-4_12
[37]
Peled, D. (2001) Model Checking. Department of Computer Science, Bar llan University, Ramat Gan.
[38]
Guo, H.Y., Wu, M., Zhou, L.D., Hu, G., Yang, J.F. and Zhang L. (2011) Practical Software Model Checking via Dynamic Interface Reduction. Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles, Cascais, 23-26 October 2011, 265-278. https://doi.org/10.1145/2043556.2043582
[39]
Nguyen, V.Y. and Ruys, T.C. (2013) Selected Dynamic Issues in Software Model Checking. International Journal on Software Tools for Technology Transfer, 15, 337-362. https://doi.org/10.1007/s10009-012-0261-y
[40]
Gupta, A., Kahlon, V., Qadeer, S. and Touili, T. (2018) Model Checking Concurrent Programs. In: Clarke, E., Henzinger, T., Veith, H. and Bloem, R., Eds., Handbook of Model Checking, Springer, Cham, 573-611. https://doi.org/10.1007/978-3-319-10575-8_18
[41]
Santos, I.S., Rocha, L.S., Santos-Neto, P.A. and Andrade, R.M.C. (2016) Model Verification of Dynamic Software Product Lines. Proceedings of the XXX Brazilian Symposium on Software Engineering, Maringá, 19-23 September 2016, 113-122. https://doi.org/10.1145/2973839.2973852
[42]
Avgerinos, T., Rebert, A., Cha, S.K. and Brumley, D. (2014) Enhancing Symbolic Execution with Veritesting. Proceedings of the 36th International Conference on Software Engineering, Hyderabad, 31 May-7 June 2014, 1083-1094. https://doi.org/10.1145/2568225.2568293
[43]
Bohme, M., Pham, V.T. and Roychoudhury, A. (2017) Coverage-Based Greybox Fuzzing as Markov Chain. IEEE Transactions on Software Engineering, 45, 489-506. https://doi.org/10.1109/TSE.2017.2785841
[44]
Gulzar, M.A., Musuvathi, M. and Kim, M. (2020) BigTest: A Symbolic Execution Based Systematic Test Generation Tool for Apache Spark. Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Companion Proceedings, Seoul South, 27 June-19 July 2020, 61-64. https://doi.org/10.1145/3377812.3382145
[45]
Chalupa, M., Jasek, T., Movak, J., Rechtackova, A., Sokova, V. and Strejcek, J. (2021) Symbiotic 8: Beyond Symbolic Execution. In: Groote, J.F. and Larsen, K.G., Eds., TACAS 2021: Tools and Algorithms for the Construction and Analysis of Systems, Springer, Cham, 453-457. https://doi.org/10.1007/978-3-030-72013-1_31
[46]
Mrazek, J., Bauch, P., Lauko, H. and Barnat, J. (2016) SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. In: Bošnački, D. and Wijs, A., Eds., SPIN 2016: Model Checking Software, Springer, Cham, 208-213. https://doi.org/10.1007/978-3-319-32582-8_14
[47]
Visser, W., Pasareanu, C.S. and Khurshid, S. (2004) Test Input Generation with Java Pathfinder. ACM SIGSOFT Software Engineering Notes, 29, 97-107. https://doi.org/10.1145/1013886.1007526
[48]
Penczek, W., Szreter, M., Gerth, R. and Kuiper, R. (2000) Improving Partial Order Reductions for Universal Branching Time Properties. Fundameta Informaticae, 43, 245-267. https://doi.org/10.3233/FI-2000-43123413
[49]
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L. and Hwang, L.J. (1992) Symbolic Model Checking: 1020 States and Beyond. Information and Computation, 98, 142-170. https://doi.org/10.1016/0890-5401(92)90017-A
[50]
Havelund, K. and Pressburger, T. (1999) Model Checking Java Programs Using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2, 366-381. https://doi.org/10.1007/s100090050043
[51]
Cadar, C., Dunbar, D. and Engler, D.R. (2008) KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, San Diego, 8-10 December 2008, 209-224.
[52]
Clarke, E.M., Grumberg, O., Kroening D., Peled, D. and Veith H. (2018) Model Checking. 2nd Edition, MIT Press, Cambridge.
[53]
McMillan, K.L. (1999) Symbolic Model Checking. In: Inan, M.K. and Kurshan, R.P., Eds., Verification of Digital and Hybrid Systems, Springer, Berlin, 117-137. https://doi.org/10.1007/978-3-642-59615-5_6
[54]
Godefroid, P. (1996) Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, Berlin. https://doi.org/10.1007/3-540-60761-7
[55]
Sen, K., Marinov, D., Agha, G. and Sridharan, M. (2016) Guiding Symbolic Execution towards Unexplored Code. Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications, Amsterdam, 2-4 November 2016, 753-771.
[56]
Bao, X., Yin, H., Chen, X. and Zhang, L. (2018) Speeding Up Symbolic Model Checking with Machine Learning. Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, Montpellier, 3-7 September 2018, 570-580.
[57]
Ma, L., Zhang, F.Y., et al. (2018) DeepGauge: Multi-Granularity Testing Criteria for Deep Learning Systems. ArXiv: 1803.07519.
[58]
Durrelli, V.H.S., Durelli, R.S., Borges, S.S., Endo, A.T., Eler, M.M., Dias, D.R.C. and Guimaraes, M.P. (2019) Machine Learning Applied to Software Testing: A Systematic Mapping Study. IEEE Transactions on Realiability, 68, 1189-1212. https://doi.org/10.1109/TR.2019.2892517
[59]
Vardhan, A., Sen, K., Viswanathan, M. and Agha, G. (2004) Learning to Verify Safety Properties. In: Davies, J., Schulte, W. and Barnett, M., Eds., ICFEM 2004: Formal Methods and Software Engineering, Springer, Berlin, 274-289. https://doi.org/10.1007/978-3-540-30482-1_26
[60]
Kalyan, A., Mohta, A., Polozov, O., Batra, D., Jain, P. and Gulwani, S. (2018) Neural-Guided Deductive Search for Real-Time Program Synthesis from Examples. ArXiv: 1804.01186. https://arxiv.org/abs/1804.01186
[61]
Gennari, J., Gurfinkel, A., Kahsai, T., Navas, J.A. and Schwartz, E.J. (2018) Executable Counterexamples in Software Model Checking. In: Piskac, R. and Rümmer, P., Eds., VSTTE 2018: Verified Software: Theories, Tools and Experiments, Vol. 11294, Springer, Cham, 17-37. https://doi.org/10.1007/978-3-030-03592-1_2
[62]
Utting, M. and Legeard, B. (2006) Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann, San Francisco.
[63]
Havelund, K. and Rosu, G. (2002) Monitoring Programs Using Rewriting. Proceedings of the 14th International Conference on Computer Aided Verification, Copenhagen, 27-31 July 2002, 450-462.
[64]
Pacheco, C., Lahiri, S.K., Ernst, M.D. and Ball, T. (2007) Feedback-Directed Random Test Generation. 29th International Conference on Software Engineering, Minneapolis, MN, 20-26 May 2007, 75-84. https://doi.org/10.1109/ICSE.2007.37
[65]
Harman, M. and Sthamer, H. (2002) Search-Based Software Testing. Proceedings of the 2002 International Symposium on Software Testing and Analysis, Roma, 22-24 July 2002, 249-258.
[66]
King, J.C. (1976) Symbolic Execution and Program Testing. Communications of the ACM, 19, 385-394. https://doi.org/10.1145/360248.360252
[67]
Liang, G., Liao, L., Xu, X., Du, J., Li, G. and Zhao, H. (2013) Effective Fuzzing Based on Dynamic Taint Analysis. 2013 Ninth International Conference on Computational Intelligence and Security, Emeishan, 14-15 December 2013, 615-619. https://doi.org/10.1109/CIS.2013.135
[68]
Kwiatkowska, M., Norman, G. and Parker, D. (2018) Probabilistic Model Checking: Advances and Applications. In: Drechsler, R., Ed., Formal System Verification, Springer, Cham, 73-121. https://doi.org/10.1007/978-3-319-57685-5_3
[69]
Sen, K., Marinov, D. and Agha, G. (2005) CUTE: A Concolic Unit Testing Engine for C. Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE-13), Chicago, 5-9 September 2005, 263-272.
[70]
Satpathy, M. and Ramesh, S. (2007) Test Case Generation from Formal Models through Abstraction Refinement and Model Checking. Proceedings of the 3rd International Workshop on Advances in Model-Based Testing, London, 9-12 July 2007, 85-94. https://doi.org/10.1145/1291535.1291544
[71]
Emerson, E.A. and Namjoshi, K.S. (1998) Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8, 244-263.
[72]
Lamport, L. (1986) On Interprocess Communication. Distributed Computing, 1, 77-85. https://doi.org/10.1007/BF01786227
[73]
Alur, R., Bodík, R., Juniwal, G. and Seshia, S.A. (2015) Synthesis of Cyber-Physical Systems. Proceedings of the IEEE, 103, 1589-1609.
[74]
Gurfinkel, A. and Chaki, S. (2015) Combining Static Analysis and Model Checking for Program Analysis. Formal Methods in System Design, 47, 62-91.
[75]
Zhang, L., Chen, Y., Zhang, Y. and Liu, Y. (2020) A Critical Survey of Machine Learning-Assisted Verification. IEEE Transactions on Software Engineering, 47, 1064-1087.
[76]
Pei, K., Cao, Y., Yang, J. and Jia, Z. (2017) Deep Learning-Based Software-Defined Networking for IoT Security. IEEE Network, 31, 80-85.
[77]
Gao, Y., Wei, Y., Sun, J. and Zhang, X. (2019) Learning-Based Abstraction Refinement for Software Model Checking. Frontiers of Information Technology and Electronic Engineering, 20, 372-382.
[78]
Zhang, X., Liu, Y., Huang, L. and Zhang, Y. (2021) Reinforcement Learning-Based Heuristic for Accelerating Software Model Checking. Journal of Systems and Software, 174, Article ID: 110950.
