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