ISSN 1000-1239 CN 11-1777/TP

• 综述 •

### 软件模型检测中的抽象模型研究综述

1. 1(南京航空航天大学计算机科学与技术学院 南京 210016); 2(南京林业大学信息科学技术学院 南京 210037) (owei@nuaa.edu.cn)
• 出版日期: 2015-07-01
• 基金资助:
基金项目：国家自然科学基金项目(61170043,61100034,61272083)；国家“九七三”重点基础研究发展计划基金项目(2014CB744904)

### 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.