網(wǎng)絡(luò)系統(tǒng)實(shí)時(shí)性模型的驗(yàn)證方法綜述

杜澤民 王曉玲 陳宜成

摘 要：互聯(lián)網(wǎng)技術(shù)的發(fā)展和應(yīng)用在各個(gè)生產(chǎn)領(lǐng)域中發(fā)揮著越來(lái)越積極的作用，但隨著網(wǎng)絡(luò)技術(shù)應(yīng)用的深入，網(wǎng)絡(luò)系統(tǒng)的實(shí)時(shí)性成為影響網(wǎng)絡(luò)安全的一大因素，因此對(duì)網(wǎng)絡(luò)模型的通信實(shí)時(shí)性、威脅分析實(shí)時(shí)性的驗(yàn)證成為網(wǎng)絡(luò)安全的重要保障。目前，國(guó)內(nèi)外在實(shí)時(shí)性驗(yàn)證方面有諸多研究，形成了不同的方法體系。文章把主要的模型實(shí)時(shí)性驗(yàn)證方法，從理論和工具角度加以介紹分析，并對(duì)各個(gè)方法進(jìn)行了比較。

關(guān)鍵詞：網(wǎng)絡(luò)安全；實(shí)時(shí)性；模型驗(yàn)證；實(shí)時(shí)性驗(yàn)證

中圖分類(lèi)號(hào)：TP393.0 文獻(xiàn)標(biāo)識(shí)碼：A

1 引言

在互聯(lián)網(wǎng)時(shí)代，網(wǎng)絡(luò)安全問(wèn)題是互聯(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)該對(duì)相應(yīng)的問(wèn)題快速做出反應(yīng)并處理措施。問(wèn)題處理完畢后，還應(yīng)將處理結(jié)果在規(guī)定的時(shí)間內(nèi)反饋給系統(tǒng)。實(shí)時(shí)網(wǎng)絡(luò)系統(tǒng)的每一個(gè)運(yùn)行過(guò)程都是為了能夠保證整個(gè)網(wǎng)絡(luò)系統(tǒng)各項(xiàng)工作的協(xié)調(diào)進(jìn)行。

模型驅(qū)動(dòng)方法面對(duì)復(fù)雜度、集成性更高的大型系統(tǒng)有著安全性高、開(kāi)發(fā)成本低等優(yōu)勢(shì)。當(dāng)前的航空、航天控制系統(tǒng)、軍事指揮自動(dòng)化系統(tǒng)，也逐漸采用基于模型的開(kāi)發(fā)方式，而這類(lèi)系統(tǒng)對(duì)軟件有著應(yīng)實(shí)時(shí)性要求，反應(yīng)時(shí)間要控制在幾毫秒以內(nèi)，而通常還要求保留一定的反應(yīng)余量。因此，模型驗(yàn)證在網(wǎng)絡(luò)系統(tǒng)的實(shí)時(shí)性驗(yàn)證上具有先天優(yōu)勢(shì)。

目前，國(guó)內(nèi)外對(duì)模型的功能與正確性驗(yàn)證研究比較豐富，但是實(shí)時(shí)性驗(yàn)證研究并不廣泛。因此，本文將介紹當(dāng)前實(shí)時(shí)性驗(yàn)證所面臨的問(wèn)題，并重點(diǎn)介紹網(wǎng)絡(luò)系統(tǒng)實(shí)時(shí)性驗(yàn)證領(lǐng)域的建模方法，并結(jié)合這些方法所依托的工具，分析各種方法所面臨的問(wèn)題，最后針對(duì)檢測(cè)方法面臨的挑戰(zhàn)提出一些思路。

2 模型驗(yàn)證方法及面臨的問(wèn)題

模型檢測(cè)首先要對(duì)系統(tǒng)建模，選用一種形式化描述方法，將待驗(yàn)證的系統(tǒng)設(shè)計(jì)轉(zhuǎn)化為工具所能接受的模型，比如狀態(tài)遷移圖。然后，將系統(tǒng)所要驗(yàn)證的性質(zhì)采用形式化的邏輯公式來(lái)描述，比如時(shí)態(tài)邏輯。它能夠描述系統(tǒng)隨著時(shí)間變化而引起的行為變化。最后是系統(tǒng)驗(yàn)證，是通過(guò)模型檢測(cè)算法對(duì)系統(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)遷移圖來(lái)表示。這種方法對(duì)那些進(jìn)程數(shù)量較少的網(wǎng)絡(luò)系統(tǒng)非常實(shí)用[2]。而當(dāng)網(wǎng)絡(luò)分量較多時(shí)，系統(tǒng)的全局狀態(tài)空間會(huì)隨著分量的增加，呈指數(shù)增長(zhǎng)，即產(chǎn)生狀態(tài)爆炸問(wèn)題，狀態(tài)爆炸問(wèn)題是阻礙模型檢測(cè)技術(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í)間的越來(lái)越復(fù)雜，WCET分析技術(shù)逐漸受到研究者的重視，目前，國(guó)內(nèi)外有許多機(jī)構(gòu)或大學(xué)開(kāi)始加深對(duì)WCET的研究，從2001年開(kāi)始，國(guó)際上每年召開(kāi)一次WCET研討會(huì)。WCET分析技術(shù)與計(jì)算方法趨于多樣化，從早期的程序標(biāo)注和語(yǔ)法制導(dǎo)算法發(fā)展為基于樹(shù)和路徑的計(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)能夠接受的最大相對(duì)誤差。

