ISSN 1000-1239 CN 11-1777/TP

Journal of Computer Research and Development ›› 2015, Vol. 52 ›› Issue (7): 1580-1603.doi: 10.7544/issn1000-1239.2015.20140413

Previous Articles     Next Articles

Abstract Modeling Formalisms in Software Model Checking

Wei Ou1, Shi Yufeng1, Xu Bingfeng1,2, Huang Zhiqiu1, Chen Zhe1   

  1. 1(College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016);2(College of Information Science and Technology, Nanjing Forestry University, Nanjing 210037)
  • Online:2015-07-01

Abstract: Abstraction is a fundamental technique for solving the state-explosion problem in software model checking. In this paper, we survey a variety of abstract modeling formalisms that have been developed for this over the years. We first provide an overview of abstract software model checking based on the theoretical framework of abstract interpretation. We then discuss in detail several abstract modeling formalisms that are represented by 1) boolean Kripke structures, supporting traditional over-approximation or under-approximation; 2) Kripke modal transition systems and mixed transition systems, respectively corresponding to 3-valued and 4-valued Kripke structures, supporting both over-approximation and under-approximation on a single model; and 3) models with hyper transitions, including generalized Kripke modal transition systems and hyper transition systems, allowing for more precise abstract model checking. We discuss the corresponding approximation relations and optimal abstract models, and highlight their shortcomings and the motivations for the development of new formalisms. We also introduce the completeness results of abstract modeling formalisms. Finally, we discuss the problems in theoretical and practical aspects of abstract models and point out future research directions.

Key words: abstract models, over-approximation, under-approximation, model checking, multi-valued models

CLC Number: