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

A Model-Checking Tool with Non-Trivial Data Structures

作　　者：张轶[1] 林惠民[1] 

机构地区：[1]中国科学院软件研究所计算机科学重点实验室,北京100080

出　　处：《计算机研究与发展》2004年第11期1990-1999,共10页Journal of Computer Research and Development

基　　金：国家自然科学基金项目 (6983 3 0 2 0 )

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

关 键 词：模型检测 传值进程 带赋值符号迁移图 谓词μ演算 复杂数据结构 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]