李國(guó)拯，高 正

(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 210016)

基于帶數(shù)據(jù)約束實(shí)時(shí)系統(tǒng)的互模擬檢測(cè)方法

李國(guó)拯，高 正

(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 210016)

帶數(shù)據(jù)約束的實(shí)時(shí)系統(tǒng)是指一種既帶有時(shí)間約束又帶有數(shù)據(jù)變量約束的計(jì)算系統(tǒng)，其廣泛存在于航空航天、工業(yè)控制、國(guó)防等安全攸關(guān)系統(tǒng)，并發(fā)揮著至關(guān)重要的作用。針對(duì)這類系統(tǒng)的形式化建模與驗(yàn)證是確保其正確性和可靠性的重要途徑。文中首先研究了組合接口自動(dòng)機(jī)、Z語(yǔ)言、時(shí)間自動(dòng)機(jī)的形式規(guī)范—CT-ZIA，其能同時(shí)描述帶數(shù)據(jù)約束的實(shí)時(shí)系統(tǒng)的時(shí)序行為性質(zhì)和數(shù)據(jù)結(jié)構(gòu)性質(zhì)；其次，為了研究該規(guī)范上的互模擬形式化驗(yàn)證，給出了CT-ZIA上的互模擬關(guān)系定義；然后，為了互模擬算法的可判定性，對(duì)CT-ZIA中的時(shí)鐘進(jìn)行等價(jià)劃分，提出了有限論域CT-ZIA的定義；最后，基于有限論域CT-ZIA模型，給出了其上互模擬檢測(cè)算法，并說(shuō)明其正確性。

實(shí)時(shí)系統(tǒng)；接口自動(dòng)機(jī)；Z語(yǔ)言；時(shí)間自動(dòng)機(jī)；互模擬檢測(cè)

0 引 言

帶數(shù)據(jù)約束的實(shí)時(shí)系統(tǒng)[1]是指一種既帶有時(shí)間約束，又帶有數(shù)據(jù)變量約束的計(jì)算系統(tǒng)。飛行控制、核反應(yīng)堆控制以及鐵路調(diào)度控制等計(jì)算機(jī)控制系統(tǒng)都屬于帶數(shù)據(jù)約束的實(shí)時(shí)系統(tǒng)。這些系統(tǒng)中許多動(dòng)作的完成都與時(shí)間相關(guān)，即要滿足一定的時(shí)間限制，如某個(gè)動(dòng)作要在一秒鐘內(nèi)完成；同時(shí)這些系統(tǒng)中數(shù)據(jù)變量之間也有一定的約束關(guān)系，如飛機(jī)的飛行速度可能跟氣壓、溫度等有一定的約束關(guān)系。單一的規(guī)范技術(shù)很難適合這樣的應(yīng)用場(chǎng)景，所以這就要求利用多種能夠描述系統(tǒng)行為各個(gè)方面的專門(mén)技術(shù)?；谶@一想法，在文獻(xiàn)[2]中提出了組合接口自動(dòng)機(jī)、時(shí)間自動(dòng)機(jī)和Z語(yǔ)言的形式規(guī)范。

接口自動(dòng)機(jī)(Interface Automata)[3]是一種輕量級(jí)的基于自動(dòng)機(jī)語(yǔ)言的組件規(guī)范語(yǔ)言，能夠描述基于組件系統(tǒng)中組件及組件間的交互行為。時(shí)間自動(dòng)機(jī)(Timed Automata)[4]是使用最為廣泛的一種描述實(shí)時(shí)系統(tǒng)的數(shù)學(xué)模型，可簡(jiǎn)單看作帶時(shí)鐘變量的有限自動(dòng)機(jī)。Z[5]是基于一階謂詞邏輯和集合論的形式規(guī)格語(yǔ)言。

