一類線性時段不變式的驗證優(yōu)化與實現(xiàn)

胡棐禹

摘要：線性時段不變式是一類重要的時段演算公式。文獻[1]中提出一種驗證算法，能夠針對以時間自動機建模的系統(tǒng)，模型檢驗其是否滿足一個擴展的線性時段不變式。在驗證一類特定公式時，該算法需要引入O（b）個輔助變量，且需全程保留它們的值，會導致檢驗這類公式所需的變量數(shù)和復雜度急劇增長。該文提出一種基于系統(tǒng)反轉(zhuǎn)的模型檢驗方法，并為線性時段不變式的模型檢驗問題提供一種全新的解決思路

關鍵詞：模型檢驗；時間自動機；線性時段不變式；切變；反向系統(tǒng)

中圖分類號：TP311 文獻標識碼：A 文章編號：1009-3044（2016）03-0071-02

1 背景

在某些實時系統(tǒng)中，如航空交管系統(tǒng)、化工廠控制系統(tǒng)等，任何錯誤都可能造成重大經(jīng)濟損失和人員傷亡。顯然，這類安全攸關系統(tǒng)對設計正確性的要求極其嚴格。如何在系統(tǒng)開發(fā)的早期階段驗證設計的正確性，成為研發(fā)人員必須面對的問題。

2 相關概念與術語

2.1 實時系統(tǒng)的形式化模型

近些年來許多不同的實時系統(tǒng)模型被提出。其中，R Alur等人提出的時間自動機（Timed Automata）已成為標準。時間自動機是在有窮狀態(tài)自動機的基礎上擴充了一個時鐘變量集合X得到的。

2.2 實時系統(tǒng)的時段性質(zhì)與線性時段不變式

線性時段不變式是實時系統(tǒng)的一類重要性質(zhì)，由周巢塵等人1994年首次提出。它可用時段演算公式表示，形如：

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

意思是若觀察區(qū)間[b，e]的長度滿足約束：[A≤e-b≤B]，則在該區(qū)間上系統(tǒng)處于各個狀態(tài)的累計時間就滿足線性約束。

2.3 帶切變的線性時段不變式及其模型檢驗

時段演算的一個主要運算符是“切變（chop）”，用；表示。公式 B；C

含義是 B；C 在區(qū)間 [b， e] 上成立，當且僅當區(qū)間可以被切成兩個子區(qū)間，使得B在第一個區(qū)間上成立，C 在第二個區(qū)間上成立。切變是個連接運算，它能通過組裝幾個子區(qū)間上的性質(zhì)，來刻畫整個系統(tǒng)在觀察區(qū)間上的性質(zhì)。定義帶切變的線性時段不變式的基本形式為[A≤e-b≤B?P1，P2]

2.4 離散時段演算的有界模型檢測

定義2.4（PCP、OPCP）

給出一個ELDI表達式和時間區(qū)間[t1，t2]，對于該區(qū)間中的一個整數(shù)時間時刻t，若[φ']在子區(qū)間[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]在區(qū)間[b，e]上的取值，那么在時刻[t']，稱時刻t是關于[dk]的最優(yōu)潛在切變點（OPCP）。也是就說，在時刻[t']，根據(jù)時刻t算得的比根據(jù)之前[dk]所有其他PCP算得的[dk]都要小。

并非任何形式的ELDI表達式都能使用基于OPCP的思想來簡化驗證過程。當ELDI表達式中存在切變運算符直接作用于交、非運算符的情況時，就不能運用這種想法。比如：對于[D1；（D2∧D3）]，可能發(fā)生時間區(qū)間中的所有PCP均非OPCP的情形。因為當前時刻的OPCP需同時考慮d2、d3的取值，而不像上述定義中只需考慮d2或d3的取值。

3 結(jié)束語

3.1 帶切邊的線性時段不變式的反向驗證

上節(jié)提出了一種用于驗證擴展的線性時段不變的算法。在驗證ELDI公式時，該算法需引入2b+3個變量，且需全程保留它們的值，以便實時運用、更新和重置。

根據(jù)線性時段公式[dk]的定義，可知：在一個觀察區(qū)間上，[dk]的真假只與系統(tǒng)A駐留各個位置的時長有關，與它駐留這些位置的先后次序無關。那么，可以得出以下結(jié)論：檢驗A的一個行為是否滿足ELDI公式，等價于檢驗系統(tǒng)A的反向行為是否滿足反向公式，

該方法主要包含三步：

1）對系統(tǒng)模型進行反轉(zhuǎn)操作，得到對應的反向系統(tǒng)，使反向系統(tǒng)恰好體現(xiàn)正向系統(tǒng)中所有被檢驗行為；

2）對ELDI公式進行反轉(zhuǎn)，得到對應的反向公式；

3）檢驗原系統(tǒng)模型對原公式的滿足性，這等價于檢驗反向系統(tǒng)對反向公式的滿足性。

通過這種反轉(zhuǎn)方法，有效降低驗證所需的復雜度，并為線性時段不變式的模型檢驗提供一種全新的思路。。

參考文獻：

[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.