網絡系統實時性模型的驗證方法綜述

杜澤民 王曉玲 陳宜成

摘 要：互聯網技術的發展和應用在各個生產領域中發揮著越來越積極的作用，但隨著網絡技術應用的深入，網絡系統的實時性成為影響網絡安全的一大因素，因此對網絡模型的通信實時性、威脅分析實時性的驗證成為網絡安全的重要保障。目前，國內外在實時性驗證方面有諸多研究，形成了不同的方法體系。文章把主要的模型實時性驗證方法，從理論和工具角度加以介紹分析，并對各個方法進行了比較。

關鍵詞：網絡安全；實時性；模型驗證；實時性驗證

中圖分類號：TP393.0 文獻標識碼：A

1 引言

在互聯網時代，網絡安全問題是互聯網建設的重要議題，而網絡系統的實時性是網絡安全的重要保證[1]。其中，包括通信的實時性以及威脅分析的實時性等。當網絡受到外界攻擊時，系統應該對相應的問題快速做出反應并處理措施。問題處理完畢后，還應將處理結果在規定的時間內反饋給系統。實時網絡系統的每一個運行過程都是為了能夠保證整個網絡系統各項工作的協調進行。

模型驅動方法面對復雜度、集成性更高的大型系統有著安全性高、開發成本低等優勢。當前的航空、航天控制系統、軍事指揮自動化系統，也逐漸采用基于模型的開發方式，而這類系統對軟件有著應實時性要求，反應時間要控制在幾毫秒以內，而通常還要求保留一定的反應余量。因此，模型驗證在網絡系統的實時性驗證上具有先天優勢。

目前，國內外對模型的功能與正確性驗證研究比較豐富，但是實時性驗證研究并不廣泛。因此，本文將介紹當前實時性驗證所面臨的問題，并重點介紹網絡系統實時性驗證領域的建模方法，并結合這些方法所依托的工具，分析各種方法所面臨的問題，最后針對檢測方法面臨的挑戰提出一些思路。

2 模型驗證方法及面臨的問題

模型檢測首先要對系統建模，選用一種形式化描述方法，將待驗證的系統設計轉化為工具所能接受的模型，比如狀態遷移圖。然后，將系統所要驗證的性質采用形式化的邏輯公式來描述，比如時態邏輯。它能夠描述系統隨著時間變化而引起的行為變化。最后是系統驗證，是通過模型檢測算法對系統模型的狀態空間進行窮盡搜索。如果未發現違反性質描述的狀態，則表明該模型滿足期望的性質，否則給出一個反例路徑，供設計人員參考。

模型驗證方法應用初期，系統的狀態和狀態間的遷移都是采用顯式的狀態遷移圖來表示。這種方法對那些進程數量較少的網絡系統非常實用[2]。而當網絡分量較多時，系統的全局狀態空間會隨著分量的增加，呈指數增長，即產生狀態爆炸問題，狀態爆炸問題是阻礙模型檢測技術應用的瓶頸。

3 建模方法

3.1 最差情況執行時間方法

最差情況執行時間（Worst-Case Execution Time，WCET）是驗證系統實時性的主要方法之一，由奧地利維也納技術大學的Puschner和Burns提出[3]。WCET剛提出時，由于當時計算機軟件需求有限，軟件代碼的執行時間未引起人們的重視。但是，隨著軟件技術的不斷發展，代碼執行時間的越來越復雜，WCET分析技術逐漸受到研究者的重視，目前，國內外有許多機構或大學開始加深對WCET的研究，從2001年開始，國際上每年召開一次WCET研討會。WCET分析技術與計算方法趨于多樣化，從早期的程序標注和語法制導算法發展為基于樹和路徑的計算方法。

WCET分析是指計算給定應用程序代碼片斷執行時間的上限，這里的執行時間定義為執行代碼片斷所花費的處理器時間。在實時系統中，如果想保證系統整體的實時性得到滿足，就必須要求軟件各部分在最差情況下執行的時間也能滿足實時性要求，這樣由部分集成到整體時，整個系統才會滿足實時性的要求。

WCET分析要求安全性和精確性，安全要求不能低估最差執行時間，精確要求能夠給出可以接受的高估值。我們假設程序P的WCET估算值為WCETc （P），P的實際WCET值為WCETA （P），安全性和精確性描述為：

安全性：

WCETc （P） ≥WCETA （P）

精確性：

（WCETc（P） -WCETA（P））/WCETA（P）≤δmax

其中，δmax為系統能夠接受的最大相對誤差。

在程序層次的驗證方面，國防科技大學張曦團隊利用WCET技術對嵌入式實時軟件的驗證進行了深入研究，提出了一種基于WCET分析的模型檢驗方法框架[4]，實現了對源程序的一種實時性驗證方法。

該框架首先對源程序進行WCET分析，其中包括對程序的靜態分析，劃分出程序代碼的路徑集，然后利用WCET工具進行分析程序執行時間上限，分析過程如圖1所示。