文中研究了一種組合接口自動(dòng)機(jī)、時(shí)間自動(dòng)機(jī)和Z語(yǔ)言的規(guī)范語(yǔ)言，即CT-ZIA[2]。接口自動(dòng)機(jī)是描述軟件組件接口性質(zhì)的直觀模型，時(shí)間自動(dòng)機(jī)是描述實(shí)時(shí)系統(tǒng)的模型，Z可以描述狀態(tài)的數(shù)據(jù)性質(zhì)以及狀態(tài)的變遷。為了對(duì)復(fù)雜實(shí)時(shí)系統(tǒng)進(jìn)行規(guī)范說(shuō)明，這里簡(jiǎn)單介紹下CT-ZIA的定義，粗略地講，CT-ZIA具有時(shí)間自動(dòng)機(jī)風(fēng)格和特點(diǎn)，但它的狀態(tài)和操作是用Z語(yǔ)言來(lái)描述的。文中進(jìn)一步研究了CT-ZIA上的互模擬關(guān)系，并給出了有限論域CT-ZIA上的互模擬檢測(cè)算法。

1 連續(xù)時(shí)間ZIA規(guī)范

在文獻(xiàn)[2]中，提出了CT-ZIA規(guī)范，并研究其上的模型檢測(cè)[6]問(wèn)題，下面直接給出其定義：

(1)SP是狀態(tài)的集合；

(7)X為時(shí)鐘變量的非負(fù)實(shí)數(shù)有限集合，C(X)為X上時(shí)鐘約束的集合，其語(yǔ)法定義如下：

Φ::=xc|cx|?1∧?2

其中，x∈X；∈{<,≤}；c為非負(fù)有理數(shù)。

(8)映射I：SP→C(X)為每個(gè)狀態(tài)賦以一時(shí)間約束，此約束稱為節(jié)點(diǎn)不變量；

2 CT-ZIAs間的互模擬關(guān)系

互模擬[7-8]是進(jìn)程演算里的一個(gè)十分重要的概念，用來(lái)研究并發(fā)系統(tǒng)行為的一種方法。在軟件系統(tǒng)里，互模擬通常用來(lái)描述抽象規(guī)格說(shuō)明與可執(zhí)行程序代碼的相互轉(zhuǎn)換過(guò)程，所以互模擬關(guān)系的目的在于形式化說(shuō)明相同組件的抽象和具體版本之間的關(guān)系，例如接口的規(guī)范與其實(shí)現(xiàn)之間的關(guān)系。

對(duì)于某個(gè)Z模式A，使用VI(A)代表A中的輸入變量集合，VO(A)代表A中的輸出變量集合，VH(A)表示A中的內(nèi)部變量集合。

為了定義Z模式之間的互模擬關(guān)系，需要如下的符號(hào)。

直觀上，A?B意味著模式A和模式B有相同的輸入變量和相同的輸出變量，并且模式A和模式B的輸入變量范圍和輸出變量范圍一樣。

現(xiàn)在給出Z模式之間的互模擬關(guān)系，其描述了狀態(tài)的數(shù)據(jù)結(jié)構(gòu)屬性間的互模擬關(guān)系。粗略地講，對(duì)于模式A和模式B，說(shuō)A和B是互模擬的，就是兩者的輸入輸出變量一樣，并且兩者的輸入變量范圍和輸出變量范圍也一樣。

定義3：考慮兩個(gè)Z模式A和B，使用符號(hào)A?B，如果

(1)VI(A)=VI(B)，VO(A)=VO(B)；

(2)A(x1,x2,…,xm)?B(y1,y2,…,yn)，其中{x1,x2,…,xm}=V(A)-VI(A)-VO(A)，{y1,y2,…,yn}=V(B)-VI(A)-VO(A)。

接下來(lái)給出CT-ZIAs間的互模擬關(guān)系。對(duì)CT-ZIAs來(lái)說(shuō)，狀態(tài)不僅有數(shù)據(jù)屬性，還有行為屬性。因此，CT-ZIAs間的互模擬關(guān)系既包含數(shù)據(jù)屬性間的互模擬關(guān)系，又包含行為屬性間的互模擬關(guān)系。

定義4：給定一個(gè)CT-ZIAP，定義有序?qū)?s,DP)∈SP×為P在某個(gè)時(shí)刻的狀態(tài)，其中是實(shí)數(shù)集合。下面定義P中的狀態(tài)變遷：

定義5：考慮CT-ZIAP和CT-ZIAQ，稱二元對(duì)稱關(guān)系R?(SP×)×(SQ×)是互模擬關(guān)系，需對(duì)(s,DP)∈SP×，(t,DQ)∈SQ×，(s,DP)R(t,DQ)推出如下條件滿足：