在程序?qū)哟蔚尿?yàn)證方面，國(guó)防科技大學(xué)張曦團(tuán)隊(duì)利用WCET技術(shù)對(duì)嵌入式實(shí)時(shí)軟件的驗(yàn)證進(jìn)行了深入研究，提出了一種基于WCET分析的模型檢驗(yàn)方法框架[4]，實(shí)現(xiàn)了對(duì)源程序的一種實(shí)時(shí)性驗(yàn)證方法。

該框架首先對(duì)源程序進(jìn)行WCET分析，其中包括對(duì)程序的靜態(tài)分析，劃分出程序代碼的路徑集，然后利用WCET工具進(jìn)行分析程序執(zhí)行時(shí)間上限，分析過(guò)程如圖1所示。

利用WCET分析結(jié)果對(duì)原有的實(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)邏輯公式通過(guò)驗(yàn)證工具UPPAAL對(duì)模型的實(shí)時(shí)性進(jìn)行驗(yàn)證，如果實(shí)時(shí)性驗(yàn)證不通過(guò)，則返回修改源程序。如圖2所示。

本方法做到了對(duì)實(shí)時(shí)系統(tǒng)的程序?qū)哟蔚尿?yàn)證，較好地解決了狀態(tài)爆炸問(wèn)題，其中源程序的WCET分析是驗(yàn)證環(huán)節(jié)的重要一環(huán)，但是當(dāng)前WCET分析能力有限，比如復(fù)雜程序運(yùn)算時(shí)間估算、估值精確度、誤差控制等問(wèn)題。另外，對(duì)源程序的修正可能會(huì)引入新的錯(cuò)誤，并且修正內(nèi)容無(wú)法反映到生成代碼的上層模型中。

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ī)是一類(lèi)帶有時(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)對(duì)實(shí)時(shí)系統(tǒng)建模，首先要對(duì)系統(tǒng)進(jìn)行抽象和簡(jiǎn)化，子系統(tǒng)要簡(jiǎn)化為有限控制結(jié)構(gòu)、時(shí)鐘和變量構(gòu)成的時(shí)間自動(dòng)機(jī)，子系統(tǒng)之間通過(guò)通道進(jìn)行通訊。然后要分析實(shí)時(shí)系統(tǒng)的信息處理過(guò)程，提煉重要的信息處理狀態(tài)和事件進(jìn)行建模。子系統(tǒng)的行為抽象為時(shí)間自動(dòng)機(jī)，它們之間的信息交互通過(guò)通道來(lái)完成，各個(gè)時(shí)間自動(dòng)機(jī)就組成網(wǎng)絡(luò)進(jìn)而描述整個(gè)實(shí)時(shí)系統(tǒng)的信息處理過(guò)程。

時(shí)間自動(dòng)機(jī)是一種反映了時(shí)間約束的有限狀態(tài)轉(zhuǎn)換圖，通過(guò)使用有限的真值時(shí)鐘變量表示時(shí)間約束，實(shí)時(shí)系統(tǒng)行為可以通過(guò)時(shí)間自動(dòng)機(jī)來(lái)刻畫(huà)，在對(duì)實(shí)時(shí)系統(tǒng)建模后，可以利用時(shí)間自動(dòng)機(jī)來(lái)驗(yàn)證系統(tǒng)的實(shí)時(shí)性。在實(shí)時(shí)性約束下檢驗(yàn)狀態(tài)是否可達(dá)，因此對(duì)狀態(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í)間無(wú)限制，會(huì)導(dǎo)致?tīng)顟B(tài)空間的無(wú)限性，隨著系統(tǒng)的復(fù)雜程度和進(jìn)程數(shù)量的增加，將無(wú)可避免的發(fā)生狀態(tài)空間爆炸。狀態(tài)空間爆炸也是困擾實(shí)時(shí)系統(tǒng)驗(yàn)證的最大問(wè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)既可以是簡(jiǎn)單狀態(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)勢(shì)。

3.3 RTCTL模型檢測(cè)方法

