金志威 田毅 蘆浩 王鵬

摘? 要： 模型檢測技術已廣泛應用于計算機硬件、通信協(xié)議、控制系統(tǒng)等領域，在民用航空領域如何采用模型檢測技術開展硬件符合性驗證，成為設計及驗證人員待解決的問題。文中介紹模型檢測方法的驗證機理，并提出使用該方法作為機載電子硬件的補充驗證方案。以PCI總線狀態(tài)機模塊作為驗證對象，開展模型檢測補充驗證，確定了狀態(tài)機各狀態(tài)轉移路徑的正確，說明了該方法的合理性。

關鍵詞： 民用航空; 模型檢測; 機載電子硬件; 驗證方案; PCI總線; 狀態(tài)機

中圖分類號： TN609?34; V243? ? ? ? ? ? ? ? ? ? ?文獻標識碼： A? ? ? ? ? ? ? ? ? ? ?文章編號： 1004?373X（2019）16?0006?04

0? 引? 言

隨著科技的飛速發(fā)展，微電子技術的應用不斷延伸到生活中的各個領域。由于其具有低功耗、高性能、高容量等優(yōu)良特性，微電子技術在產品中實現(xiàn)信息存儲、處理以及加工等重要功能。然而隨著系統(tǒng)復雜度的不斷增加，為了確保設計的安全性及可靠性，如何進行全面且完整的驗證給驗證工程師帶來了巨大的挑戰(zhàn)。

在民用航空等高安全性領域，電子硬件的功能覆蓋率及代碼覆蓋率是衡量設計及驗證工作的重要指標[1]。在高安全性等級的設計中，驗證人員將花費大量的時間搭建驗證平臺，編制測試激勵來獲取100%的覆蓋率數(shù)據(jù)。特別對于帶有多狀態(tài)、路徑復雜的狀態(tài)機設計，往往大量的測試激勵也難以覆蓋到所有的狀態(tài)路徑。由此一方面大幅度增加了驗證人員的工作量，延長了項目的研制生命周期;另一方面從適航角度講，對于A/B級機載電子硬件，在審查過程中若存在未覆蓋到的狀態(tài)轉移路徑，則無法滿足代碼覆蓋的要求[2]。因此，有必要在驗證過程中，針對復雜狀態(tài)機采用更加有效的方法進行補充驗證，提高項目的驗證效率，進而提高設計的安全性指標。

本文將討論模型檢測方法在機載電子硬件驗證過程中的應用，并以PCI總線從端口設計為例，利用模型檢測工具NuXMV實踐相關方法。實驗結果表明，在機載電子硬件驗證過程中，對狀態(tài)機使用模型檢測方法搭建模型，能夠有效對狀態(tài)機進行驗證，對難以獲取狀態(tài)轉移覆蓋度的設計進行補充驗證，有效提高了驗證效率并確保了設計的安全及可靠。

1? 模型檢測方法

模型檢測是通過搜索待驗證系統(tǒng)模型的有窮狀態(tài)空間來檢驗系統(tǒng)的行為是否具備預測屬性的一種自動驗證技術。該方法由E. A. Emerson等于1981年首次提出[3]，目前已經被廣泛應用于計算機、軟件、通信、微電子等多個領域。

模型檢測基本思想是：假設模型Μ是一個有窮狀態(tài)轉換系統(tǒng)的抽象，屬性φ是該系統(tǒng)的時態(tài)邏輯公式描述。可使用公式Μ╞φ來表示模型M是屬性φ的一個模型，進而說明系統(tǒng)滿足了所有期望屬性。將Μ和φ輸入模型檢查器，當Μ╞ φ語義推導成立，模型檢查器輸出“TRUE”，否則輸出“FALSE” [4]。由于模型檢測使用系統(tǒng)描述語言對模型進行抽象，并且使用CTL（分支時序邏輯）或LTL[5]（線性時序邏輯）模型檢測算法來抽象系統(tǒng)屬性，因此該方法具有檢驗過程自動化、無需外加測試激勵、檢測速度快、反例定位準確等特點。