(2)對(duì)于時(shí)延d∈+，如果，那么存在時(shí)延d′∈+，使得以及；并且如果，那么存在時(shí)延d′∈+，使得以及；

3 有限論域CT-ZIA

考慮一個(gè)CT-ZIAP以及其上的狀態(tài)有序?qū)?s,DP)∈SP×，顯然，P是一個(gè)無(wú)限狀態(tài)系統(tǒng)，為了互模擬算法的可判定性，需要首先將無(wú)限狀態(tài)轉(zhuǎn)為有限狀態(tài)。為了獲得CT-ZIA無(wú)限狀態(tài)空間的有限描述，下面給出有限論域CT-ZIA的定義。

Alur，Courcoubetis和Dill在文獻(xiàn)[9-10]中提出一種時(shí)鐘等價(jià)方法，把時(shí)間自動(dòng)機(jī)等價(jià)為域自動(dòng)機(jī)，但是按照Alur時(shí)鐘等價(jià)方法構(gòu)造出的域自動(dòng)機(jī)，存在狀態(tài)空間迅速膨脹爆炸的問(wèn)題。在文獻(xiàn)[2]中，筆者采用一種優(yōu)化的時(shí)鐘等價(jià)方法，并在此基礎(chǔ)上定義了適合于優(yōu)化時(shí)鐘等價(jià)規(guī)則的域自動(dòng)機(jī)，使等價(jià)后的域自動(dòng)機(jī)狀態(tài)數(shù)盡量少[11]，這樣就將CT-ZIA等價(jià)為一種帶Z的域自動(dòng)機(jī)。

大體思想如下：在構(gòu)建時(shí)鐘等價(jià)規(guī)則時(shí)，主要考慮時(shí)鐘關(guān)鍵點(diǎn)的相互比較。例如，對(duì)狀態(tài)s來(lái)說(shuō)，約束條件x≥2中的約束常量2是一個(gè)關(guān)鍵點(diǎn)，對(duì)于x的賦值v(x)來(lái)說(shuō)，當(dāng)v(x)>2或v(x)<2時(shí)，無(wú)論取何值都是不相關(guān)的，所以僅需要考慮約束常量這個(gè)關(guān)鍵點(diǎn)就可以了。

綜上所述，對(duì)時(shí)鐘x而言，可分為三種情況：

(1)v(x)

(2)v(x)=cx則v'(x)=cx；

(3)v(x)>cx則v'(x)>cx。

類似的，對(duì)于y-x的取值范圍，只需要考慮時(shí)鐘關(guān)鍵點(diǎn)的比較。

如上方法將CT-ZIA等價(jià)為一種帶Z的域自動(dòng)機(jī)，下面對(duì)CT-ZIA中Z模式再加以適當(dāng)?shù)募s束，就得到一類特殊的CT-ZIAs，其上的互模擬檢測(cè)算法是可判定的。

定義7:給定一個(gè)Z模式S[v1:T1;…;vm:Tm|P1;…;Pn]，如果模式中的每個(gè)變量vi有有限多可能的值，即變量的類型Ti有有限多元素，那么稱S為有限域Z模式?？紤]一個(gè)，稱其為有限論域CT-ZIA，需滿足如下條件：

4 互模擬檢測(cè)算法

給定一個(gè)CT-ZIAP，可以將P轉(zhuǎn)為等價(jià)的帶Z域自動(dòng)機(jī)，進(jìn)一步約束P中Z模式的變量取值，就得到有限論域CT-ZIA，記為F(P)。這部分給出針對(duì)有限論域CT-ZIAs的互模擬檢測(cè)算法BC。假定F(P)和F(Q)是兩個(gè)有限論域CT-ZIAs，具體算法如下：

BC(P,Q)=

Rp,q:=BCS(p,q)

BCS(p,q)=

return(Bp,q)

elseB:=∧a∈A(p,q)Matcha(p,q)

Matcha∈A(p,q)(p,q)=

return(false)

return(false)

Di,j:=BCS(pi,qj)

return(∧i(∨j(Ca∧Ci,j∧Di,j)))

BCZ(S,T)=

if(VI(S)≠VI(T))or(VO(S)≠VO(T))

thenreturn(false)

