結合關注事件的時間自動機語言包含模型檢測

王 婷,蘇 琪,陳鐵明

(浙江工業大學 計算機科學與技術學院,杭州 310023)

1 引 言

由Alur等人提出的時間自動機[1]在實時系統的建模和驗證分析領域是最重要的模型之一.時間自動機的語言包含問題被描述為,給定兩個時間自動機M和N,其中M為系統模型,N為規約模型(即系統需要滿足的屬性),檢查M的時間自動機語言是否包含于N的語言.時間自動機語言包含驗證[2]的主要目的是檢查系統模型和規約模型(表達系統需要滿足的屬性)是否存在語言包含關系,即系統行為是否滿足某種屬性,包括該屬性蘊含的時間要求.已經有一些工作將時間自動機相關理論和方法用于實時系統,例如對物聯網系統[3]、網絡系統控制器[4]、認知機器人系統[5]等的建模和驗證,然而大部分方法采用可達性(Reachability)驗證、基于時間時序邏輯(例如TLTL[6]、TCTL[7])的驗證等方式,目前還沒有完善的基于語言包含驗證的方法,以應用于實際系統.

由于時間自動機運行時的時間點的無窮性,并不能直接對其進行狀態空間搜索.我們之前的工作[2]首次給出了基于時間域抽象(Zone Abstraction)的方法來解決語言包含問題.該方法對無窮時間點進行時間域抽象,求解兩個時間自動機的同步積(即狀態空間的展開),并將語言包含問題轉化成了同步積的可達性問題.然而在實際問題中,系統模型包含大量可能發生的事件,而屬性模型一般只需要關注少數幾個事件的順序和時間性.倘若由于語言包含的定義,屬性模型必須具有和系統模型同樣的事件集合,則會給屬性模型的建立帶來很大困難.另一方面,通常開發或者測試人員并不熟悉形式化的建模方式,使用時間自動機詳細描述驗證屬性具有一定困難.而為了驗證系統正確性及可靠性,模型檢查工具必須要以系統和驗證屬性作為輸入.因此,屬性模式[8，9]可以用于彌補相關人員和模型檢查工具之間的缺口.

圍繞上述背景,本文首先在文獻[2]的基礎上,給出了改進的時間自動機語言包含算法,屬性建模時只需考慮關注的事件,簡化了屬性模型,并且總結了幾種常用的時間自動機描述的屬性模式,從而能夠指導相關人員編寫系統需要滿足的屬性.由于實踐中大部分常用的屬性復雜度不會很高,并且根據屬性模式建立的屬性都是可確定化的,該算法具備了較好的實際應用價值.此外,本文還將提出的算法應用于水位控制系統[10]的建模及驗證中,并得出了有效結論.

本文章節安排如下.第2節給出時間自動機相關背景知識.第3節詳細介紹了時間自動機語言包含驗證算法并總結了時間自動機驗證常用的屬性模式.第4節以水位控制系統為例,應用算法檢測系統的一些重要屬性.最后是全文總結和未來工作.

2 時間自動機背景

首先給出時間自動機相關定義[1,2].設C為一個時鐘集合,Φ(C)表示時鐘約束集合.每一個時鐘約束定義如下:d:=true|x～n|d1∧d2|d1,其中～∈{=,≤,≥,<,>},x是時鐘集合C中的一個時鐘,n是一個非負整數.由符號～∈{≤,<}可以獲得下行的時鐘約束,用Φ≤,<(C)表示.基于C的一個時鐘賦值v是指為C中的每個時鐘賦予一個實數值.如果v的時鐘賦值使得時間約束δ的布爾值為真,則稱v滿足基于C的一個時間約束δ.對任意d∈R+,令v+d代表時鐘賦值v′,使得對所有c∈C都滿足v′(c)=v(c)+d.令X代表被重置的時鐘集合,[X|→0]v表示所有t∈X都被賦值為零,且其他滿足t∈C和t?X的時鐘值仍與v相同.

定義1.(時間自動機)時間自動機是一個六元組A=(S,Init,S,C,L,T),其中S是有窮狀態集合;Init?S是初始狀態集合;Σ是事件集合;C是有窮時鐘集合;L:S→Φ≤,<(C)為將狀態映射到狀態不變式的函數;T?S×Σ×Φ(C)×2C×S為帶時間約束的轉移關系.