利用WCET分析結果對原有的實時約束進行修正，建立系統的實時性模型，同時在系統需求中提取時態邏輯作為系統的性質描述，其中時態邏輯反映了程序應該遵循的先后順序。結合實時性模型與時態邏輯公式通過驗證工具UPPAAL對模型的實時性進行驗證，如果實時性驗證不通過，則返回修改源程序。如圖2所示。

本方法做到了對實時系統的程序層次的驗證，較好地解決了狀態爆炸問題，其中源程序的WCET分析是驗證環節的重要一環，但是當前WCET分析能力有限，比如復雜程序運算時間估算、估值精確度、誤差控制等問題。另外，對源程序的修正可能會引入新的錯誤，并且修正內容無法反映到生成代碼的上層模型中。

3.2 時間自動機建模

為了描述實時系統的時間約束關系，Alur等人提出了時間自動機（Timed Automata，TA）[5]。時間自動機是一類帶有時鐘變量的有限狀態自動機，其數學模型可表述為一個六元組：

Ta= （L，L0，C，A，E，I ）

其中：L是位置的有限集合；l0∈L，為初始位置；C是時鐘有限集合；A是行為的有限集合；"EL×B（C）×A×2c×L是邊的集合，用于描述位置之間的轉移；B（C）是使能條件集合，用于描述發生轉移的時間約束，2c為轉移發生時的時鐘集合；映射I："L→ B（C）" 用于給每個位置指定一個時鐘約束。

用時間自動機網對實時系統建模，首先要對系統進行抽象和簡化，子系統要簡化為有限控制結構、時鐘和變量構成的時間自動機，子系統之間通過通道進行通訊。然后要分析實時系統的信息處理過程，提煉重要的信息處理狀態和事件進行建模。子系統的行為抽象為時間自動機，它們之間的信息交互通過通道來完成，各個時間自動機就組成網絡進而描述整個實時系統的信息處理過程。

時間自動機是一種反映了時間約束的有限狀態轉換圖，通過使用有限的真值時鐘變量表示時間約束，實時系統行為可以通過時間自動機來刻畫，在對實時系統建模后，可以利用時間自動機來驗證系統的實時性。在實時性約束下檢驗狀態是否可達，因此對狀態可達性的研究是時間自動機的驗證技術的關鍵。

時間自動機技術也有不足：構造時間自動機方法很復雜，如果發生錯誤，將導致最終驗證結果的不準確。另外，時間自動機的時間無限制，會導致狀態空間的無限性，隨著系統的復雜程度和進程數量的增加，將無可避免的發生狀態空間爆炸。狀態空間爆炸也是困擾實時系統驗證的最大問題。

但是，典型的時間自動機組成的平面網絡作為模型不易于模擬和調試大規模的工業系統。AIexandre David和Wang Yi提出了一種層疊時間自動機（Hierarchical Timed Automata，HTA）模型，它的狀態既可以是簡單狀態也可以是組合狀態，組合狀態本身就是一個時間自動機。

層疊時間自動機的允許用戶在模擬時，將系統模型的內部結構隱藏或者抽象，并且更容易調試，在處理多層次復雜系統建模時有較大優勢。

3.3 RTCTL模型檢測方法

計算樹邏輯（Computation Tree Logic，CTL）是時序邏輯的一個分支，時序邏輯非常適合于對并發系統進行驗證與刻畫，即使對于復雜的并發系統而言，其刻畫性質依然很強。時序邏輯用于描述系統中的狀態變遷序列，不顯示地表示時間，而是通過語義隱式表達時間。時序邏輯定義時序運算符與邏輯連接詞來表達復雜的時序性質。CTL作為時序邏輯的一個分支主要用來描述計算樹的性質[8]。

CTL公式由路徑量詞與時序運算符組成。路徑量詞用于描述計算樹的分支結構，有兩種路徑量詞：A（對于所有計算路徑）和E（對于某些計算路徑），分別表示從某狀態開始的所有路徑和某些路徑所具有的性質。時序運算符描述某條路徑的具體性質。有5個基本運算符，意義如下：X（下一個狀態）F（將來某狀態）G（將來全局狀態）U（直到……都滿足）R（直到……才滿足）。

CTL有兩種公式：狀態公式與路徑公式。令AP為原子命題集合，狀態公式語法為：

1） 如果p∈AP，則p是一個狀態公式；

2） 如果f和g是狀態公式，則f和f∧g，f∨g是狀態公式；

3） 如果f是一個路徑公式，則Ef和Af是狀態公式。

路徑公式的語法為：

如果f是一狀態公式，則f也是一路徑公式；

如果f和g是路徑公式，則f，f∧g，f∨g，Xf，Ff，Gf，fUg和飛fRg是路徑公式[9]。

檢測實時系統的時間約束的有效方法就是擴充CTL運算符，Emerson等人將CTL邏輯擴充為RTCTL。基本的RTCTL運算符是受限的直到運算符U[a，b]這里[a，b]表示時間間隔，在此間隔內這個性質必須是真的。fU[a，b]g關于某條路徑π=s0，s1…為真，僅當g在此路徑上將來的某個狀態s上滿足，那么f在s0到s上所有狀態都為真，并且s0到s的距離在間隔[a，b]之間。同樣的，CTL中的其他運算符可以增加時間限制來擴展。[a，b]作為一個時間間隔，可以看做是實時性的約束。

