构建度量区时序逻辑的时间自动机

作者：王勤思

来源：计算机工程与设计, 2011, (02): 568-571+575.

DOI：10.16208/j.issn1000-7024.2011.02.035

• 模型检测
• 实时时序逻辑
• 度量区时序逻辑
• 基于迁移的扩展时间Bchi自动机
• Tableau方法 model checking
• real-time temporal logic
• metric interval temporal logic
• transition-based generalized timed Buhi automata
• tableau method

在实时系统的形式验证中,为了直接验证带有明显时间约束的性质,选用了一种被广泛接受的(线性时间)实时时序逻辑——度量区时序逻辑来描述待验证的性质;提出了基于迁移的扩展时间B chi自动机;构建了度量区时序逻辑的基于迁移的扩展时间B chi自动机。这样扩展了已有实时系统模型检测工具的性质规范语言的表达能力,使其能直接处理和验证带有明显时间约束的性质。实现的工具表明,该算法有效且可行,并且显著地减少了结果自动机节点和迁移的数量,从而降低了结果自动机的大小,有利于进一步的模型检测过程。

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