基于時間自動機A運行的具體語義,其每個節點是一個(s,v)形式的對,其中s∈S是一個狀態,v是一個滿足vL(s)的時鐘值.A的運行是一個有窮序列Δ=<(s0,v0),(d0,e0),(s1,v1),(d1,e1),…,(si,vi),(di,ei),…>,其中s0∈Init;v0將時鐘重置為0;對于所有i≥0都有(si,ei,δ,X,si+1)∈T,使得vi+diL(si),vi+diδ,vi+1=[X0](vi+di)和vi+1L(si+1).給定一個Δ,可以得到其時間語言<(d0,e0),(d1,e1),…,(di,ei),…>.我們用Lan(A)表示所有時間自動機A中的語言.如果兩個時間自動機的語言是相同的,那么這兩個時間自動機是等價的.

時間域抽象[2](Zone Abstraction)是目前最常用的抽象技術.時間自動機經過時間域抽象后得到一個有窮狀態的時間域圖(Zone Graph).

一個時間域是由定義在C上的簡單線性不等式或線性不等式的合取式結合組成,例如x-y≤5,y>3∧x<7等,其中x,y∈C.給定一個時間域δ,用δ↑表示從δ經過任意時間后得到的時間域.

圖1 智能燈控的時間自動機模型Fig.1 Timed automaton model of intelligent light control

圖1為一個智能燈控系統的時間自動機模型,系統的初始狀態為Off,智能燈有Light和Bright兩種光線強度.初始狀態下,事件Press發生后,系統跳轉到狀態Light,時鐘x重置后開始計時.如果在3個時鐘單位內,事件Press再次發生,系統狀態由Light跳轉到Bright,如果超出3個時鐘單位,由于Light上沒有狀態不變式,系統可以一直停留在該狀態,或者經由事件Press跳轉回Off狀態.除上圖中的表達,本文的系統模型還包括如下約定:

1)常量和變量:常量是在模型運行時不會被修改的量,表示如#define A 3,即定義常量A的值為3;變量能夠被修改,表示如var B:{0..10}=7,即定義變量B,其初始值為7,取值范圍為0到10.

2)信道事件(channel):表示不同進程間發送或接收消息,假設c為信道名,c!表示發送消息,c？表示接收消息[11].

3)轉移:其完整表示為,Clock:<時鐘約束> [轉移條件]事件{操作} Clockreset:{時鐘}.在時鐘變量滿足時鐘約束及系統變量滿足轉移條件的情況下,可以執行事件.事件執行的同時可以發生一些操作,例如改變變量值.Clockreset表示將{}內的時鐘重置為零.

3 時間自動機語言包含驗證算法

時間自動機語言包含問題定義如下:給定時間自動機M和N,如果Lan(M)?Lan(N),那么語言包含成立.我們之前的工作[2]給出了基于時間域抽象(Zone Abstraction)的方法,利用時間域抽象技術,求解兩個時間自動機的同步積(即狀態空間),并將語言包含問題轉化成了同步積上的可達性問題.然而在實際問題中,雖然系統模型和屬性模型都為時間自動機,但是系統模型往往包含大量可能發生的事件,而屬性模型一般只關注某幾個事件的順序和時間性.因此,我們對該方法進行了改進,使得其在驗證時只需考慮關注事件,具體步驟如下.

3.1 驗證預處理

根據時間自動機的定義,狀態上可存在狀態不變式.為了便于同步積上可達狀態的搜索,我們首先將時間自動機轉換為等價的沒有狀態不變式的自動機,而不改變其語言[2].該轉化將狀態的狀態不變式移動到該狀態的進入和離開的轉移上.給定一個時間自動機A=(S,Init,∑,C,L,T),對于任意狀態s∈S以及其上的狀態不變式L(s),滿足:

1)如果(s,e,δ,X,s′)是一個從狀態s離開的轉移,則將L(s)移動到轉移(s,e,δ,X,s′)中,即將其變為(s,e,δ∧L(s),X,s′);

2)如果(s′,e,δ,X,s)是一個進入狀態s的轉移,對于任意L(s)中的x～n(其中～∈{≤,<},n任意正整數),若x?X,則將x～n與δ合取,否則忽略該x～n.

