杜澤民 王曉玲 陳宜成
摘 要:互聯(lián)網(wǎng)技術(shù)的發(fā)展和應(yīng)用在各個(gè)生產(chǎn)領(lǐng)域中發(fā)揮著越來越積極的作用,但隨著網(wǎng)絡(luò)技術(shù)應(yīng)用的深入,網(wǎng)絡(luò)系統(tǒng)的實(shí)時(shí)性成為影響網(wǎng)絡(luò)安全的一大因素,因此對網(wǎng)絡(luò)模型的通信實(shí)時(shí)性、威脅分析實(shí)時(shí)性的驗(yàn)證成為網(wǎng)絡(luò)安全的重要保障。目前,國內(nèi)外在實(shí)時(shí)性驗(yàn)證方面有諸多研究,形成了不同的方法體系。文章把主要的模型實(shí)時(shí)性驗(yàn)證方法,從理論和工具角度加以介紹分析,并對各個(gè)方法進(jìn)行了比較。
關(guān)鍵詞:網(wǎng)絡(luò)安全;實(shí)時(shí)性;模型驗(yàn)證;實(shí)時(shí)性驗(yàn)證
中圖分類號(hào):TP393.0 文獻(xiàn)標(biāo)識(shí)碼:A
1 引言
在互聯(lián)網(wǎng)時(shí)代,網(wǎng)絡(luò)安全問題是互聯(lián)網(wǎng)建設(shè)的重要議題,而網(wǎng)絡(luò)系統(tǒng)的實(shí)時(shí)性是網(wǎng)絡(luò)安全的重要保證[1]。其中,包括通信的實(shí)時(shí)性以及威脅分析的實(shí)時(shí)性等。當(dāng)網(wǎng)絡(luò)受到外界攻擊時(shí),系統(tǒng)應(yīng)該對相應(yīng)的問題快速做出反應(yīng)并處理措施。問題處理完畢后,還應(yīng)將處理結(jié)果在規(guī)定的時(shí)間內(nèi)反饋給系統(tǒng)。實(shí)時(shí)網(wǎng)絡(luò)系統(tǒng)的每一個(gè)運(yùn)行過程都是為了能夠保證整個(gè)網(wǎng)絡(luò)系統(tǒng)各項(xiàng)工作的協(xié)調(diào)進(jìn)行。
模型驅(qū)動(dòng)方法面對復(fù)雜度、集成性更高的大型系統(tǒng)有著安全性高、開發(fā)成本低等優(yōu)勢。當(dāng)前的航空、航天控制系統(tǒng)、軍事指揮自動(dòng)化系統(tǒng),也逐漸采用基于模型的開發(fā)方式,而這類系統(tǒng)對軟件有著應(yīng)實(shí)時(shí)性要求,反應(yīng)時(shí)間要控制在幾毫秒以內(nèi),而通常還要求保留一定的反應(yīng)余量。因此,模型驗(yàn)證在網(wǎng)絡(luò)系統(tǒng)的實(shí)時(shí)性驗(yàn)證上具有先天優(yōu)勢。
目前,國內(nèi)外對模型的功能與正確性驗(yàn)證研究比較豐富,但是實(shí)時(shí)性驗(yàn)證研究并不廣泛。因此,本文將介紹當(dāng)前實(shí)時(shí)性驗(yàn)證所面臨的問題,并重點(diǎn)介紹網(wǎng)絡(luò)系統(tǒng)實(shí)時(shí)性驗(yàn)證領(lǐng)域的建模方法,并結(jié)合這些方法所依托的工具,分析各種方法所面臨的問題,最后針對檢測方法面臨的挑戰(zhàn)提出一些思路。
2 模型驗(yàn)證方法及面臨的問題
模型檢測首先要對系統(tǒng)建模,選用一種形式化描述方法,將待驗(yàn)證的系統(tǒng)設(shè)計(jì)轉(zhuǎn)化為工具所能接受的模型,比如狀態(tài)遷移圖。然后,將系統(tǒng)所要驗(yàn)證的性質(zhì)采用形式化的邏輯公式來描述,比如時(shí)態(tài)邏輯。它能夠描述系統(tǒng)隨著時(shí)間變化而引起的行為變化。最后是系統(tǒng)驗(yàn)證,是通過模型檢測算法對系統(tǒng)模型的狀態(tài)空間進(jìn)行窮盡搜索。如果未發(fā)現(xiàn)違反性質(zhì)描述的狀態(tài),則表明該模型滿足期望的性質(zhì),否則給出一個(gè)反例路徑,供設(shè)計(jì)人員參考。
模型驗(yàn)證方法應(yīng)用初期,系統(tǒng)的狀態(tài)和狀態(tài)間的遷移都是采用顯式的狀態(tài)遷移圖來表示。這種方法對那些進(jìn)程數(shù)量較少的網(wǎng)絡(luò)系統(tǒng)非常實(shí)用[2]。而當(dāng)網(wǎng)絡(luò)分量較多時(shí),系統(tǒng)的全局狀態(tài)空間會(huì)隨著分量的增加,呈指數(shù)增長,即產(chǎn)生狀態(tài)爆炸問題,狀態(tài)爆炸問題是阻礙模型檢測技術(shù)應(yīng)用的瓶頸。
3 建模方法
3.1 最差情況執(zhí)行時(shí)間方法
最差情況執(zhí)行時(shí)間(Worst-Case Execution Time,WCET)是驗(yàn)證系統(tǒng)實(shí)時(shí)性的主要方法之一,由奧地利維也納技術(shù)大學(xué)的Puschner和Burns提出[3]。WCET剛提出時(shí),由于當(dāng)時(shí)計(jì)算機(jī)軟件需求有限,軟件代碼的執(zhí)行時(shí)間未引起人們的重視。但是,隨著軟件技術(shù)的不斷發(fā)展,代碼執(zhí)行時(shí)間的越來越復(fù)雜,WCET分析技術(shù)逐漸受到研究者的重視,目前,國內(nèi)外有許多機(jī)構(gòu)或大學(xué)開始加深對WCET的研究,從2001年開始,國際上每年召開一次WCET研討會(huì)。WCET分析技術(shù)與計(jì)算方法趨于多樣化,從早期的程序標(biāo)注和語法制導(dǎo)算法發(fā)展為基于樹和路徑的計(jì)算方法。
WCET分析是指計(jì)算給定應(yīng)用程序代碼片斷執(zhí)行時(shí)間的上限,這里的執(zhí)行時(shí)間定義為執(zhí)行代碼片斷所花費(fèi)的處理器時(shí)間。在實(shí)時(shí)系統(tǒng)中,如果想保證系統(tǒng)整體的實(shí)時(shí)性得到滿足,就必須要求軟件各部分在最差情況下執(zhí)行的時(shí)間也能滿足實(shí)時(shí)性要求,這樣由部分集成到整體時(shí),整個(gè)系統(tǒng)才會(huì)滿足實(shí)時(shí)性的要求。
WCET分析要求安全性和精確性,安全要求不能低估最差執(zhí)行時(shí)間,精確要求能夠給出可以接受的高估值。我們假設(shè)程序P的WCET估算值為WCETc (P),P的實(shí)際WCET值為WCETA (P),安全性和精確性描述為:
安全性:
WCETc (P) ≥WCETA (P)
精確性:
(WCETc(P) -WCETA(P))/WCETA(P)≤δmax
其中,δmax為系統(tǒng)能夠接受的最大相對誤差。
在程序?qū)哟蔚尿?yàn)證方面,國防科技大學(xué)張曦團(tuán)隊(duì)利用WCET技術(shù)對嵌入式實(shí)時(shí)軟件的驗(yàn)證進(jìn)行了深入研究,提出了一種基于WCET分析的模型檢驗(yàn)方法框架[4],實(shí)現(xiàn)了對源程序的一種實(shí)時(shí)性驗(yàn)證方法。
該框架首先對源程序進(jìn)行WCET分析,其中包括對程序的靜態(tài)分析,劃分出程序代碼的路徑集,然后利用WCET工具進(jìn)行分析程序執(zhí)行時(shí)間上限,分析過程如圖1所示。
利用WCET分析結(jié)果對原有的實(shí)時(shí)約束進(jìn)行修正,建立系統(tǒng)的實(shí)時(shí)性模型,同時(shí)在系統(tǒng)需求中提取時(shí)態(tài)邏輯作為系統(tǒng)的性質(zhì)描述,其中時(shí)態(tài)邏輯反映了程序應(yīng)該遵循的先后順序。結(jié)合實(shí)時(shí)性模型與時(shí)態(tài)邏輯公式通過驗(yàn)證工具UPPAAL對模型的實(shí)時(shí)性進(jìn)行驗(yàn)證,如果實(shí)時(shí)性驗(yàn)證不通過,則返回修改源程序。如圖2所示。
本方法做到了對實(shí)時(shí)系統(tǒng)的程序?qū)哟蔚尿?yàn)證,較好地解決了狀態(tài)爆炸問題,其中源程序的WCET分析是驗(yàn)證環(huán)節(jié)的重要一環(huán),但是當(dāng)前WCET分析能力有限,比如復(fù)雜程序運(yùn)算時(shí)間估算、估值精確度、誤差控制等問題。另外,對源程序的修正可能會(huì)引入新的錯(cuò)誤,并且修正內(nèi)容無法反映到生成代碼的上層模型中。
3.2 時(shí)間自動(dòng)機(jī)建模
為了描述實(shí)時(shí)系統(tǒng)的時(shí)間約束關(guān)系,Alur等人提出了時(shí)間自動(dòng)機(jī)(Timed Automata,TA)[5]。時(shí)間自動(dòng)機(jī)是一類帶有時(shí)鐘變量的有限狀態(tài)自動(dòng)機(jī),其數(shù)學(xué)模型可表述為一個(gè)六元組:
Ta= (L,L0,C,A,E,I )
其中:L是位置的有限集合;l0∈L,為初始位置;C是時(shí)鐘有限集合;A是行為的有限集合;"EL×B(C)×A×2c×L是邊的集合,用于描述位置之間的轉(zhuǎn)移;B(C)是使能條件集合,用于描述發(fā)生轉(zhuǎn)移的時(shí)間約束,2c為轉(zhuǎn)移發(fā)生時(shí)的時(shí)鐘集合;映射I:"L→ B(C)" 用于給每個(gè)位置指定一個(gè)時(shí)鐘約束。
用時(shí)間自動(dòng)機(jī)網(wǎng)對實(shí)時(shí)系統(tǒng)建模,首先要對系統(tǒng)進(jìn)行抽象和簡化,子系統(tǒng)要簡化為有限控制結(jié)構(gòu)、時(shí)鐘和變量構(gòu)成的時(shí)間自動(dòng)機(jī),子系統(tǒng)之間通過通道進(jìn)行通訊。然后要分析實(shí)時(shí)系統(tǒng)的信息處理過程,提煉重要的信息處理狀態(tài)和事件進(jìn)行建模。子系統(tǒng)的行為抽象為時(shí)間自動(dòng)機(jī),它們之間的信息交互通過通道來完成,各個(gè)時(shí)間自動(dòng)機(jī)就組成網(wǎng)絡(luò)進(jìn)而描述整個(gè)實(shí)時(shí)系統(tǒng)的信息處理過程。
時(shí)間自動(dòng)機(jī)是一種反映了時(shí)間約束的有限狀態(tài)轉(zhuǎn)換圖,通過使用有限的真值時(shí)鐘變量表示時(shí)間約束,實(shí)時(shí)系統(tǒng)行為可以通過時(shí)間自動(dòng)機(jī)來刻畫,在對實(shí)時(shí)系統(tǒng)建模后,可以利用時(shí)間自動(dòng)機(jī)來驗(yàn)證系統(tǒng)的實(shí)時(shí)性。在實(shí)時(shí)性約束下檢驗(yàn)狀態(tài)是否可達(dá),因此對狀態(tài)可達(dá)性的研究是時(shí)間自動(dòng)機(jī)的驗(yàn)證技術(shù)的關(guān)鍵。
時(shí)間自動(dòng)機(jī)技術(shù)也有不足:構(gòu)造時(shí)間自動(dòng)機(jī)方法很復(fù)雜,如果發(fā)生錯(cuò)誤,將導(dǎo)致最終驗(yàn)證結(jié)果的不準(zhǔn)確。另外,時(shí)間自動(dòng)機(jī)的時(shí)間無限制,會(huì)導(dǎo)致狀態(tài)空間的無限性,隨著系統(tǒng)的復(fù)雜程度和進(jìn)程數(shù)量的增加,將無可避免的發(fā)生狀態(tài)空間爆炸。狀態(tài)空間爆炸也是困擾實(shí)時(shí)系統(tǒng)驗(yàn)證的最大問題。
但是,典型的時(shí)間自動(dòng)機(jī)組成的平面網(wǎng)絡(luò)作為模型不易于模擬和調(diào)試大規(guī)模的工業(yè)系統(tǒng)。AIexandre David和Wang Yi提出了一種層疊時(shí)間自動(dòng)機(jī)(Hierarchical Timed Automata,HTA)模型,它的狀態(tài)既可以是簡單狀態(tài)也可以是組合狀態(tài),組合狀態(tài)本身就是一個(gè)時(shí)間自動(dòng)機(jī)。
層疊時(shí)間自動(dòng)機(jī)的允許用戶在模擬時(shí),將系統(tǒng)模型的內(nèi)部結(jié)構(gòu)隱藏或者抽象,并且更容易調(diào)試,在處理多層次復(fù)雜系統(tǒng)建模時(shí)有較大優(yōu)勢。
3.3 RTCTL模型檢測方法
計(jì)算樹邏輯(Computation Tree Logic,CTL)是時(shí)序邏輯的一個(gè)分支,時(shí)序邏輯非常適合于對并發(fā)系統(tǒng)進(jìn)行驗(yàn)證與刻畫,即使對于復(fù)雜的并發(fā)系統(tǒng)而言,其刻畫性質(zhì)依然很強(qiáng)。時(shí)序邏輯用于描述系統(tǒng)中的狀態(tài)變遷序列,不顯示地表示時(shí)間,而是通過語義隱式表達(dá)時(shí)間。時(shí)序邏輯定義時(shí)序運(yùn)算符與邏輯連接詞來表達(dá)復(fù)雜的時(shí)序性質(zhì)。CTL作為時(shí)序邏輯的一個(gè)分支主要用來描述計(jì)算樹的性質(zhì)[8]。
CTL公式由路徑量詞與時(shí)序運(yùn)算符組成。路徑量詞用于描述計(jì)算樹的分支結(jié)構(gòu),有兩種路徑量詞:A(對于所有計(jì)算路徑)和E(對于某些計(jì)算路徑),分別表示從某狀態(tài)開始的所有路徑和某些路徑所具有的性質(zhì)。時(shí)序運(yùn)算符描述某條路徑的具體性質(zhì)。有5個(gè)基本運(yùn)算符,意義如下:X(下一個(gè)狀態(tài))F(將來某狀態(tài))G(將來全局狀態(tài))U(直到……都滿足)R(直到……才滿足)。
CTL有兩種公式:狀態(tài)公式與路徑公式。令A(yù)P為原子命題集合,狀態(tài)公式語法為:
1) 如果p∈AP,則p是一個(gè)狀態(tài)公式;
2) 如果f和g是狀態(tài)公式,則f和f∧g,f∨g是狀態(tài)公式;
3) 如果f是一個(gè)路徑公式,則Ef和Af是狀態(tài)公式。
路徑公式的語法為:
如果f是一狀態(tài)公式,則f也是一路徑公式;
如果f和g是路徑公式,則f,f∧g,f∨g,Xf,F(xiàn)f,Gf,fUg和飛fRg是路徑公式[9]。
檢測實(shí)時(shí)系統(tǒng)的時(shí)間約束的有效方法就是擴(kuò)充CTL運(yùn)算符,Emerson等人將CTL邏輯擴(kuò)充為RTCTL?;镜腞TCTL運(yùn)算符是受限的直到運(yùn)算符U[a,b]這里[a,b]表示時(shí)間間隔,在此間隔內(nèi)這個(gè)性質(zhì)必須是真的。fU[a,b]g關(guān)于某條路徑π=s0,s1…為真,僅當(dāng)g在此路徑上將來的某個(gè)狀態(tài)s上滿足,那么f在s0到s上所有狀態(tài)都為真,并且s0到s的距離在間隔[a,b]之間。同樣的,CTL中的其他運(yùn)算符可以增加時(shí)間限制來擴(kuò)展。[a,b]作為一個(gè)時(shí)間間隔,可以看做是實(shí)時(shí)性的約束。
RTCTL模型在CTL的基礎(chǔ)上進(jìn)行了擴(kuò)充,繼承了CTL模型的精確性,解決了狀態(tài)空間爆炸問題,同時(shí)加入了時(shí)間性約束,可以高效地表達(dá)實(shí)時(shí)性要求。目前有很多工具可以完成基于CTL的模型驗(yàn)證,RTCTL在實(shí)時(shí)性驗(yàn)證中的有很好的應(yīng)用前景。
通過對時(shí)間進(jìn)行量化分析,可以得到系統(tǒng)的最大、最小時(shí)延,完成實(shí)時(shí)性驗(yàn)證。
4 模型驗(yàn)證常用工具
4.1 UPPAAL
UPPAAL是丹麥Aalborg和瑞士Uppsala大學(xué)聯(lián)合開發(fā)[10],高效實(shí)用的基于時(shí)間自動(dòng)機(jī)的實(shí)時(shí)系統(tǒng)模型驗(yàn)證工具。UPPAAL特別適用于實(shí)時(shí)系統(tǒng)的安全性和活性的自動(dòng)驗(yàn)證。它將每個(gè)進(jìn)程都描述為有限控制結(jié)構(gòu)、時(shí)鐘和變量組成的時(shí)間自動(dòng)機(jī),進(jìn)程之間通過管道共享數(shù)據(jù)變量進(jìn)行通信,管道用于保證不同自動(dòng)機(jī)中的兩個(gè)轉(zhuǎn)換同時(shí)執(zhí)行。UPPAAL通過快速搜索機(jī)制來驗(yàn)證時(shí)鐘約束和可達(dá)性,不僅可以有效地發(fā)現(xiàn)設(shè)計(jì)中出現(xiàn)的錯(cuò)誤,而且可以清楚地顯示導(dǎo)致錯(cuò)誤的判定路徑。
UPPAAL擁有圖形用戶界面,主要包括三個(gè)部分:編輯器(Editor)、模擬器(Simulator)和驗(yàn)證器(Verifier)。編輯器用于創(chuàng)建和編輯所要分析的系統(tǒng);模擬器用于模擬系統(tǒng)模型執(zhí)行過程可能出現(xiàn)的錯(cuò)誤,以便在驗(yàn)證前發(fā)現(xiàn)潛在的錯(cuò)誤;驗(yàn)證器通過快速搜索機(jī)制搜索系統(tǒng)的狀態(tài)空間、檢查時(shí)鐘約束和響應(yīng)限制性質(zhì)。
UPPAAL體系結(jié)構(gòu)如圖3所示。
UPPAAL的引入,簡化了實(shí)時(shí)系統(tǒng)驗(yàn)證的工作量,并且增加了驗(yàn)證系統(tǒng)的可靠性。首先,UPPAAL中時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)中每個(gè)時(shí)間自動(dòng)機(jī)都是相對獨(dú)立的,又是可以互相通信的,不需要構(gòu)造時(shí)間自動(dòng)機(jī)的積,避免了構(gòu)造模型的繁雜。另外,UPPAAL中的模擬器從直觀上可以看到系統(tǒng)的運(yùn)行過程,發(fā)現(xiàn)存在的問題,而驗(yàn)證器又嚴(yán)格的從語義上保證了系統(tǒng)的安全性。UPPAAL在時(shí)間和空間上的性能顯著高于其他的實(shí)時(shí)驗(yàn)證工具,能夠處理較為復(fù)雜的系統(tǒng)。
4.2 NuSMV
1987年左右,卡內(nèi)基梅隆大學(xué)在讀博士生McMillan開發(fā)出一個(gè)符號(hào)模型驗(yàn)證器SMV(Symbolic Model Verifier),首次使用二叉決策圖(Binary Decision Diagram,BDD)來緩解狀態(tài)爆炸問題,實(shí)現(xiàn)了符號(hào)模型檢測技術(shù),SMV是第一個(gè)基于BDD的符號(hào)模型驗(yàn)證工具[11]。2001年,Carnegie Mellon University(CMU)和Istitutoperla Ricerca Scientificae Techolgica(IRST)聯(lián)合開發(fā)出NuSMV( New Symbolic Model Verifier)[12],NuSMV支持計(jì)算樹邏輯(Computation Tree Logic,CTL)和線性時(shí)序邏輯(Linear Temporal Logic,LTL)描述的所有規(guī)范,作為一款比較成熟的模型檢測工具已經(jīng)發(fā)展到2.6.0版,NuSMV是開源工具,其源代碼和二進(jìn)制文件可以在官網(wǎng)上獲取。
作為一種通用的模型驗(yàn)證器,NuSMV的基本運(yùn)行原理:用戶使用NuSMV提供的輸入語言描述待驗(yàn)證實(shí)時(shí)系統(tǒng)和約束性規(guī)范,通過NuSMV自動(dòng)進(jìn)行,驗(yàn)證確定模型在規(guī)范中是否成立,若不成立輸出No,并給出反例,解析為什么規(guī)范在模型中不成立。NuSMV的運(yùn)行原理如圖4所示。
在功能上,NuSMV支持CTL描述規(guī)范,所以RTCTL同樣可以在NuSMV上得到驗(yàn)證,NuSMV在實(shí)時(shí)驗(yàn)證領(lǐng)域占有一席之地。
在結(jié)構(gòu)上,NuSMV定義了一個(gè)良好的軟件系統(tǒng)架構(gòu),做到了模塊化和開放性,用戶可以自由定制模塊。
在支持性上,NuSMV有豐富的文檔和開放的源碼,作為一種模型檢測的通用平臺(tái),用戶可以在官網(wǎng)和開源社區(qū)獲得幫助。
NuSMV的引入,明顯地簡化了實(shí)時(shí)系統(tǒng)驗(yàn)證的工作量,研究者提供了更廣闊的研究空間[13]。
4.3 PAT
PAT[14]是由新加坡國立大學(xué)PAT研究小組自主開發(fā)的一套模型檢測工具,支持并發(fā)、網(wǎng)絡(luò)實(shí)時(shí)系統(tǒng)的建模驗(yàn)證,能夠?qū)Χ喾N語言進(jìn)行模擬驗(yàn)證和反例生成。PAT是一個(gè)可擴(kuò)展、模塊化的通用架構(gòu),其系統(tǒng)框架如圖5所示。
框架分為四層,方便了模塊的擴(kuò)展,建模驗(yàn)證過程分為三步:編譯、抽象和驗(yàn)證。PAT工具具有良好的擴(kuò)展性,因此可以利用建模層的抽象功能對建模語言進(jìn)行抽象,避免狀態(tài)爆炸。擴(kuò)展PAT的并行模塊可以方便網(wǎng)絡(luò)系統(tǒng)的實(shí)時(shí)性的建模與驗(yàn)證。抽象后的語言模塊能夠自動(dòng)轉(zhuǎn)化為PAT已經(jīng)支持的語言,從而簡化系統(tǒng)描述和實(shí)現(xiàn)過程,使得建模過程更人性化、更易使用。借助PAT工具良好的擴(kuò)展性,可方便對網(wǎng)絡(luò)系統(tǒng)進(jìn)行實(shí)時(shí)性建模。
4 結(jié)束語
本文首先介紹了模型驗(yàn)證的概念與當(dāng)前的問題,并總結(jié)了三種網(wǎng)絡(luò)實(shí)時(shí)性模型的驗(yàn)證方法和主流的實(shí)時(shí)性驗(yàn)證工具,對其優(yōu)缺點(diǎn)進(jìn)行了比較,為今后的研究提供有益參考。網(wǎng)絡(luò)安全領(lǐng)域的模型檢測技術(shù)應(yīng)用越來越廣泛。保障日益復(fù)雜的網(wǎng)絡(luò)空間的安全性,是當(dāng)前研究的難題,建立在嚴(yán)格數(shù)學(xué)理論基礎(chǔ)之上的模型驗(yàn)證必將在其中占據(jù)一席之地。
參考文獻(xiàn)
[1] 劉權(quán),王超.勒索軟件攻擊事件或?qū)⒁l(fā)網(wǎng)絡(luò)軍備競賽升級(jí)[J].網(wǎng)絡(luò)空間安全,2018,01:1-4.
[2] 張修康,金春華,白瑩.應(yīng)對網(wǎng)絡(luò)安全威脅的技術(shù)演變[J].網(wǎng)絡(luò)空間安全,2018,01:46-50.
[3] PETER PUSCHNER and A.Burns. Guest Editorial: A Review of Worst-Case Execution-Time Analysis, Real-Tim Systems, May 2000, 18(2-3): 115~128.
[4] 張曦.基于WCET分析技術(shù)的程序?qū)崟r(shí)性模型檢驗(yàn)方法研究[D].國防科學(xué)技術(shù)大學(xué),2012.
[5] Alur R, Dill DL. A theory of t imed automat a[J] . Theoretical Computer Science, 1994, 126( 2) : 183- 235.
[6] David A , Yi W . Hierarchical Timed Automat a for UPPAAL [ A ] .10th Nordic Workshop on Programming Theory ( NWPT) 98) [ C] .Turku Cent re f or Computer Science (T UCS) , Finland, 1998.
[7] Michael Huth and Mark Ryan.Logic in Computer Science:Modelling and Reasoning about System,Second Edition.Cambridge University Press,2004.
[8] E.M.Clarke and E.A.Emerson.Synthesis of synchronization skeletons for branching time temporal logic.In Logic of Programs:Workshop,Yorktown,Heights NY May 1981,volume 131 of LNCS.Springer-Verlag,1981.
[9] Emerson E.A..Branching time temporal logic and the design of correct concurrent programs[Ph.D.dissertation].Harvard University,Cambridge,MA,1981
[10] Behrmann G, David A, Larsen KG. A tutorial on UPPAAL. In: Bernardo M, ed. Proc. of the Formal Methods for the Design of Real-Time Systems. Springer-Verlag, 2004. 200?236. [doi: 10.1007/978-3-540-30080-9_7]
[11] 張軍林,張治國.NuSMV模型驗(yàn)證器實(shí)現(xiàn)與分析[D].中山大學(xué),2010.
[12] CIMATTI A,CLARKE E,GIUNCHIGLIA F,et al.NuSMV: a new symbolic model verifier[C]Computer Aided Verification.Berlin: Springer,1999: 495-499.
[13] 劉博,李蜀瑜.基于NuSMV的AADL行為模型驗(yàn)證的探究[J].計(jì)算機(jī)技術(shù)與發(fā)展,2012,(2).
[14] LIU Y, SUNJ, DONGJS.Developing model checkers using PAT[C]//8th International Symposium on Automated Technology for Verification and Analysis. Sydney: Springer Press, 2010:371-377.