金志威 田毅 蘆浩 王鵬

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

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

中圖分類號： TN609?34; V243? ? ? ? ? ? ? ? ? ? ?文獻(xiàn)標(biāo)識碼： A? ? ? ? ? ? ? ? ? ? ?文章編號： 1004?373X（2019）16?0006?04

0? 引? 言

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

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

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

1? 模型檢測方法

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

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

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

2? 基于模型檢測的補(bǔ)充驗(yàn)證

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

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

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

3? 案例實(shí)施

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

3.1? 案例描述

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

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

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

3.2? 模型檢測工具

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

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

3.3? 模型搭建

3.3.1? 模型檢測算法

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

3.3.2? 模型抽象

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

將上述定義代入PCI總線從接口的狀態(tài)機(jī)模塊中，其狀態(tài)轉(zhuǎn)移過程描述如圖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總線的配置、讀、寫等事務(wù)操作狀態(tài)。

3.4? 結(jié)果分析

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

通過分析其他檢測結(jié)果發(fā)現(xiàn)，PCI狀態(tài)機(jī)模塊中的所有狀態(tài)轉(zhuǎn)移路徑均為正確，實(shí)現(xiàn)了對狀態(tài)轉(zhuǎn)移覆蓋的補(bǔ)充驗(yàn)證。在模型檢測過程中，當(dāng)存在錯(cuò)誤的狀態(tài)轉(zhuǎn)移路徑時(shí)，工具會(huì)自動(dòng)生成不滿足系統(tǒng)屬性的反例，即說明模型或?qū)傩源嬖谌毕?。通過分析定位錯(cuò)誤后，設(shè)計(jì)人員和驗(yàn)證人員進(jìn)行修改，最終實(shí)現(xiàn)設(shè)計(jì)及驗(yàn)證的目標(biāo)。

4? 結(jié)? 語

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

參考文獻(xiàn)

[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] 林惠民，張文輝.模型檢測：理論、方法與應(yīng)用[J].電子學(xué)報(bào)，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] 化希耀，蘇博妮，陳立平，等.模型檢測技術(shù)研究綜述[J].塔里木大學(xué)學(xué)報(bào)，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.