計(jì)算樹(shù)邏輯（Computation Tree Logic，CTL）是時(shí)序邏輯的一個(gè)分支，時(shí)序邏輯非常適合于對(duì)并發(fā)系統(tǒng)進(jìn)行驗(yàn)證與刻畫(huà)，即使對(duì)于復(fù)雜的并發(fā)系統(tǒng)而言，其刻畫(huà)性質(zhì)依然很強(qiáng)。時(shí)序邏輯用于描述系統(tǒng)中的狀態(tài)變遷序列，不顯示地表示時(shí)間，而是通過(guò)語(yǔ)義隱式表達(dá)時(shí)間。時(shí)序邏輯定義時(shí)序運(yùn)算符與邏輯連接詞來(lái)表達(dá)復(fù)雜的時(shí)序性質(zhì)。CTL作為時(shí)序邏輯的一個(gè)分支主要用來(lái)描述計(jì)算樹(shù)的性質(zhì)[8]。

CTL公式由路徑量詞與時(shí)序運(yùn)算符組成。路徑量詞用于描述計(jì)算樹(shù)的分支結(jié)構(gòu)，有兩種路徑量詞：A（對(duì)于所有計(jì)算路徑）和E（對(duì)于某些計(jì)算路徑），分別表示從某狀態(tài)開(kāi)始的所有路徑和某些路徑所具有的性質(zhì)。時(shí)序運(yùn)算符描述某條路徑的具體性質(zhì)。有5個(gè)基本運(yùn)算符，意義如下：X（下一個(gè)狀態(tài)）F（將來(lái)某狀態(tài)）G（將來(lái)全局狀態(tài)）U（直到……都滿足）R（直到……才滿足）。

CTL有兩種公式：狀態(tài)公式與路徑公式。令A(yù)P為原子命題集合，狀態(tài)公式語(yǔ)法為：

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)公式。

路徑公式的語(yǔ)法為：

如果f是一狀態(tài)公式，則f也是一路徑公式；

如果f和g是路徑公式，則f，f∧g，f∨g，Xf，F(xiàn)f，Gf，fUg和飛fRg是路徑公式[9]。

檢測(cè)實(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在此路徑上將來(lái)的某個(gè)狀態(tài)s上滿足，那么f在s0到s上所有狀態(tài)都為真，并且s0到s的距離在間隔[a，b]之間。同樣的，CTL中的其他運(yùn)算符可以增加時(shí)間限制來(lái)擴(kuò)展。[a，b]作為一個(gè)時(shí)間間隔，可以看做是實(shí)時(shí)性的約束。

RTCTL模型在CTL的基礎(chǔ)上進(jìn)行了擴(kuò)充，繼承了CTL模型的精確性，解決了狀態(tài)空間爆炸問(wèn)題，同時(shí)加入了時(shí)間性約束，可以高效地表達(dá)實(shí)時(shí)性要求。目前有很多工具可以完成基于CTL的模型驗(yàn)證，RTCTL在實(shí)時(shí)性驗(yàn)證中的有很好的應(yīng)用前景。

通過(guò)對(duì)時(shí)間進(jìn)行量化分析，可以得到系統(tǒng)的最大、最小時(shí)延，完成實(shí)時(shí)性驗(yàn)證。

4 模型驗(yàn)證常用工具

4.1 UPPAAL

UPPAAL是丹麥Aalborg和瑞士Uppsala大學(xué)聯(lián)合開(kāi)發(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)程之間通過(guò)管道共享數(shù)據(jù)變量進(jìn)行通信，管道用于保證不同自動(dòng)機(jī)中的兩個(gè)轉(zhuǎn)換同時(shí)執(zhí)行。UPPAAL通過(guò)快速搜索機(jī)制來(lái)驗(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í)行過(guò)程可能出現(xiàn)的錯(cuò)誤，以便在驗(yàn)證前發(fā)現(xiàn)潛在的錯(cuò)誤；驗(yàn)證器通過(guò)快速搜索機(jī)制搜索系統(tǒng)的狀態(tài)空間、檢查時(shí)鐘約束和響應(yīng)限制性質(zhì)。

UPPAAL體系結(jié)構(gòu)如圖3所示。

UPPAAL的引入，簡(jiǎn)化了實(shí)時(shí)系統(tǒng)驗(yàn)證的工作量，并且增加了驗(yàn)證系統(tǒng)的可靠性。首先，UPPAAL中時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)中每個(gè)時(shí)間自動(dòng)機(jī)都是相對(duì)獨(dú)立的，又是可以互相通信的，不需要構(gòu)造時(shí)間自動(dòng)機(jī)的積，避免了構(gòu)造模型的繁雜。另外，UPPAAL中的模擬器從直觀上可以看到系統(tǒng)的運(yùn)行過(guò)程，發(fā)現(xiàn)存在的問(wèn)題，而驗(yàn)證器又嚴(yán)格的從語(yǔ)義上保證了系統(tǒng)的安全性。UPPAAL在時(shí)間和空間上的性能顯著高于其他的實(shí)時(shí)驗(yàn)證工具，能夠處理較為復(fù)雜的系統(tǒng)。

