楊蕊鴻

摘要：模型檢驗是一種對有限狀態(tài)系統(tǒng)的性質(zhì)進行自動檢驗的技術(shù)，能夠?qū)ο到y(tǒng)設(shè)計的正確性進行驗證。線性時段不變式是一類重要的時段演算公式，它用來描述實時系統(tǒng)的安全性質(zhì)。而擴展線性時段不變式通過命題邏輯和“切變”運算對線性時段不變式進行了擴展，是更有表達力的時段演算公式。由于擴展線性時段不變式不能通過其離散語義下的滿足性來等價于其連續(xù)語義下的滿足性，離散時間下的模型檢驗算法并不適用于連續(xù)時間的情況，因此研究連續(xù)時間下擴展線性時段不變式的模型檢驗方法對于實時系統(tǒng)的性質(zhì)檢驗具有重要的實用意義。該文提出了連續(xù)時間下針對擴展線性時段不變式的有界模型檢驗算法，根據(jù)離散化方法將連續(xù)時間下的問題轉(zhuǎn)化為離散情況，通過迭代地調(diào)用離散時間下線性時段不變式的有界模型檢驗算法，來解決研究的問題。實驗表明，該文提出的算法能夠有效地對連續(xù)時間下的擴展線性時段不變式進行有界模型檢驗。

關(guān)鍵詞：模型檢驗；時間自動機；連續(xù)時段演算；切變

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

1緒論

隨著計算機技術(shù)的飛速發(fā)展，軟件系統(tǒng)日趨復雜，計算機系統(tǒng)的規(guī)模和復雜性與日俱增，系統(tǒng)潛在的任何問題都可能引發(fā)嚴重的后果。因此，如何在系統(tǒng)開發(fā)早期階段驗證設(shè)計的正確性和可靠性，成為軟件工程領(lǐng)域研究的重點課題。形式化方法（FormalMethod）是一種用于提高系統(tǒng)可靠性和安全性的重要方法。模型檢驗（Model Checking）[1]是形式化方法的重要組成部分，它是一種自動驗證有窮狀態(tài)系統(tǒng)的技術(shù)。時段演算（Duration Calculus）[2]是一種區(qū)間時態(tài)邏輯，用于表示系統(tǒng)在區(qū)間上的性質(zhì)。線性時段不變式和擴展線性時段不變式都是重要的時段演算表達式。

本文提出了一種針對連續(xù)時態(tài)語義下由擴展線性時段不變式描述的系統(tǒng)性質(zhì)的模型檢驗方法。該方法主要基于模型檢驗工具UPPAAL完成。主要思想是將連續(xù)語義下的時段演算的模型檢驗轉(zhuǎn)化為離散語義下的模型檢驗，基于離散語義下的時段演算方法[3]，對其進行轉(zhuǎn)化和改造，形成連續(xù)時段演算的模型檢驗方法。

2 基礎(chǔ)理論

2.1 時段演算

時段演算是一種區(qū)間時序邏輯，它將布爾函數(shù)在區(qū)間上的積分進行形式化，用來表述和推理實時系統(tǒng)的定量性質(zhì)。線性時段不變式是一類重要的時段演算公式，實時系統(tǒng)中的許多安全性質(zhì)都可以用線性時段不變式進行規(guī)約。而擴展的線性時段不變式是對于線性時段不變式的擴展，它是更具有表達力的時段演算公式，因此本文主要以擴展線性時段不變式為研究對象進行論述。

2.2擴展線性時段不變式

擴展線性時段不變式（Extended Linear Duration Invariants，ELDI）[4]是對普通線性時段不變式在切變（chop，符號；）語義上擴展形成的，形如ELDI，它表示從初始時間0時刻開始，對系統(tǒng)進行觀測，當觀測時長在[]區(qū)間內(nèi)時，要求系統(tǒng)處于某個狀態(tài)的累積時間長度滿足，其中、、、為實數(shù)，為系統(tǒng)狀態(tài)，則該系統(tǒng)滿足性質(zhì)。ProCos項目中的一個著名研究實例就是對煤氣燃燒器的需求進行形式化表述，比如對于需求：“如果對煤氣燃燒器的觀察時長大于等于60秒，則燃氣泄露時長不會超過整個觀察時長的二十分之一”，即可使用ELDI來形式化地規(guī)約：這里的是一個布爾函數(shù)，它表示煤氣燃燒器是否處于漏氣狀態(tài)。注意，這里對該煤氣燃燒器的觀察是一個封閉區(qū)間。

此外，還有一種經(jīng)過chop（）語義擴展的ELDI，形如，其中。對于chop語義的理解如下，。即在觀測時段范圍內(nèi)，存在一個點m使得性質(zhì)在的時段內(nèi)成立，而性質(zhì)在的時段內(nèi)成立，如圖1所示。

2.3 時間自動機

時間自動機（Timed Automata）[5]理論是實時系統(tǒng)最常用的表示模型，它所建立的模型用于描述時間系統(tǒng)的行為，它作為有限時間自動機的時間擴展，在其基礎(chǔ)上增加了時間變量和約束條件。時間自動機使用有限數(shù)量的變量來表示時間，稱為時間變量；同時用一個約束條件來注釋狀態(tài)轉(zhuǎn)換圖，用于決定狀態(tài)轉(zhuǎn)換發(fā)生的時間限制，也稱為時間約束。對于具有時間行為的系統(tǒng)，如實時系統(tǒng)等，時間自動機可被用來對其行為進行建模和分析，進一步檢驗系統(tǒng)的性質(zhì)。

在對時間自動機進行性質(zhì)規(guī)約的模型檢驗時，有時會引入離散時間語義作為背景，表示驗證過程只考慮該時間自動機的整數(shù)行為，簡稱為離散時間自動機；相反，連續(xù)時間語義下的驗證過程中，我們簡稱時間自動機為連續(xù)時間自動機。