給定兩個時間自動機M=(Sm,Initm,∑m,Cm,Lm,Tm)和N=(Sn,Initn,∑n,Cn,Ln,Tn).其中N已將狀態不變式進行轉換(M不需要進行此操作).

3.2 基于時間域抽象的同步積

接下來,給定任意節點node=(sm,Xn,δ),通過給出對于非關注事件及關注事件的后續節點的生成步驟來定義T.

b)由于需要將N進行確定化,Tran(e,Xn)中所有轉移的時間約束必須是互斥的.用Exclusive(e,Xn)表示互斥的時間約束集合,集合中每個元素都是一個時間約束.Tran(e,Xn)中的每個轉移上的時間約束或取其本身,或取其的否定,然后進行合取.因此,生成的集合Exclusive(e,Xn)中的時間約束一定是互斥的.對于Exclusive(e,Xn)中的每個時間約束,其由所有Tran(e,Xn)中轉移上的時間約束本身或其否定組成,如果某個轉移并未取否定,則該轉移是會發生的.

定理1.Lan(M)?Lan(N)成立,當且僅當Zone(M?N)中不存在可達狀態(sm,φ,δ),使得δ為真.

圖2的例子完整說明了我們提出的方法如何分步進行.圖中M為系統模型,其中h為非關注事件,a為關注事件.N為屬性模型,右側Zone(M?N)為時間域圖,其初始節點為node0=(m1,{(n1,y)},0≤x=y0).

node1為node0經過事件h的后續節點,m1經過事件h后依然處于m1.由于h為非關注事件,N此時并不需要運行,因此node1中的(n1,y0)與node0相同.時間約束經過條件x>2為2≤x=y0.(步驟1))

當M執行m1到m2的轉移,時鐘條件為x>3,事件a為關注事件.對于node0中的(n1,y0),基于事件a有兩個從n1離開的轉移,其時鐘條件分別是y>7和y> 3.y的初始活躍時鐘是y0,因此將轉移((n1,y0),a,y0>3,{y0},(n2,R))和((n1,y0),a,y0>7,φ,(n1,y0))添加到Tran(a,(n1,y0)).轉移中的變量將在后續步驟中確定.(步驟 2)中的a))

通過使得時間約束互斥的操作,從Tran(a,(n1,y0))可以得到四個時間約束y0>7∧y0>3,y0>7∧y0≤3,y0≤7∧y0>3和y0≤7∧y0≤3,組成Exclusive(a,(n1,y0)).其中y0>7和37,在N中從n1離開的兩個轉移都可以發生,因此從node0到node2,node2中關聯N的集合中會有兩個元素;而對于3

從node0到node2,對于狀態n1的回到自身的轉移,時鐘y0沒有被重置,因此(n1,y0)在node2中依然為(n1,y0),時鐘y0仍在使用;對于n1到n2的轉移,時鐘y0被重置,但由于y0在(n1,y0)中需要繼續被使用,所以在node2的(n2,y1)中啟用新時鐘y1(當前R=y1).從node0到node3,只有n1到n2的轉移可行,那么可以在node3中重新使用時鐘y0.node2和node3中的時間約束是通過node0的初始時間約束、轉移時鐘條件以及重置時鐘情況計算出來的.至此,node0的后續節點構建完畢.(步驟 2)中的c))

圖2 基于時間域抽象的同步積Fig.2 Synchronous product based on zone abstraction

對于到達每個節點時語言包含是否成立的判斷,舉例來說,node0的Exclusive(a,(n1,y0))中的negAll是y0≤3.0≤x=y0(node0的時間約束),x>3和negAll組合的結果不為真,因此從node0無法生成形如(sm,φ,δ)的節點,其他節點也同樣處理(在此例中,M和N的語言包含成立).

3.3 時間自動機語言包含驗證算法

算法1.時間自動機語言包含驗證算法

輸入:時間自動機M和N

輸出:驗證結果(true或者false)

1.working:=Init;

2.done:=?;

3. whileworking≠? do

4. removenode=(sm,Xn,δ) formworking;

5. addnodeintodone;

6. ifXn=? then

7. return false;

8. end if

10. ife∈Σm∧e?Σnthen

