The role of model checking in software engineering  

作　　者：Anil Kumar KARNA Yuting CHEN Haibo YU Hao ZHONG Jianjun ZHAO 

机构地区：[1]Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai 200240, China [2]School of Software, Shanghai Jiao Tong University, Shanghai 200240, China [3]Department of Advanced Information Technology, Kyushu University, Fukuoka 819-0395, Japan

出　　处：《Frontiers of Computer Science》2018年第4期642-668,共27页中国计算机科学前沿（英文版）

摘　　要：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 liter- atures 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 soft- ware 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.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 liter- atures 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 soft- ware 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.

关 键 词：software engineering model checking state-explosion 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术] TP311.5[自动化与计算机技术—计算机科学与技术]