TY - JOUR
T1 - The role of model checking in software engineering
AU - Karna, Anil Kumar
AU - Chen, Yuting
AU - Yu, Haibo
AU - Zhong, Hao
AU - Zhao, Jianjun
N1 - Funding Information:
The authors are grateful to anonymous referee for their valuable comments and suggestions to improve the presentation and contents of this paper. This research was sponsored in part by the National Basic Research Program of China (2015CB352203) and the National Nature Science Foundation of China (Grant Nos. 61572312 and 61572313). Jianjun Zhao was supported in part by Japan Society for the Promotion of Science, Grantin- Aid for Research Activity Start-up (16H07031). Hao Zhong was partially supported by Science and Technology Commission of Shanghai Municipality’s Innovation Action Plan (15DZ1100305).
Publisher Copyright:
© 2018, Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature.
PY - 2018/8/1
Y1 - 2018/8/1
N2 - Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, model checking is now playing an important role in software engineering for verifying rather complicated software artifacts. This paper surveys the role of model checking in software engineering. In particular, we searched for the related literatures published at reputed conferences, symposiums, workshops, and journals, and took a survey of (1) various model checking techniques that can be adapted to software development and their implementations, and (2) the use of model checking at different stages of a software development life cycle. We observed that model checking is useful for software debugging, constraint solving, and malware detection, and it can help verify different types of software systems, such as object- and aspect-oriented systems, service-oriented applications, web-based applications, and GUI applications including safety- and mission-critical systems. The survey is expected to help human engineers understand the role of model checking in software engineering, and as well decide which model checking technique(s) and/or tool(s) are applicable for developing, analyzing and verifying a practical software system. For researchers, the survey also points out how model checking has been adapted to their research topics on software engineering and its challenges.
AB - Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, model checking is now playing an important role in software engineering for verifying rather complicated software artifacts. This paper surveys the role of model checking in software engineering. In particular, we searched for the related literatures published at reputed conferences, symposiums, workshops, and journals, and took a survey of (1) various model checking techniques that can be adapted to software development and their implementations, and (2) the use of model checking at different stages of a software development life cycle. We observed that model checking is useful for software debugging, constraint solving, and malware detection, and it can help verify different types of software systems, such as object- and aspect-oriented systems, service-oriented applications, web-based applications, and GUI applications including safety- and mission-critical systems. The survey is expected to help human engineers understand the role of model checking in software engineering, and as well decide which model checking technique(s) and/or tool(s) are applicable for developing, analyzing and verifying a practical software system. For researchers, the survey also points out how model checking has been adapted to their research topics on software engineering and its challenges.
UR - http://www.scopus.com/inward/record.url?scp=85046025714&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85046025714&partnerID=8YFLogxK
U2 - 10.1007/s11704-016-6192-0
DO - 10.1007/s11704-016-6192-0
M3 - Review article
AN - SCOPUS:85046025714
SN - 2095-2228
VL - 12
SP - 642
EP - 668
JO - Frontiers of Computer Science
JF - Frontiers of Computer Science
IS - 4
ER -