RTCTL模型在CTL的基礎上進行了擴充，繼承了CTL模型的精確性，解決了狀態空間爆炸問題，同時加入了時間性約束，可以高效地表達實時性要求。目前有很多工具可以完成基于CTL的模型驗證，RTCTL在實時性驗證中的有很好的應用前景。

通過對時間進行量化分析，可以得到系統的最大、最小時延，完成實時性驗證。

4 模型驗證常用工具

4.1 UPPAAL

UPPAAL是丹麥Aalborg和瑞士Uppsala大學聯合開發[10]，高效實用的基于時間自動機的實時系統模型驗證工具。UPPAAL特別適用于實時系統的安全性和活性的自動驗證。它將每個進程都描述為有限控制結構、時鐘和變量組成的時間自動機，進程之間通過管道共享數據變量進行通信，管道用于保證不同自動機中的兩個轉換同時執行。UPPAAL通過快速搜索機制來驗證時鐘約束和可達性，不僅可以有效地發現設計中出現的錯誤，而且可以清楚地顯示導致錯誤的判定路徑。

UPPAAL擁有圖形用戶界面，主要包括三個部分：編輯器（Editor）、模擬器（Simulator）和驗證器（Verifier）。編輯器用于創建和編輯所要分析的系統；模擬器用于模擬系統模型執行過程可能出現的錯誤，以便在驗證前發現潛在的錯誤；驗證器通過快速搜索機制搜索系統的狀態空間、檢查時鐘約束和響應限制性質。

UPPAAL體系結構如圖3所示。

UPPAAL的引入，簡化了實時系統驗證的工作量，并且增加了驗證系統的可靠性。首先，UPPAAL中時間自動機網絡中每個時間自動機都是相對獨立的，又是可以互相通信的，不需要構造時間自動機的積，避免了構造模型的繁雜。另外，UPPAAL中的模擬器從直觀上可以看到系統的運行過程，發現存在的問題，而驗證器又嚴格的從語義上保證了系統的安全性。UPPAAL在時間和空間上的性能顯著高于其他的實時驗證工具，能夠處理較為復雜的系統。

4.2 NuSMV

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

作為一種通用的模型驗證器，NuSMV的基本運行原理：用戶使用NuSMV提供的輸入語言描述待驗證實時系統和約束性規范，通過NuSMV自動進行，驗證確定模型在規范中是否成立，若不成立輸出No，并給出反例，解析為什么規范在模型中不成立。NuSMV的運行原理如圖4所示。

在功能上，NuSMV支持CTL描述規范，所以RTCTL同樣可以在NuSMV上得到驗證，NuSMV在實時驗證領域占有一席之地。

在結構上，NuSMV定義了一個良好的軟件系統架構，做到了模塊化和開放性，用戶可以自由定制模塊。

在支持性上，NuSMV有豐富的文檔和開放的源碼，作為一種模型檢測的通用平臺，用戶可以在官網和開源社區獲得幫助。

NuSMV的引入，明顯地簡化了實時系統驗證的工作量，研究者提供了更廣闊的研究空間[13]。

4.3 PAT

PAT[14]是由新加坡國立大學PAT研究小組自主開發的一套模型檢測工具，支持并發、網絡實時系統的建模驗證，能夠對多種語言進行模擬驗證和反例生成。PAT是一個可擴展、模塊化的通用架構，其系統框架如圖5所示。

框架分為四層，方便了模塊的擴展，建模驗證過程分為三步：編譯、抽象和驗證。PAT工具具有良好的擴展性，因此可以利用建模層的抽象功能對建模語言進行抽象，避免狀態爆炸。擴展PAT的并行模塊可以方便網絡系統的實時性的建模與驗證。抽象后的語言模塊能夠自動轉化為PAT已經支持的語言，從而簡化系統描述和實現過程，使得建模過程更人性化、更易使用。借助PAT工具良好的擴展性，可方便對網絡系統進行實時性建模。

4 結束語

本文首先介紹了模型驗證的概念與當前的問題，并總結了三種網絡實時性模型的驗證方法和主流的實時性驗證工具，對其優缺點進行了比較，為今后的研究提供有益參考。網絡安全領域的模型檢測技術應用越來越廣泛。保障日益復雜的網絡空間的安全性，是當前研究的難題，建立在嚴格數學理論基礎之上的模型驗證必將在其中占據一席之地。

參考文獻

[1] 劉權，王超.勒索軟件攻擊事件或將引發網絡軍備競賽升級[J].網絡空間安全，2018，01：1-4.

[2] 張修康，金春華，白瑩.應對網絡安全威脅的技術演變[J].網絡空間安全，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分析技術的程序實時性模型檢驗方法研究[D].國防科學技術大學，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模型驗證器實現與分析[D].中山大學，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行為模型驗證的探究[J].計算機技術與發展，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.