通?？蓪⒛Ｐ蜋z測過程劃分為3個步驟，分別為系統(tǒng)建模、屬性描述和算法運行[6]，如圖1所示。系統(tǒng)建模：對有窮狀態(tài)轉換系統(tǒng)采用Kripke結構或自動機等狀態(tài)模型進行模型搭建，獲得模型M。屬性描述：采用CTL或LTL公式描述系統(tǒng)的屬性，獲得屬性φ;算法運行：將模型M和屬性φ輸入到模型檢測算法（工具）中并運行，對系統(tǒng)進行驗證，若Μ╞φ，則輸出TRUE，否則給出反例。

2? 基于模型檢測的補充驗證

針對復雜機載電子硬件的設計，RTL層級的驗證工作主要包括功能覆蓋和代碼覆蓋兩方面。代碼覆蓋用于檢查設計中哪些代碼在驗證期間被執(zhí)行過，是否存在冗余代碼以及無法達到的路徑等情況。功能覆蓋也可稱為基于需求的覆蓋，是代碼覆蓋的補充，用于衡量驗證對象是否實現(xiàn)了設計者所期望的功能。

功能覆蓋率的要求需要達到100%，即證明此設計實現(xiàn)了所有功能需求。代碼覆蓋率根據(jù)機載電子硬件的設計保證等級（DAL）的高低有所不同，對于DAL為A和B等級的機載電子硬件，不但要求語句、分支、條件、表達式等覆蓋率，還要求狀態(tài)轉移覆蓋率達到100%，即應當覆蓋到設計中狀態(tài)機的所有狀態(tài)轉移路徑。

圖2為基于模型檢測的補充驗證流程。復雜設計驗證中功能覆蓋率和代碼覆蓋率的數(shù)據(jù)收集是反復迭代的過程。若硬件設計中存在大規(guī)模、多狀態(tài)的有限狀態(tài)機，當使用傳統(tǒng)的驗證方法難以收集到100%的狀態(tài)轉移覆蓋率時，則可通過模型檢測的方式對設計進行補充驗證，當其他覆蓋率也達到要求之后，則驗證工作結束。

3? 案例實施

PCI總線是先進的高性能局部總線，可同時支持多個外圍設備。該總線不受制于處理器，其主要作用在于為中央處理器及高速外圍設備提供一座運輸橋梁，提高數(shù)據(jù)吞吐量?，F(xiàn)如今基于PCI總線的VbPCI（Virtual backplane PCI）總線已被霍尼韋爾應用其PC架構中，同時PCI總線被廣泛應用在航空測試系統(tǒng)中。

3.1? 案例描述

圖3所示為PCI從接口的系統(tǒng)框圖，由圖可知，此硬件設計分為8個功能模塊，其核心部分為狀態(tài)機模塊。

IP核的控制狀態(tài)機模塊一方面按照PCI總線協(xié)議，結合總線的輸入控制信號，經過分析，發(fā)送出相應的總線輸出信號;另一方面，通過判斷PCI總線事務，并結合本地端口的控制信號，完成PCI總線對從設備的各操作事務，包括配置、讀、寫、重試、錯誤中斷等。

該模塊的硬件程序為一個12狀態(tài)的狀態(tài)機，狀態(tài)包括idle（空閑）、config_wait（配置等待）、config_ready（配置準備）、config（配置）、rw_wait（讀寫等待）、rw_ready（讀寫準備）、read_wait（讀等待）、rw（讀寫）、last_rw（最后讀寫）、retry（重試）、abort（停止）和backoff（返回）。通過控制狀態(tài)機各狀態(tài)的跳轉，完成總線的配置、讀、寫等操作的使能信號輸出，進而實現(xiàn)總線的數(shù)據(jù)傳輸。

3.2? 模型檢測工具