時間自動機從一個狀態(tài)到另一個狀態(tài)的轉(zhuǎn)換稱為遷移。模型檢驗通過時間自動機的遷移路徑對驗證性質(zhì)的滿足性進行判定，對于時間自動機，滿足ELDI性質(zhì)的條件是的所有遷移路徑滿足，即。對于任意不滿足性質(zhì)的自動機，能且至少能夠找到一條不滿足待檢驗性質(zhì)。

3時段演算的模型檢驗

對于時間自動機，其模型檢驗的步驟如下：

1） 找出時間自動機在檢驗時間區(qū)間[]的所有運行路徑；

2） 對于形如，其中，計，確定檢驗范圍內(nèi)潛在的切變點；

3） 對于任意一條遷移路徑，計算潛在切變點下的可能取值組合，滿足所有的切變點即為有效切變點；

4） 討論有效切變點下內(nèi)所有遷移路徑，若所有路徑都滿足性質(zhì)，則表明該自動機能夠找到滿足性質(zhì)的切變點，即自動機滿足性質(zhì)。

現(xiàn)給出待檢驗的自動機及ELDI性質(zhì)，具體說明檢驗過程：

ELDI性質(zhì)：

該性質(zhì)表示，從任意時刻為初始時刻對系統(tǒng)進行觀測，當觀測時長為2時，要求尋找到一時間點，使得時段內(nèi)系統(tǒng)滿足，其中。以初始觀測時刻為0為例，在觀測時長為2的情況下，能夠找到的離散切變點可能有3個，0，1和2，而可能的連續(xù)切變點則為無數(shù)個。

因此可以得出結(jié)論，在離散語義下，該自動機不滿足性質(zhì)，即。

然而對于實際運行狀態(tài)下的系統(tǒng)，時間并非簡單的離散值，更有可能是連續(xù)值，因此對于離散語義下的模型檢驗結(jié)果并不能完全代表系統(tǒng)的檢驗結(jié)果，對于連續(xù)語義下的模型檢驗更有必要。

在連續(xù)語義下，自動機的時鐘變量和遷移時刻均有可能是連續(xù)值，而切變點也可能是連續(xù)值，因此首先定性地分析離散之間自動機對連續(xù)ELDI性質(zhì)的模型檢驗，即是否能夠找到連續(xù)的切變點，使得所有離散的遷移路徑能夠滿足性質(zhì)。

由于模型檢驗工具僅支持時間約束和時間變量為整數(shù)的檢驗，通過離散化和微積分的思想可以用有限的若干離散值表示無限的連續(xù)值的情況，具體可以改變時間自動機中的時間約束和ELDI的系數(shù)，改造出若干連續(xù)點。

以上述檢驗過程為例，通過將時間自動機的所有時間約束擴大3倍，同時ELDI中的觀測時長也變?yōu)?倍，即可得到單位為原自動機1/3長度的遷移路徑，如一條路徑：，其時間約束都乘以3倍后得到的遷移路徑長度為6，對應的該路徑可能變?yōu)椋骸Ｓ捎诖藭r該路徑的時長為6，對于該自動機則產(chǎn)生了新的路徑，如，不難理解該條路徑等價于原來的。同時由于觀測時長也擴大了3倍，在給定的觀測時長為6的情況下，則產(chǎn)生了多個連續(xù)的切變點。通過這種方式可以討論一些連續(xù)遷移路徑和連續(xù)切變點的情況。

根據(jù)計算，在此情況下，起始時刻3個時間單位后的點為切變點，此時所有路徑均滿足該切變點，即存在實際切變點1.5，使得該自動機滿足ELDI性質(zhì)

因此，在該計算方法下，能夠找到使得系統(tǒng)滿足的連續(xù)切變點，即實驗證明：。

4實驗分析與結(jié)論

在實驗中，我們發(fā)現(xiàn)該方法能夠解決一部分連續(xù)時段演算的模型檢驗要求，對單切變點和多切變點情況均適用，并得出較離散語義下更為準確的檢驗結(jié)果，為一部分離散模型檢驗下不滿足的系統(tǒng)找到能夠滿足性質(zhì)的連續(xù)切變點。然而對于另一部分仍無法找到連續(xù)切變點的時間自動機，需要進行嚴格的語義規(guī)約及定性檢驗，僅對一部分單切變點的模型檢驗找到連續(xù)遷移路徑下的離散規(guī)約方法，并進行檢驗。

從實際工程應用的角度來說，連續(xù)時段演算下的模型檢驗在工程上具有重要的意義。它保證了實際應用中相關(guān)具有連續(xù)性的機械設(shè)備、通信協(xié)議等系統(tǒng)在時間規(guī)約性質(zhì)上的準確性和可靠性，對驗證具有連續(xù)時間意義的性質(zhì)的系統(tǒng)驗證研究具有實際意義。

參考文獻：

[1] Edmund M Clarke， Orna Grumberg， Doron A Peled. Model Checking[M]. The MIT Press， 1999.

[2] Chaochen Zhou. Linear duration invariants[C]. In FTRTFT 1994， 1994： 86–109.

[3] Zu Q， Zhang M， Zhu J， et al. Bounded model-checking of discrete duration calculus[C]//Proceedings of the 16th international conference on Hybrid systems： computation and control. ACM， 2013： 213-222.

[4] 李曉山， 周巢塵.時段演算綜述[J].計算機學報， 1994，17（11）： 842-851.

[5] Rajeev Alur ，David L Dill. A theory of timed automata[C]. Theoretical Computer Science， 126（2）：183–235， 1994.