11. addsucc1(node,Zone(M?N)) intoworking;

12. else ife∈Σm∧e∈Σnthen

15. end for

16. end if

17. end for

18.end while

19.return true;

算法1為我們提出的時間自動機語言包含驗證算法.算法中有兩個數據結構,working存儲時間域圖Zone(M?N)中待搜索的節點,done存儲已經搜索過的節點,working的初始值為Zone(M?N)的初始狀態,done為空集.在從第3行到第18行的循環中,每次將當前節點從working中刪除隨后添加到done,并且對該節點進行判斷(第6行),如果是違反語言包含的節點,則在第7行返回false.第9行到17行判斷當前節點的轉移事件是否為非關注事件并進行對應操作,若事件e只屬于M的事件集合Σm即為非關注事件,則將succ1(node,Zone(M?N))的節點加入working;若事件e既屬于Σm也屬于Σn,則將succ2(node,Zone(M?N))中的所有節點加入working.最后,如果搜索完所有狀態都沒有找到違反語言包含的節點,則兩個時間自動機是語言包含成立,此時working為空,并在第19行返回true.

3.4 基于時間自動機的屬性模式

屬性模式的建立使用戶能夠更好地編寫出用于自動化模型檢查的形式化規范.當前已有研究中的屬性模式可以推斷事件的發生與否,也能夠描述與時間相關的事件發生順序等邏輯行為[8].然而對于本文中帶有狀態不變式的時間自動機,尚沒有總結出完整的屬性模式.

基于時間自動機的屬性模式如圖3所示,其中a、b、c為事件;x為時鐘變量,k為任意正整數.基本的屬性模式均為單一時鐘變量的時間自動機.實際問題中的驗證屬性也可以多種模式或者其變體的并行組合,并且可以有多個時鐘.文中屬性模式的狀態上包含的狀態不變式,表示系統必須在規定時間離開該狀態.以下詳細介紹對各個屬性模式:

應答屬性模式(response),即系統要滿足事件b總是緊跟在事件a之后,并且必須在k個時鐘單位內發生.State_2上的狀態不變式表明了事件b在事件a后發生的必然性.前置屬性模式(precedence)與應答屬性模式的主要區別在于,事件a發生后,并不強制發生事件b,但是事件b一旦發生,必須在事件a之后,且需要滿足一定的時間條件.前置屬性模式1表示事件b的發生與a間隔時鐘至少為k前置屬性模式2表示事件b的發生與a間隔時鐘不超過k.由于自循環轉移中事件a發生后時鐘重置,因此前置屬性模式的計時都從a的最后一次發生開始.

圖3 屬性模式Fig.3 Property patterns

缺失屬性模式(absence)表示系統開始運行后,事件a只能在k個時鐘單位后發生;事件a也可以永遠不發生,即系統一直停留在狀態State_1(State_1上沒有狀態不變式).存在屬性模式(existence)表示系統開始運行后,事件a必須在k個時鐘單位內發生(由于State_2的狀態不變式x≤k,系統無法一直停留在State_2).

鏈(chain)屬性模式表示系統開始運行后,在k個時鐘單位內,事件a、b和c必須順序發生一次.其中三個狀態上的狀態不變式,表示在k單位時間內無論a、b和c如何發生,最終必須離開這該狀態,且到達State_4(處于該狀態說明三個事件已經按照順序發生過一次).

根據[2]所述,3.2節中Zone(M?N)的節點數量可能是無窮的,這是由于某些情況下,在確定化N的過程中,有可能產生無窮多的時鐘,使得狀態持續增長、無法終止.值得慶幸的是,本節的屬性模式都是可以被確定化的,因此利用屬性模式建立的系統被檢測屬性在驗證時并不會產生上述情況.在實際系統的建模和驗證中,大部分屬性都可以套用屬性模式(或者變種),側面反映了我們提出的改進方法的可行性.

4 案例分析

本章以水位控制系統[10]為例,給出我們提出的算法的應用,算法基于模型檢測工具PAT[12]實現.首先使用時間自動機對系統進行建模,其次依據屬性模式給出待驗證屬性的描述,最后得出驗證的結果.該案例建模及驗證均運行于PC(2.71GHz Intel(R)Core(TM)i5-7200 CPU,8.0GB的RAM).

