Using predicate abstraction to reduce object-oriented programs for model checking
Using predicate abstraction to reduce object-oriented programs for model checking
复制标题
使用谓词抽象来减少模型检查的面向对象程序
DOI：
10.1145/349360.351125
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
J. Penix
中科院分区：
文献类型：
--
作者：
W. Visser;Seungjoon Park;J. Penix
虽然模型检查应用于软件需求规范变得越来越普遍，但它很少应用于软件实现。 NASA 艾姆斯的自动化软件工程小组目前正在研究对实际源代码进行模型检查的用途，最终目标是允许软件开发人员通过模型检查来增强传统测试。由于模型检查存在状态爆炸问题，因此程序模型检查的主要障碍之一是减小程序的大小。在本文中，我们研究了使用抽象技术来减少用 C++ 编写的实时操作系统内核的状态空间。我们展示了如何在谓词抽象（一种基于抽象解释的技术）框架内形式化和改进非正式抽象论证。我们引入了一些谓词抽象的扩展，所有这些扩展都允许它在面向对象语言的类实例框架中使用。然后，我们演示如何将这些扩展集成到执行 Java 程序自动谓词抽象的抽象工具中。
While it is becoming more common to see model checking applied to software requirements specifications, it is seldom applied to software implementations. The Automated Software Engineering group at NASA Ames is currently investigating the use of model checking for actual source code, with the eventual goal of allowing software developers to augment traditional testing with model checking. Because model checking suffers from the state-explosion problem, one of the main hurdles for program model checking is reducing the size of the program. In this paper we investigate the use of abstraction techniques to reduce the state-space of a real-time operating system kernel written in C++. We show how informal abstraction arguments could be formalized and improved upon within the framework of predicate abstraction, a technique based on abstract interpretation. We introduce some extensions to predicate abstraction that all allow it to be used within the class-instance framework of object-oriented languages. We then demonstrate how these extensions were integrated into an abstraction tool that performs automated predicate abstraction of Java programs.