模型檢測方法的主要特點是能夠自動化驗證，因此該方法離不開成熟的模型檢測工具的支持。模型檢驗工具通常要求采用時序邏輯來描述系統(tǒng)的設計規(guī)范，利用BDD（二叉判定圖）表示電路實現(xiàn)的狀態(tài)及狀態(tài)之間的轉移關系，通過遍歷BDD來檢驗電路的設計是否滿足規(guī)范，如果不滿足則給出反例[7]。目前可用的工具如Bell實驗室的SPIN[8]、瑞士的Uppsala大學和丹麥的Aalborg大學聯(lián)合開發(fā)的UPPAAL[9]、新加坡國立大學PAT小組開發(fā)的PAT[10]工具，以及卡內基梅隆大學的SMV，NuSMV[11]及NuXMV等。

本案例將采用NuXMV作為模型檢測工具。NuXMV擴展于NuSMV工具，其在算法和驗證引擎上進行了進一步提升，支持LTL和CTL描述的所有規(guī)范;對于有限狀態(tài)的情形，NuXMV特點是基于SAT算法的有效驗證引擎;通過定義良好的軟件體系結構，更方便用戶操作[12]，是一款比較常用的模型檢測工具。

3.3? 模型搭建

3.3.1? 模型檢測算法

模型檢測算法是通過遍歷狀態(tài)空間檢測屬性在系統(tǒng)模型中是否成立來實現(xiàn)。通常將模型檢測算法分為CTL（分支時序邏輯）和LTL（線性時序邏輯）。CTL模型檢測算法是采用分支時序邏輯來描述系統(tǒng)的屬性。在CTL算法中，通常將系統(tǒng)模型描述為分支結構，在該結構中，“未來”的屬性是未知的，會有多種可能發(fā)生。LTL算法是采用線性、離散且與自然數(shù)同構的時間結構，將時序邏輯與命題邏輯相結合，進而描述系統(tǒng)屬性以及系統(tǒng)在執(zhí)行路徑上的性質[13]。

3.3.2? 模型抽象

定義 假定Atoms是一組原子命題集合，在Atoms上定義Kripke結構模型M為一個四元組M=。其中：S={st1，st2，…，stn}是一個有限狀態(tài)集合;Σ={input1，input2，…，inputn}是一個有限輸入集合，可以是狀態(tài)或是其他變量;“→”表示全部狀態(tài)轉移關系，即對[?] "st∈S都[?]st′∈S，滿足st→st′;?表示對所有原子命題的一個真賦值 [14]，即?：S→p（Atoms）。

將上述定義代入PCI總線從接口的狀態(tài)機模塊中，其狀態(tài)轉移過程描述如圖4所示。FSM狀態(tài)S={idle， config_wait， config_ready， config， rw_wait， rw_ready， read_wait， rw， last_rw， retry， abort， backoff}。其中：狀態(tài){idle}表示空閑;狀態(tài){retry}表示重試;狀態(tài){abort}表示終止;狀態(tài){backoff}表示返回;其他狀態(tài)分別為PCI總線的配置、讀、寫等事務操作狀態(tài)。

3.4? 結果分析

使用NuXMV對PCI狀態(tài)機模塊模型進行分析，部分檢測結果如圖5所示。同樣以配置操作為例，其結果輸出顯示該操作的屬性描述為True，證明該條狀態(tài)轉移路徑正確。

通過分析其他檢測結果發(fā)現(xiàn)，PCI狀態(tài)機模塊中的所有狀態(tài)轉移路徑均為正確，實現(xiàn)了對狀態(tài)轉移覆蓋的補充驗證。在模型檢測過程中，當存在錯誤的狀態(tài)轉移路徑時，工具會自動生成不滿足系統(tǒng)屬性的反例，即說明模型或屬性存在缺陷。通過分析定位錯誤后，設計人員和驗證人員進行修改，最終實現(xiàn)設計及驗證的目標。

4? 結? 語