圖4 水位控制系統架構及其系統模型Fig.4 Architecture and models of water level control system

4.1 水位控制系統建模

圖4為水位控制系統架構及其系統模型,圖中1)為水位控制系統架構圖,2)-8)為系統各個組件的時間自動機模型圖.系統日常運行主要包含5個組件:執行器(Actuator)、控制器(CtrlWithAct和CtrlWithCon)、儲蓄池(Heater)、傳感器(Sensor)和組態站(Configuration).儲蓄池的容量為100,蒸發下降1.組態站設置最高(SH=90)和最低(SL=10)的安全水位.控制器確保水位在正常范圍內(L=40<水位SH并且L

#define SH 90; //最高水位值

#define SL 10; //最低水位值

varWL:{0..100}=50;//儲蓄池水位值

varWL_Sen:{0..100}=0; //傳感器存儲的水位值

varWL_Ctrl:{0..100}=0; //控制器存儲的水位值

varH=60;//安全高水位值

varL=40;//安全低水位值

varC=1;//水泵開關控制變量,1表示開,0表示關

channelWLToSen; //發送給傳感器的水位值

channelObtainHL;//獲取安全水位值

channelFalseHL;//錯誤的安全水位值

channelCorrectHL;//正確的安全水位值

channelOffToAct;//閥門關閉

channelOnToAct;//閥門打開

channelWLToCtrl;//發送給控制器器的水位值

4.2 待驗證的屬性描述

根據我們提出的屬性模式,針對水位控制系統模型建立待驗證屬性,如圖5所示,以下進行詳細介紹.

1)驗證屬性Resp用來檢測傳感器接收到水位值消息WLToSen后,能否在一個時鐘單位內將消息WLToCtrl發送給控制器,以保證消息的實時性.其在PAT中的驗證語句為:#assert System refines Resp.

2)驗證屬性Pre驗證語句為:#assert SystemWithAttacker refines Pre.控制器每隔6個時鐘單位檢測當前H>SH和L

3)驗證屬性Existence為屬性模式Existence的變體,其驗證語句為:#assert SystemWithAttacker refines Existence.該屬性驗證系統受到攻擊后能否在不超過6個時鐘單位內發送獲取正確值的消息.

圖5 待驗證屬性的時間自動機模型Fig.5 Timed automaton models of property to be verified

4.3 驗證結果

我們在PAT工具中實現了本文的時間自動機語言包含算法,使用該算法進行模型檢測后的驗證結果數據如表1所示,并可分析出以下結論:

表1 驗證結果數據
Table 1 Data for verification results

屬性驗證結果狀態數轉移數運行時間(秒)Resptrue1842300.01Pretrue36094718367.30Existencetrue33889673756.82

1)如果將Resp屬性的時間約束條件x≤1改為x<1,則驗證結果為假,表明該系統模型中的傳感器能夠在接收到消息后不超過1個時鐘單位發送消息給控制器.

2)若將Pre屬性中的時間約束條件x≤7改為x≤6,則驗證結果為假,表明系統在有攻擊者的情況下,水位正常范圍被篡改之后,最終總是能夠在不超過7個時鐘單位恢復.這一驗證屬性表明系統的恢復機制是有效的.

3)Existence屬性的驗證結果表明系統受到攻擊后,能夠在不超過6個時鐘單位及時獲取正確值.

需要注意的是,本文算法改進的目標在于需要驗證的屬性在建模時不必關注無關事件,從而大大簡化了建模方式.算法在改進前后運行時訪問的狀態空間是一致的,進而訪問的狀態和轉移數量是相同的,因此運行時間和效率也是一致的.

5 結束語

本文對已有的時間自動機語言包含檢測算法進行了優化,只需要關注與驗證相關的事件及其發生先后順序、時間條件等,而不必考慮與驗證屬性無關的事件,簡化了待驗證屬性的建模,并且總結了基于時間自動機的常用屬性模式.此外,本文還以水位控制系統為例,展示了我們提出的方法,包括系統模型、屬性模型和驗證結果.

關于未來工作,一方面將研究時間自動機語言包含算法的優化問題,例如減少狀態空間的方法,性能及運算效率的提高;另一方面繼續探索屬性模式和語言包含算法如何更好地解決實際問題.