构建度量区时序逻辑的时间自动机 |
| |
引用本文: | 王勤思.构建度量区时序逻辑的时间自动机[J].计算机工程与设计,2011,32(2):568-571,575. |
| |
作者姓名: | 王勤思 |
| |
作者单位: | 中国科学院软件研究所,计算机科学重点实验室,北京,100190;中国科学院研究生院,北京,100049 |
| |
摘 要: | 在实时系统的形式验证中,为了直接验证带有明显时间约束的性质,选用了一种被广泛接受的(线性时间)实时时序逻辑——度量区时序逻辑来描述待验证的性质;提出了基于迁移的扩展时间B chi自动机;构建了度量区时序逻辑的基于迁移的扩展时间B chi自动机。这样扩展了已有实时系统模型检测工具的性质规范语言的表达能力,使其能直接处理和验证带有明显时间约束的性质。实现的工具表明,该算法有效且可行,并且显著地减少了结果自动机节点和迁移的数量,从而降低了结果自动机的大小,有利于进一步的模型检测过程。
|
关 键 词: | 模型检测 实时时序逻辑 度量区时序逻辑 基于迁移的扩展时间Bchi自动机 Tableau方法 |
本文献已被 CNKI 万方数据 等数据库收录! |
|