带复杂数据结构的模型检测工具

A Model-Checking Tool with Non-Trivial Data Structures

模型检测是近二十几年来最成功的自动验证技术之一 ,而模型检测工具的开发是将模型检测和实际相结合的关键 为了有效地对涉及到复杂数据类型的并发传值系统进行模型检测 ,总结了以扩展的带赋值符号迁移图和模态图分别作为并发系统和逻辑公式的语义模型来实现模型检测工具的工作 ,特别是将复杂数据结构引入传值进程定义语言和带赋值符号迁移图

Model-checking is one of the most successful automatic verification techniques over the last 20 years, and the development of model-checking tools is the bridge that connects theories in this field and applications. In order to efficiently model-check value-passing current systems which involve non-trivial data structures. An extended symbolic transition graph with assignment (STGA) is introduced as the semantic model of concurrent systems, and a modal graph is used as the semantic model of logic formulae. And then following an on-the-fly algorithm, a prototype tool is implemented to model-check concurrent systems. In this paper model-checking is summarized by introducing non-trivial data structures into value-passing process specification language and STGA. A practical case is also presented to justify the tool's efficiency.