else

VT:=V(T)-VI(S)-VO(S)

E:=BCL(SVS,TVT)

return(E)

BCL(M,N)=

TV(LS)=

rewriteschemaLStoanequivalentfirstorderlogicalformulaLF

if(LFisalwaystrueforanyassignmentonvariables)thenreturn(true)

elsereturn(false)

在上面的算法中，如果對(duì)任意賦值LS總是返回true，那么函數(shù)TV(LS)返回true。一般，因?yàn)橐浑A邏輯的重言式問(wèn)題是不可判定的，所以函數(shù)TV(LS)不能被實(shí)現(xiàn)，但是如果只考慮某些可判定的子邏輯，比如，邏輯公式的每個(gè)變量有有限多可能的值，這樣的子邏輯的重言式問(wèn)題就是可判定的。因?yàn)長(zhǎng)S是有限域Z模式，每個(gè)變量?jī)H有有限多的可能的取值。

不難證明上文提出的互模擬檢測(cè)算法的正確性。下面給出上面算法的正確性說(shuō)明：

引理1:算法BCZ(S,T)可以終止，并且是正確的，即算法返回true當(dāng)且僅當(dāng)S?T。

證明：由Z模式的精化關(guān)系定義可得引理1是正確的。

引理2:算法BCS(p,q)可以終止，并且是正確的，即算法返回true,當(dāng)且僅當(dāng)p～q。

證明：函數(shù)BCS(p,q)從有限劃分后的系統(tǒng)初始狀態(tài)有序?qū)?p,q)出發(fā)，通過(guò)匹配從它們出發(fā)的變遷來(lái)檢測(cè)p,q之間的相似性。在遍歷變遷圖的過(guò)程中，算法根據(jù)CT-ZIA的變遷從每個(gè)狀態(tài)有序?qū)Ξa(chǎn)生接下來(lái)的變遷以及狀態(tài)，然后通過(guò)模擬來(lái)匹配變遷，如果匹配成功，算法就進(jìn)入了下一對(duì)狀態(tài)有序?qū)?。函?shù)Matcha在兩個(gè)變遷圖的乘積圖上執(zhí)行深度優(yōu)先的算法，如果一個(gè)狀態(tài)不能匹配另外一個(gè)狀態(tài)的變遷，那么它們間就不是互模擬關(guān)系，函數(shù)返回false，否則返回true。將P和Q進(jìn)行了有限劃分得到有限狀態(tài)系統(tǒng)F(P)和F(Q)，這就保證了僅會(huì)有限次調(diào)用函數(shù)Matcha(p,q)，所以，函數(shù)BCS(P,Q)總是會(huì)終止。

通過(guò)上面的引理，即可得出下面的命題：

命題1:算法BCS(P,Q)可以終止，并且是正確的，即算法返回true當(dāng)且僅當(dāng)P～Q。

5 結(jié)束語(yǔ)

為了研究帶有數(shù)據(jù)約束的實(shí)時(shí)系統(tǒng)，文獻(xiàn)[2]中提出了組合接口自動(dòng)機(jī)、時(shí)間自動(dòng)機(jī)和Z語(yǔ)言三種形式規(guī)范說(shuō)明技術(shù)的模型(CT-ZIA)，研究了其上的模型檢測(cè)問(wèn)題，但是未對(duì)該模型進(jìn)行進(jìn)一步研究；文獻(xiàn)[12]提出了一種基于離散時(shí)間的ZIA規(guī)范，但是基于離散時(shí)間的模型較適用于同步系統(tǒng)；文獻(xiàn)[13]提出了混成ZIA模型，并給出了其上的近似精化關(guān)系定義，由于混成ZIA多數(shù)子集的不可判定性，未給出精化檢測(cè)算法。

文中給出了CT-ZIAs間互模擬關(guān)系的定義，并對(duì)CT-ZIAs中的時(shí)鐘進(jìn)行等價(jià)劃分，給出有限論域CT-ZIA的定義，在其上的互模擬檢測(cè)算法是可以判定的，這對(duì)自動(dòng)化驗(yàn)證組件的規(guī)范與實(shí)現(xiàn)的關(guān)系有重大意義。

