連續時段演算的模型檢驗

楊蕊鴻

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

關鍵詞：模型檢驗；時間自動機；連續時段演算；切變

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

1緒論

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

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

2 基礎理論

2.1 時段演算

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

2.2擴展線性時段不變式

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

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

2.3 時間自動機

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

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

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

3時段演算的模型檢驗

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

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

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

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

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

現給出待檢驗的自動機及ELDI性質，具體說明檢驗過程：

ELDI性質：

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

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

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

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

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

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

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

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

4實驗分析與結論

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

從實際工程應用的角度來說，連續時段演算下的模型檢驗在工程上具有重要的意義。它保證了實際應用中相關具有連續性的機械設備、通信協議等系統在時間規約性質上的準確性和可靠性，對驗證具有連續時間意義的性質的系統驗證研究具有實際意義。

參考文獻：

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