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

作者：张轶; 林惠民

来源：Z200411018, 2004, (11): 1990-1999.

• 模型检测
• 传值进程
• 带赋值符号迁移图
• 谓词μ演算
• 复杂数据结构 model-checking
• value-passing process
• STGA
• predicate μ-calculus
• non-trivial data structures

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

• 单位
  中国科学院软件研究所; 计算机科学国家重点实验室