[1] 李廣元,唐稚松.帶有時(shí)鐘變量的線性時(shí)序邏輯與實(shí)時(shí)系統(tǒng)驗(yàn)證[J].軟件學(xué)報(bào),2002,13(1):33-41.

[2] 倪水妹,曹子寧,李心磊.帶數(shù)據(jù)約束實(shí)時(shí)系統(tǒng)的模型檢測(cè)[J].計(jì)算機(jī)科學(xué),2014,41(5):254-262.

[3]deAlfaroL,HenzingerTA.Interfaceautomata[C]//ProcofACMSIGSOFTsoftwareengineeringnotes.[s.l.]:ACM,2001:109-120.

[4] Alur R,Dill D L.A theory of timed automata[J].Theoretical Computer Science,1994,126(2):183-235.

[5] Spivey J M.The Z notation:a reference manual[M].UK:Prentice Hall International Ltd,1992.

[6] 戎 玫,張廣泉.模型檢測(cè)新技術(shù)研究[J].計(jì)算機(jī)科學(xué),2003,30(5):102-104.

[7] 朱維軍,劉保羅,周清雷.時(shí)間自動(dòng)機(jī)與信號(hào)自動(dòng)機(jī)的互模擬算法[J].華南理工大學(xué)學(xué)報(bào)：自然科學(xué)版,2008,36(5):38-42.

[8] 李 娜,姚從軍.互模擬的一些基本性質(zhì)[J].云南師范大學(xué)學(xué)報(bào)：哲學(xué)社會(huì)科學(xué)版,2010,42(5):68-73.

[9] Alur R.Techniques for automatic verification of real-time systems[D].Stanford:Stanford University,1991.

[10] Alur R,Courcoubetis C,Dill D.Model-checking for real-time systems[C]//Proceedings of fifth annual IEEE symposium on logic in computer science.[s.l.]:IEEE,1990:414-425.

[11] 錢俊彥,趙嶺忠,古天龍.一種基于時(shí)間自動(dòng)機(jī)的時(shí)鐘等價(jià)性優(yōu)化方法[J].計(jì)算機(jī)工程,2005,31(18):71-73.

[12] 狄楊思.形式規(guī)范的自動(dòng)驗(yàn)證算法的研究[D].南京:南京航空航天大學(xué)，2012.

[13] Cao Z,Wang H.Hybrid ZIA and its approximated refinement relation[C]//Proceedings of the 6th international conference on evaluation of novel approaches to software engineering.Beijing,China:[s.n.],2011:260-265.

An Approach of Bisimulation Checking for Real-time System Based on Data Constraints

LI Guo-zheng，GAO Zheng

(School of Computer Science and Technology,Nanjing University of Aeronautics & Astronautics,Nanjing 210016,China)

Real-time systems with data constraints refer to computing systems both with time-bound and data variables constraints,which is widely used in safety-critical areas like aerospace,industry control,defense system,playing an important role.Formal modeling and verification for these systems is an important way to ensure the correctness and reliability of the systems.In this paper,study a specification model combining interface automata,timed automata and Z language,named CT-ZIA.This model can be used to describe temporal properties and data properties of real-time systems with data constraints.Second,in order to study formal verification for bisimulation in the specification,the bisimulation definition for CT-ZIA is given.Then,for the decidability of simulation algorithm,each clock of CT-ZIA is partitioning in equivalence,putting forward the definition of limited domain CT-ZIA’s.Finally,give an algorithm for checking bisimulation relation between CT-ZIAs with finite domain and demonstrate the correctness of the algorithm.

real-time system;interface automata;Z notation;timed automata;bisimulation checking

2014-11-25

2015-03-04

時(shí)間：2016-01-04

航空科學(xué)基金(20128052064)；中央高校基本科研業(yè)務(wù)費(fèi)專項(xiàng)資金(NZ2013306)；國(guó)家“973”重點(diǎn)基礎(chǔ)研究發(fā)展計(jì)劃項(xiàng)目(2014CB744903)

李國(guó)拯(1990-)，男，碩士研究生，研究方向?yàn)樾问交椒?、模型檢測(cè)。

http://www.cnki.net/kcms/detail/61.1450.TP.20160104.1608.084.html

TP311

A

1673-629X(2016)01-0006-04

10.3969/j.issn.1673-629X.2016.01.002