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