The role of model checking in software engineering
The role of model checking in software engineering
复制标题
模型检查在软件工程中的作用
DOI：
10.1007/s11704-016-6192-0
复制
发表时间：
2018-06
影响因子：
4.2
通讯作者：
Zhao Jianjun
中科院分区：
文献类型：
--
作者：
Karna Anil Kumar;Chen Yuting;Yu Haibo;Zhong Hao;Zhao Jianjun
模型检验是一种形式化验证技术。它需要一个详尽的策略来检查硬件电路和网络协议是否符合所需的属性。模型检测在软件工程中已经发展了30多年，目前在验证相当复杂的软件工件方面发挥着重要的作用。特别是，我们检索了在著名会议、研讨会、研讨会和期刊上发表的相关文献，并调查了（1）可适用于软件开发的各种模型检查技术及其实现，以及（2）在软件开发生命周期的不同阶段使用模型检查。我们观察到，模型检查对于软件调试、约束求解和恶意软件检测是有用的，并且它可以帮助验证不同类型的软件系统，例如面向对象和面向方面的系统、面向服务的应用、基于Web的应用和GUI应用，包括安全和任务关键型系统。该调查预计将帮助人类工程师理解模型检查在软件工程中的作用，以及决定哪些模型检查技术和/或工具适用于开发、分析和验证实际软件系统。对于研究人员来说，调查还指出了模型检查如何适应他们在软件工程及其挑战方面的研究主题。
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.
登录
查看更多内容
DOI：
10.1109/ase.2001.989825
发表时间：
2001-11
期刊：
Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001)
影响因子：
--
作者：
K. S. Barber;T. Graser;J. Holt
通讯作者：
K. S. Barber;T. Graser;J. Holt
DOI：
10.1145/940071.940106
发表时间：
2003-09
期刊：
--
影响因子：
--
作者：
D. Giannakopoulou;J. Magee
通讯作者：
D. Giannakopoulou;J. Magee
DOI：
10.1145/2970276.2970319
发表时间：
2016-08
期刊：
2016 31st IEEE/ACM International Conference on Automated Software Engineering (ASE)
影响因子：
--
作者：
Masataka Nishi
通讯作者：
Masataka Nishi
DOI：
10.1109/rtas.2013.6531083
发表时间：
2013-04
期刊：
2013 IEEE 19th Real-Time and Embedded Technology and Applications Symposium (RTAS)
影响因子：
--
作者：
Bernard Blackham;Gernot Heiser
通讯作者：
Bernard Blackham;Gernot Heiser
影响因子：
3.7
作者：
Yean-Ru Chen;Jia-Jen Yeh;Pao-Ann Hsiung;Sao-Jie Chen
通讯作者：
Yean-Ru Chen;Jia-Jen Yeh;Pao-Ann Hsiung;Sao-Jie Chen