模型检验中对CTL公式的空属性探测

• 作者: 郭建 金乃咏
• 来源期刊: 西安电子科技大学学报（自然科学版）
• 学科: 工学
• 关键词: 模型检验 空属性探测 可计算时态逻辑公式 验证综合系统系统
• 年，卷（期）: 2007,（5）
• 页码范围: 794-799
• 页数: 6页
• 分类号: TP301.1
• 字数: 3987字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-2400.2007.05.023

摘要

在模型检验中建立了一种新方法:检验可计算时态逻辑(CTL)公式描述的系统属性是否为空属性.根据原子命题的极性,用TRUE 或FALSE替换原子命题,得到一系列的CTL公式,再对这些CTL公式用模型检验工具验证,若CTL公式中有一个通过了验证,则可得出该系统属性是一个空属性.该方法对CTL公式的空属性的探测不需要对它的所有子公式用TRUE 或FALSE替换,只需对原子命题替换,这样检验的次数与原子命题的个数呈线性关系.利用验证综合系统对十字路口交通控制器规范的空属性进行了检验.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	金乃咏	华东师范大学软件学院	5	23	2.0	4.0
2	郭建	西安电子科技大学微电子学院	4	18	2.0	4.0