胡棐禹

摘要：线性时段不变式是一类重要的时段演算公式。文献[1]中提出一种验证算法，能够针对以时间自动机建模的系统，模型检验其是否满足一个扩展的线性时段不变式。在验证一类特定公式时，该算法需要引入O（b）个辅助变量，且需全程保留它们的值，会导致检验这类公式所需的变量数和复杂度急剧增长。该文提出一种基于系统反转的模型检验方法，并为线性时段不变式的模型检验问题提供一种全新的解决思路

关键词：模型检验；时间自动机；线性时段不变式；切变；反向系统

中图分类号：TP311 文献标识码：A 文章编号：1009-3044（2016）03-0071-02

1 背景

在某些实时系统中，如航空交管系统、化工厂控制系统等，任何错误都可能造成重大经济损失和人员伤亡。显然，这类安全攸关系统对设计正确性的要求极其严格。如何在系统开发的早期阶段验证设计的正确性，成为研发人员必须面对的问题。

2 相关概念与术语

2.1 实时系统的形式化模型

近些年来许多不同的实时系统模型被提出。其中，R Alur等人提出的时间自动机（Timed Automata）已成为标准。时间自动机是在有穷状态自动机的基础上扩充了一个时钟变量集合X得到的。

2.2 实时系统的时段性质与线性时段不变式

线性时段不变式是实时系统的一类重要性质，由周巢尘等人1994年首次提出。它可用时段演算公式表示，形如：

[A≤e-b≤B?S∈LcSS≤M]

意思是若观察区间[b，e]的长度满足约束：[A≤e-b≤B]，则在该区间上系统处于各个状态的累计时间就满足线性约束。

2.3 带切变的线性时段不变式及其模型检验