段喜龙，陆智伟+，郑 巍，陈晋升，樊 鑫，肖 鹏

(1.南昌航空大学 软件学院，江西 南昌 330063；2.南昌航空大学 软件测评中心，江西 南昌 330063)

0 引 言

模型检测作为软件系统验证中的一个常用手段，已经在多个领域得到了应用。在基于模型开发的软件系统验证中，线性时态逻辑LTL(linear-time temporal logic)用于描述软件的性质，这些性质又被称为线性时间属性。这是迈向构建模型检测理论重要的一步，现已得到了广泛的应用[1-4]。

LTL能得到广泛应用有赖于人们对它的表达能力的研究。文献[5]中给出，LTL的表达能力与一阶谓词逻辑等价。尽管它们的表达能力是一样的，但两者在可满足性问题，可判定问题还有推理问题上的解决难易程度却大不相同。这些问题在一阶谓词逻辑上的解决难度是非初等的，也就是说它的解决方案的复杂度上界是可以无限增长的[6，7]。而在LTL上，这些问题的解决难度都只是PSPACE-完全的[8，9]。这也是能够得到广泛应用的一个重要的理论支撑。而LTL语句生成需要测试人员对被测模型要有充分的了解，而这一过程需要花费很多时间。

在模型检测方面，文献[12]从时间逻辑角度对系统行为进行了刻画，文献[13]采用时间抽象互模拟方法来验证模型；文献[14]分别采用动态层次化UML状态机模型和符号模型进行验证；文献[15]将时间自动机(timed automata，TA)模型转换为有限状态迁移图，并将有限状态迁移图转换为非确定有限状态机(finite state machine，FSM)，从而采用基于FSM的方法进行测试；文献[16]是一种通过在运行时验证软件源代码中的断言来检测不一致的方法。……