楊蕊鴻

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

關(guān)鍵詞：模型檢驗(yàn)；時(shí)間自動(dòng)機(jī)；連續(xù)時(shí)段演算；切變

中圖分類號(hào)：TP311 文獻(xiàn)標(biāo)識(shí)碼：A 文章編號(hào)：1009-3044（2016）28-0109-03

1緒論

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

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

2 基礎(chǔ)理論

2.1 時(shí)段演算

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

2.2擴(kuò)展線性時(shí)段不變式

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

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

2.3 時(shí)間自動(dòng)機(jī)

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

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

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

3時(shí)段演算的模型檢驗(yàn)

對(duì)于時(shí)間自動(dòng)機(jī)，其模型檢驗(yàn)的步驟如下：

1） 找出時(shí)間自動(dòng)機(jī)在檢驗(yàn)時(shí)間區(qū)間[]的所有運(yùn)行路徑；

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

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

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

現(xiàn)給出待檢驗(yàn)的自動(dòng)機(jī)及ELDI性質(zhì)，具體說(shuō)明檢驗(yàn)過(guò)程：

ELDI性質(zhì)：

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

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

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

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

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

以上述檢驗(yàn)過(guò)程為例，通過(guò)將時(shí)間自動(dòng)機(jī)的所有時(shí)間約束擴(kuò)大3倍，同時(shí)ELDI中的觀測(cè)時(shí)長(zhǎng)也變?yōu)?倍，即可得到單位為原自動(dòng)機(jī)1/3長(zhǎng)度的遷移路徑，如一條路徑：，其時(shí)間約束都乘以3倍后得到的遷移路徑長(zhǎng)度為6，對(duì)應(yīng)的該路徑可能變?yōu)椋?。由于此時(shí)該路徑的時(shí)長(zhǎng)為6，對(duì)于該自動(dòng)機(jī)則產(chǎn)生了新的路徑，如，不難理解該條路徑等價(jià)于原來(lái)的。同時(shí)由于觀測(cè)時(shí)長(zhǎng)也擴(kuò)大了3倍，在給定的觀測(cè)時(shí)長(zhǎng)為6的情況下，則產(chǎn)生了多個(gè)連續(xù)的切變點(diǎn)。通過(guò)這種方式可以討論一些連續(xù)遷移路徑和連續(xù)切變點(diǎn)的情況。

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

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

4實(shí)驗(yàn)分析與結(jié)論

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

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

參考文獻(xiàn)：

[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] 李曉山， 周巢塵.時(shí)段演算綜述[J].計(jì)算機(jī)學(xué)報(bào)， 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.