4.2 NuSMV

1987年左右，卡內(nèi)基梅隆大學(xué)在讀博士生McMillan開(kāi)發(fā)出一個(gè)符號(hào)模型驗(yàn)證器SMV（Symbolic Model Verifier），首次使用二叉決策圖（Binary Decision Diagram，BDD）來(lái)緩解狀態(tài)爆炸問(wèn)題，實(shí)現(xiàn)了符號(hào)模型檢測(cè)技術(shù)，SMV是第一個(gè)基于BDD的符號(hào)模型驗(yàn)證工具[11]。2001年，Carnegie Mellon University（CMU）和Istitutoperla Ricerca Scientificae Techolgica（IRST）聯(lián)合開(kāi)發(fā)出NuSMV（ New Symbolic Model Verifier）[12]，NuSMV支持計(jì)算樹(shù)邏輯（Computation Tree Logic，CTL）和線性時(shí)序邏輯（Linear Temporal Logic，LTL）描述的所有規(guī)范，作為一款比較成熟的模型檢測(cè)工具已經(jīng)發(fā)展到2.6.0版，NuSMV是開(kāi)源工具，其源代碼和二進(jìn)制文件可以在官網(wǎng)上獲取。

作為一種通用的模型驗(yàn)證器，NuSMV的基本運(yùn)行原理：用戶使用NuSMV提供的輸入語(yǔ)言描述待驗(yàn)證實(shí)時(shí)系統(tǒng)和約束性規(guī)范，通過(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)，做到了模塊化和開(kāi)放性，用戶可以自由定制模塊。

在支持性上，NuSMV有豐富的文檔和開(kāi)放的源碼，作為一種模型檢測(cè)的通用平臺(tái)，用戶可以在官網(wǎng)和開(kāi)源社區(qū)獲得幫助。

NuSMV的引入，明顯地簡(jiǎn)化了實(shí)時(shí)系統(tǒng)驗(yàn)證的工作量，研究者提供了更廣闊的研究空間[13]。

4.3 PAT

PAT[14]是由新加坡國(guó)立大學(xué)PAT研究小組自主開(kāi)發(fā)的一套模型檢測(cè)工具，支持并發(fā)、網(wǎng)絡(luò)實(shí)時(shí)系統(tǒng)的建模驗(yàn)證，能夠?qū)Χ喾N語(yǔ)言進(jìn)行模擬驗(yàn)證和反例生成。PAT是一個(gè)可擴(kuò)展、模塊化的通用架構(gòu)，其系統(tǒng)框架如圖5所示。

框架分為四層，方便了模塊的擴(kuò)展，建模驗(yàn)證過(guò)程分為三步：編譯、抽象和驗(yàn)證。PAT工具具有良好的擴(kuò)展性，因此可以利用建模層的抽象功能對(duì)建模語(yǔ)言進(jìn)行抽象，避免狀態(tài)爆炸。擴(kuò)展PAT的并行模塊可以方便網(wǎng)絡(luò)系統(tǒng)的實(shí)時(shí)性的建模與驗(yàn)證。抽象后的語(yǔ)言模塊能夠自動(dòng)轉(zhuǎn)化為PAT已經(jīng)支持的語(yǔ)言，從而簡(jiǎn)化系統(tǒng)描述和實(shí)現(xiàn)過(guò)程，使得建模過(guò)程更人性化、更易使用。借助PAT工具良好的擴(kuò)展性，可方便對(duì)網(wǎng)絡(luò)系統(tǒng)進(jìn)行實(shí)時(shí)性建模。

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

本文首先介紹了模型驗(yàn)證的概念與當(dāng)前的問(wèn)題，并總結(jié)了三種網(wǎng)絡(luò)實(shí)時(shí)性模型的驗(yàn)證方法和主流的實(shí)時(shí)性驗(yàn)證工具，對(duì)其優(yōu)缺點(diǎn)進(jìn)行了比較，為今后的研究提供有益參考。網(wǎng)絡(luò)安全領(lǐng)域的模型檢測(cè)技術(shù)應(yīng)用越來(lái)越廣泛。保障日益復(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ìng)賽升級(jí)[J].網(wǎng)絡(luò)空間安全，2018，01：1-4.

[2] 張修康，金春華，白瑩.應(yīng)對(duì)網(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].國(guó)防科學(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] 張軍林，張治國(guó).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.