一类线性时段不变式的验证优化与实现

胡棐禹

摘要：线性时段不变式是一类重要的时段演算公式。文献[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 带切变的线性时段不变式及其模型检验

时段演算的一个主要运算符是“切变（chop）”，用；表示。公式 B；C

含义是 B；C 在区间 [b， e] 上成立，当且仅当区间可以被切成两个子区间，使得B在第一个区间上成立，C 在第二个区间上成立。切变是个连接运算，它能通过组装几个子区间上的性质，来刻画整个系统在观察区间上的性质。定义带切变的线性时段不变式的基本形式为[A≤e-b≤B?P1，P2]

2.4 离散时段演算的有界模型检测

定义2.4（PCP、OPCP）

给出一个ELDI表达式和时间区间[t1，t2]，对于该区间中的一个整数时间时刻t，若[φ']在子区间[t1，t2]上满足，则称时刻t为潜在切变点（PCP）。对于一个潜在切变点t，若存在[1≤k≤i]，满足[t，t，=mindkt?，t|t?≤t'andt?isaPCP]。其中，[t1≤t≤t，≤t2]且[t，t，∈N，dkb，e]代表[dk]在区间[b，e]上的取值，那么在时刻[t']，称时刻t是关于[dk]的最优潜在切变点（OPCP）。也是就说，在时刻[t']，根据时刻t算得的比根据之前[dk]所有其他PCP算得的[dk]都要小。

并非任何形式的ELDI表达式都能使用基于OPCP的思想来简化验证过程。当ELDI表达式中存在切变运算符直接作用于交、非运算符的情况时，就不能运用这种想法。比如：对于[D1；（D2∧D3）]，可能发生时间区间中的所有PCP均非OPCP的情形。因为当前时刻的OPCP需同时考虑d2、d3的取值，而不像上述定义中只需考虑d2或d3的取值。

3 结束语

3.1 带切边的线性时段不变式的反向验证

上节提出了一种用于验证扩展的线性时段不变的算法。在验证ELDI公式时，该算法需引入2b+3个变量，且需全程保留它们的值，以便实时运用、更新和重置。

根据线性时段公式[dk]的定义，可知：在一个观察区间上，[dk]的真假只与系统A驻留各个位置的时长有关，与它驻留这些位置的先后次序无关。那么，可以得出以下结论：检验A的一个行为是否满足ELDI公式，等价于检验系统A的反向行为是否满足反向公式，

该方法主要包含三步：

1）对系统模型进行反转操作，得到对应的反向系统，使反向系统恰好体现正向系统中所有被检验行为；

2）对ELDI公式进行反转，得到对应的反向公式；

3）检验原系统模型对原公式的满足性，这等价于检验反向系统对反向公式的满足性。

通过这种反转方法，有效降低验证所需的复杂度，并为线性时段不变式的模型检验提供一种全新的思路。。

参考文献：

[1] Zhang Miaomiao， Dang Van Hung， Liu Zhiming. Verification of linear duration invariants by model checking CTL properties[C]. Proceedings of the 5th international colloquium on Theoretical Aspects of Computing. Berlin， Heidelberg： Springer-Verlag， 2008： 395-409.

[2] Zhang Miaomiao， Liu Zhiming， Zhan Naijun. Model checking linear duration invariants of networks of automata[C]. FSEN'09 Proceedings of the Third IPM international conference on.Fundamentals of Software Engineering. Berlin， Heidelberg： Springer-Verlag， 2010： 244-259.

[3] Pham Hong Thai， Dang Van Hung. Verifying linear duration constraints of timed automata[C]. ICTAC'04 Proceedings of the First international conference on Theoretical Aspects of Computing. Berlin， Heidelberg： Springer-Verlag， 2005： 295-309.

[4] Zhao Jianhua， Dang Van Hung. Checking timed automata for some discretisable duration properties[J]. Journal of Computer Science and Technology， 2000， 15（5）： 423-429.

[5] Li Yong， Dang Van Hung. Checking temporal duration properties of timed automata[J]. Journal of Computer Science and Technology， 2002， 17（6）： 689-698.