模型檢測方法由于無需編寫測試激勵且可自動化開展驗證等優(yōu)點，廣泛應用于有窮狀態(tài)系統(tǒng)的驗證過程。在民用航空領域，對于高安全等級的機載復雜電子硬件，當設計中存在大規(guī)模狀態(tài)機時，為了滿足代碼覆蓋要求，使用傳統(tǒng)的驗證方法將耗費大量的人力及時間。文中以PCI總線狀態(tài)機模塊為研究對象，采用模型檢測作為設計的補充驗證方法，使用NuXMV模型檢測工具對設計開展驗證，并獲取驗證結果。結果表明，采用模型檢測方法對設計進行補充驗證，能夠快速有效地明確狀態(tài)轉移路徑的正確性，對狀態(tài)轉移覆蓋率進行補充，為驗證人員提供了一種新的驗證方案。

參考文獻

[1] MINER P S， CARRENO V A， MALEKPOUR M， et al. A case?study application of RTCA DO?254： design assurance guidance for airborne electronic hardware [C]// Proceedings of 19th Digital Avionics Systems Conference. Philadelphia： IEEE， 2000： 1?5.

[2] European Aviation Safety Agency. Certification memorandum： development assurance of airborne electronic hardware [EB/OL]. [2011?08?11]. https：//www.easa.europa.eu/sites/default/files/dfu/certification?docs?certification?memorandum?EASA?CM?SWCEH?001?Development?Assurance?of?Airborne?Electronic?Hardware.pdf.

[3] CLARKE E M. The birth of model checking [EB/OL]. [2015?11?27]. http：//www.doc88.com/p?9912184698556.html.

[4] CLARKE E M， EMERSON E A， SIFAKIS J. Model checking： algorithmic verification and debugging [J]. Communications of the ACM， 2009， 52（11）： 74?84.

[5] PU F， ZHANG W H. Combining search space partition and search space partition and abstraction for LTL model checking [J]. Science in China series F information sciences， 2007， 50（6）： 793?810.

[6] 林惠民，張文輝.模型檢測：理論、方法與應用[J].電子學報，2002，30（z1）：1907?1912.

LIN Huimin， ZHANG Wenhui. Model detection： theories， techniques and applications [J]. Acta electronica sinica， 2002， 30（S1）： 1907?1912.

[7] 化希耀，蘇博妮，陳立平，等.模型檢測技術研究綜述[J].塔里木大學學報，2013，25（4）：119?124.

HUA Xiyao， SU Boni， CHEN Liping， et al. A survey of model checking [J]. Journal of Tarim University， 2013， 25（4）： 119?124.

[8] HOLZMANN G J， PELED D. The state of spin [C]// Proceedings of the 8th International Conference on Computer?Aided Verification. Berlin： Springer， 1996： 383?389.

[9] BENGTSSON J， LARSEN K， LARSSON F， et al. UPPAAL： a tool suite for automatic verification of real?time systems [C]// Proceedings of International Hybrid Systems Workshop. Berlin： Springer， 1995： 232?243.

[10] SUN J， LIU Y， DONG J S， et al. PAT： towards flexible verification under fairness [C]// Proceedings of the 21st International Conference on Computer Aided Verification. Berlin： Springer， 2009： 709?714.

[11] CIMATTI A， CLARKE E， GIUNCHIGLIA F， et al. NuSMV： a new symbolic model checker [J]. International journal on software tools for technology transfer， 2000， 2（4）： 410?425.

[12] CAVADA R， CIMATTI A， DORIGATTI M， et al. The NuXMV symbolic model checker [C]// Proceedings of International Conference on Computer Aided Verification. Cham： Springer， 2014： 334?342.

[13] MAIDI M. The common fragments of CTL and LTL [C]// Proceedings of 41st Annual Symposium on Foundations of Computer Science. Redondo： IEEE， 2000： 643?652.

[14] HUTH M， RYAN M. Logic in computer science： modelling and reasoning about systems [M]. 2nd ed. Cambridge： University of Cambridge， 2004.