A Composite Model Checking Toolset for Analyzing Software Systems

9970976 Bultan，Tevfik，加州大学，圣巴巴拉一个用于分析软件系统的复合模型检查工具集在这个项目中，一个新的自动验证技术，用于分析软件规格称为复合模型检查将进行调查。模型检测是一种搜索系统状态空间以确定其是否满足给定性质的技术。模型检验过程的成功依赖于用于表示系统状态的数据结构的效率。在这个项目中，将开发一个复合模型，用于组合多个特定类型的表示，以便在状态空间搜索期间可以有效地表示所有变量类型。通过这种方式，诸如二元决策图之类的对编码布尔变量有效的表示将与诸如线性算术约束之类的可以编码无界变量的表示相结合。将实施一套工具来支持复合模型检查。工具集的分层结构将允许其他研究人员在不同级别使用它：1）测试新表示的有效性; 2）研究各种模型检查策略，如向后和向前搜索，分区和抽象;或3）分析复杂的软件规范。

9970976 Bultan, Tevfik, University of California, Santa BarbaraA Composite Model Checking Toolset for Analyzing Software SystemsIn this project a new automated verification technique for analyzing software specifications called composite model checking will be investigated. Model checking is a technique for searching the state space of a system to find out if it satisfies a given property. The success of model checking procedures rely on the efficiency of the data structures used to represent the states of the system. In this project a composite model will be developed for combining multiple type-specific representations so that all variable types can be represented efficiently during the state space search. This way, representations such as Binary Decision Diagrams which are efficient for encoding Boolean variables will be combined with representations such as linear arithmetic constraints which can encode unbounded variables. A set of tools will be implemented to support composite model checking. The layered structure of the toolset will allow other researchers to use it at various levels 1) for testing the effectiveness of new representations; 2) for investigating various model checking strategies such as backward and forward search, partitioning and abstraction; or 3) for analyzing complex software specifications.