The role of model checking in software engineering

被引:0
作者
Anil Kumar Karna
Yuting Chen
Haibo Yu
Hao Zhong
Jianjun Zhao
机构
[1] Shanghai Jiao Tong University,Department of Computer Science and Engineering
[2] Shanghai Jiao Tong University,School of Software
[3] Kyushu University,Department of Advanced Information Technology
来源
Frontiers of Computer Science | 2018年 / 12卷
关键词
software engineering; model checking; state-explosion;
D O I
暂无
中图分类号
学科分类号
摘要
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.
引用
收藏
页码:642 / 668
页数:26
相关论文
共 198 条
[1]  
Ben-Ari M(2010)A primer on model checking Inroads 1 40-47
[2]  
Andersen H R(1999)Partial model checking of modal equations: a survey International Journal on Software Tools for Technology Transfer 2 242-259
[3]  
Lind-Nielsen J(2004)Model checking and abstraction to the aid of parameterized systems (a survey) Computer Languages, Systems & Structures 30 139-169
[4]  
Zuck L D(2009)Testing with model checkers: a survey Software Testing, Verification & Reliability 19 215-261
[5]  
Pnueli A(2009)Model checking: Algorithmic verification and debugging Communications of the ACM 52 74-84
[6]  
Fraser G(2009)Counterexample generation in probabilistic model checking IEEE Transactions on Software Engineering 35 241-257
[7]  
Wotawa F(2014)Making CEGAR more efficient in software model checking IEEE Transactions on Software Engineering 40 1206-1223
[8]  
Ammann P(2013)Verifying protocol conformance using software model checking for the model-driven development of embedded systems IEEE Transactions on Software Engineering 39 1307-1325
[9]  
Clarke E M(2013)Elaborating requirements using model checking and inductive learning IEEE Transactions on Software Engineering 39 361-383
[10]  
Emerson E A(2014)Modular software model checking for distributed systems IEEE Transactions on Software Engineering 40 483-501