反向验证带切变线性时段不变式.doc

反向验证带切变线性时段不变式 　　【摘 要】线性时段不变式是一类重要的时段演算公式，可以用来描述实时系统的时段性质，对其验证算法的研究具有相当高的理论意义和实际应用价值。文献[3]中提出的算法在验证某些公式时需要引入O（b）个辅助变量，庞大的变量数目会限制该算法在实际工业领域的应用。针对该问题，本文提出了一种新颖的解决思路――通过反转原系统得到其反向系统，然后在反向系统上验证对应的反向公式。它与在原系统上验证正向公式的结果等价，但只需引入O（1）个辅助变量，扩大了文献[3]所提算法在实际工业领域的适用范围。 【关键词】形式化验证；线性时段不变式；时间自动机；反向系统 Reversed Verification of Linear Duration Invariants with Chops ZHANG Xue-zhou （School of Software Engineering， Tongji University， Shanghai 201804， China） 【Abstract】Linear duration invariants（LDI） form an important class of duration calculus formulae， which can be used to describe duration properties of real-time systems. The research on verification algorithms of LDIs has profound theoretical significance and extensive applied value. The literature[3] has proposed a verification algorithm which needs to introduce O（b） auxiliary variables when verifying some formulae. This will strongly restrict its application in practical industrial fields. To solve this problem， this paper presents a novel idea which firstly reverses the original system into its backward version and then verifies the corresponding backward formulae over it. And this doesn’t change the original verification result and only needs to introduce O（1） variables， which greatly extends the scope of industrial application of the algorithm proposed in [3]. 【Key words】Formal verification； Timed automata； Linear duration invariants； Backward system 0 引言 形式化验证是一种较为常用的提高系统可靠性和正确性的技术，它是形式化方法的一个研究分支。所谓形式化方法，是以数学为基础，用于对系统进行规约和验证的语言、技术和工具等的总称[1]。 线性时段不变式（Linear Duration Invariants， LDI）是一类重要的时段演算公式，由周巢尘等人于1994年提出[2]，可以表示为：a≤l≤b？圯∑■c■■s≤M。■s表示在对于系统观察的区间[tstart，tend]上，系统处于状态s的累计时间。该线性时段不变式表示若观察时长l满足约束：a≤l≤b，则在该区间上系统驻留各状态的累计时间满足线性约束：∑■c■■s≤M。 文献[3]提出了一种高效算法，在标准离散时间语义下，验证扩展的线性时段不变式（Extended Linear Duration Invariants， ELDI）。在某些情况下，验证需要引入O（b）个辅助变量。而在实际工业应用中，b作为观察时长上限，通常是一个很大的值。这会导致验证所需变量数急剧增长，在一定程度上限制了该算法在工业领域的应用范围。 针对该问题，本文提出了一种新颖的解决思路，通过在反向系统上验证对应的公式，可将验证所需变量数从O（b）个减少到O（1）个，使文献[3]所提算法在工业领域得到更广泛运用。 1 E