文獻(xiàn)標(biāo)識(shí)碼： A
文章編號(hào)： 0258-7998(2015)06-0143-04
0 引言
隨著微電子技術(shù)的發(fā)展，人們對(duì)于數(shù)字產(chǎn)品的依賴日益提高。在航空航天、核反應(yīng)堆控制、鐵路信號(hào)等高安全領(lǐng)域，由于系統(tǒng)的復(fù)雜度不斷增加，導(dǎo)致設(shè)計(jì)存在不同程度的安全隱患，為驗(yàn)證工程師帶來了諸多挑戰(zhàn)。
在航空領(lǐng)域，機(jī)載電子硬件的驗(yàn)證工作中經(jīng)常會(huì)發(fā)現(xiàn)待測(cè)設(shè)計(jì)邊界邏輯混亂、時(shí)序錯(cuò)雜以及狀態(tài)轉(zhuǎn)移丟失等問題。在多數(shù)情況下，驗(yàn)證人員難以對(duì)問題進(jìn)行準(zhǔn)確的定位，由此大幅度延長(zhǎng)了設(shè)備的研制生命周期，給研制單位造成非必要的時(shí)間和經(jīng)濟(jì)損失。因此，有必要在項(xiàng)目初期搭建并驗(yàn)證系統(tǒng)架構(gòu)，制定完善的詳細(xì)設(shè)計(jì)規(guī)范，避免研制過程中出現(xiàn)難以修改的錯(cuò)誤，進(jìn)而提高產(chǎn)品的設(shè)計(jì)保證。
本文將討論形式化方法在機(jī)載電子硬件研制過程中的應(yīng)用，并以ARINC429總線傳輸模塊為例，利用模型檢驗(yàn)工具NuXMV實(shí)踐相關(guān)方法。實(shí)驗(yàn)結(jié)果表明，在設(shè)計(jì)初期使用基于NuXMV的形式化方法搭建設(shè)計(jì)模型，能夠有效地對(duì)設(shè)計(jì)進(jìn)行指導(dǎo)，并輔助后期驗(yàn)證活動(dòng)的進(jìn)行，確保設(shè)計(jì)正確的基礎(chǔ)上縮短了研制周期。
1 形式化方法概述
形式化方法借助數(shù)學(xué)中的自動(dòng)機(jī)、邏輯、圖論、代數(shù)等基礎(chǔ)理論來抽象具體的邏輯行為。從工程角度講，形式化方法包括形式化描述(Formal Specification)和形式化驗(yàn)證(Formal Verification)。
形式化描述通過形式語言精確描述電路功能，是設(shè)計(jì)和編制電路的出發(fā)點(diǎn)，也是驗(yàn)證電路是否完整的依據(jù)。通常，通過構(gòu)造系統(tǒng)不同行為特征的計(jì)算模型進(jìn)行系統(tǒng)建模，并且通過定義系統(tǒng)必須滿足的性質(zhì)進(jìn)行屬性描述。
形式化驗(yàn)證是基于已經(jīng)搭建的形式化描述，對(duì)硬件相關(guān)屬性依據(jù)數(shù)學(xué)分析和證明進(jìn)行評(píng)價(jià)，主要有三個(gè)方面：等價(jià)性檢查、模型檢驗(yàn)和定理證明。等價(jià)性檢查主要是對(duì)一個(gè)經(jīng)過變換的設(shè)計(jì)，窮盡地檢查變換前后功能的一致性。模型檢驗(yàn)主要是通過顯式狀態(tài)搜索或隱式不動(dòng)點(diǎn)計(jì)算來驗(yàn)證有窮狀態(tài)或?qū)崟r(shí)系統(tǒng)的屬性。定理證明主要是從系統(tǒng)的公理出發(fā)，使用推理規(guī)則逐步推導(dǎo)出其所期望的特性的證明過程[1]。
等價(jià)性檢查用于證明設(shè)計(jì)的變換沒有產(chǎn)生功能的變換。在整個(gè)設(shè)計(jì)流程中，該方法保證了設(shè)計(jì)規(guī)范在后面行為設(shè)計(jì)、結(jié)構(gòu)設(shè)計(jì)以及物理設(shè)計(jì)中一步一步地實(shí)現(xiàn)和細(xì)化。此外，如果設(shè)計(jì)者要將原來設(shè)計(jì)的功能進(jìn)行必要的修改，等價(jià)性檢查產(chǎn)生的信息可以幫助設(shè)計(jì)者確認(rèn)所做的修改是否達(dá)到了目的。但是，對(duì)于最初規(guī)范的獲得，該方法有一定的局限性。
定理證明就是定義一種數(shù)理邏輯系統(tǒng)（由公理和推理規(guī)則組成），利用這種邏輯語言分別表示被驗(yàn)證的系統(tǒng)和其期望的屬性。由于證明過程中需要的步驟依賴于系統(tǒng)的公理和推理規(guī)則，并且在某種程度上也依賴于其派生定義和中間引理，因此自動(dòng)化程度不高，難以大規(guī)模工程應(yīng)用。
模型檢測(cè)[2，3]是一種自動(dòng)的、基于模型的、屬性驗(yàn)證的處理方法，關(guān)注于時(shí)態(tài)屬性和時(shí)態(tài)演化，從描述的模型開始，檢測(cè)用戶屬性（斷言）對(duì)于該模型是否有效。模型檢測(cè)基本思想是：假設(shè)模型Μ是一個(gè)狀態(tài)轉(zhuǎn)換系統(tǒng)抽象，屬性ф是時(shí)態(tài)邏輯公式表示，以Μ和ф作輸入模型檢查器，當(dāng)Μ╞ф語義推導(dǎo)成立，則模型檢查器輸出“真”，否則輸出“失敗”。由于模型檢驗(yàn)使用規(guī)范的描述語言抽象模型，并且使用LTL[2，4]（線性時(shí)態(tài)邏輯）、CTL[2，5]（計(jì)算樹邏輯）易于抽象相關(guān)屬性，檢驗(yàn)過程具有自動(dòng)運(yùn)行、無外加測(cè)試激勵(lì)、檢驗(yàn)速度快、反例定位準(zhǔn)確的特點(diǎn)，適用于設(shè)計(jì)者獲取設(shè)計(jì)規(guī)范的活動(dòng)。
RTCA/DO-254《機(jī)載電子硬件設(shè)計(jì)保證指南》為機(jī)載電子硬件的研制提供設(shè)計(jì)保證指導(dǎo)，是航空領(lǐng)域電子硬件設(shè)計(jì)和驗(yàn)證工作重要的參考之一[6]。該標(biāo)準(zhǔn)在附錄B中第3.3節(jié)高級(jí)驗(yàn)證方法中對(duì)設(shè)計(jì)保證的驗(yàn)證方法進(jìn)行了介紹，指出可使用形式化驗(yàn)證方法作為機(jī)載電子硬件的符合性驗(yàn)證方法，并說明在生命周期的開始階段使用會(huì)更加有效。
2 基于模型檢驗(yàn)的設(shè)計(jì)規(guī)范提取
一個(gè)標(biāo)準(zhǔn)的機(jī)載電子硬件研制過程包括需求捕獲、概念設(shè)計(jì)、詳細(xì)設(shè)計(jì)、設(shè)計(jì)實(shí)現(xiàn)、試生產(chǎn)五個(gè)步驟。而主要的設(shè)計(jì)規(guī)范提取工作是在概念設(shè)計(jì)到詳細(xì)設(shè)計(jì)階段，保證設(shè)計(jì)規(guī)范中定義的狀態(tài)機(jī)合理、各狀態(tài)可達(dá)、信號(hào)之間的關(guān)系協(xié)調(diào)等。如對(duì)于高級(jí)別（A/B級(jí)）的機(jī)載電子硬件，要求對(duì)于狀態(tài)機(jī)的狀態(tài)轉(zhuǎn)移進(jìn)行完整覆蓋，以保證機(jī)載設(shè)備在異常情況下仍然在一個(gè)可控的狀態(tài)。具體的設(shè)計(jì)規(guī)范提取步驟如圖1所示。
設(shè)計(jì)人員首先根據(jù)需求文檔進(jìn)行概念設(shè)計(jì)，提出基本的狀態(tài)機(jī)、信號(hào)協(xié)議等，形成概念設(shè)計(jì)規(guī)范。然后用CTL或LTL表達(dá)電路的時(shí)序?qū)傩裕肍SM（有限狀態(tài)機(jī)）表示電路的狀態(tài)轉(zhuǎn)換的抽象結(jié)構(gòu)，通過模型檢驗(yàn)工具遍歷FSM來檢驗(yàn)CTL或LTL公式的正確性。若正確，則依據(jù)轉(zhuǎn)移關(guān)系和設(shè)計(jì)約束編制詳細(xì)設(shè)計(jì)規(guī)范；否則，依據(jù)工具給出的反例重新進(jìn)行概念設(shè)計(jì)，并將由此產(chǎn)生的衍生需求反饋到需求捕獲步驟中。待得到較為完整的詳細(xì)設(shè)計(jì)規(guī)范后，設(shè)計(jì)人員進(jìn)入詳細(xì)設(shè)計(jì)流程，開展相應(yīng)的編碼、調(diào)試、模擬、測(cè)試等工作。
3 案例實(shí)施
ARINC429總線是最常用的航空數(shù)據(jù)總線之一，具有結(jié)構(gòu)簡(jiǎn)單、性能穩(wěn)定、抗干擾能力強(qiáng)等特點(diǎn)。本文將以ARINC429總線傳輸模塊為例，實(shí)踐形式化方法在機(jī)載電子硬件研制中的應(yīng)用。
3.1 案例描述
ARINC429總線傳輸模塊是總線控制器的一部分，用于實(shí)現(xiàn)機(jī)載設(shè)備與上位機(jī)的通信，其設(shè)計(jì)架構(gòu)圖如圖2所示。
該模塊主要由兩部分組成，分別為ARINC429數(shù)據(jù)接收及緩存、數(shù)據(jù)判斷及解碼、數(shù)據(jù)轉(zhuǎn)換及校驗(yàn)、RS232數(shù)據(jù)發(fā)送，以及RS232數(shù)據(jù)接收及緩存、數(shù)據(jù)轉(zhuǎn)換及校驗(yàn)、數(shù)據(jù)編碼、ARINC429數(shù)據(jù)發(fā)送。
數(shù)據(jù)在傳輸過程中，應(yīng)考慮數(shù)據(jù)完整性、數(shù)據(jù)傳輸時(shí)延、FIFO存儲(chǔ)深度、數(shù)據(jù)校驗(yàn)等功能需求。應(yīng)按照適航性設(shè)計(jì)流程對(duì)模塊進(jìn)行設(shè)計(jì)，并按照高安全性硬件的驗(yàn)證要求，保證覆蓋度數(shù)據(jù)的滿足。
3.2 模型檢驗(yàn)工具
模型檢驗(yàn)工具通常要求使用時(shí)序邏輯規(guī)范化的描述系統(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]、卡內(nèi)基梅隆大學(xué)的SMV[9]、NuSMV[10]及NuXMV等。
本案例將采用NuXMV作為分析工具。NuXMV是NuSMV在算法和驗(yàn)證引擎上的擴(kuò)展，支持LTL和CTL描述規(guī)范；通過定義良好的軟件體系結(jié)構(gòu)，使得用戶操作更加簡(jiǎn)單[11]，是一款比較常用的形式化驗(yàn)證工具。
3.3 系統(tǒng)模型與屬性
模型檢驗(yàn)是用于對(duì)有限狀態(tài)反應(yīng)系統(tǒng)的自動(dòng)化驗(yàn)證技術(shù)[12]，在這里將對(duì)模型進(jìn)行抽象。
將上述定義帶入ARINC429總線傳輸模塊設(shè)計(jì)過程中，以接收ARINC429、發(fā)送RS232數(shù)據(jù)為例，其狀態(tài)轉(zhuǎn)移過程描述如圖3所示，F(xiàn)SM狀態(tài)S={Idle，Get，Judg，Start，Data_trans，Odd，Ends}。其中初始狀態(tài)由Rst_n復(fù)位后進(jìn)入{Idle}，此時(shí)模塊無操作；狀態(tài){Get}表示數(shù)據(jù)接收；狀態(tài){Judg}表示數(shù)據(jù)判斷；狀態(tài){Start}表示數(shù)據(jù)轉(zhuǎn)換開始；狀態(tài){Data_trans}表示數(shù)據(jù)轉(zhuǎn)換過程；狀態(tài){Odd}表示進(jìn)行數(shù)據(jù)校驗(yàn)；狀態(tài){Ends}表示數(shù)據(jù)轉(zhuǎn)換結(jié)束。
由圖3可知，F(xiàn)SM中的7個(gè)狀態(tài)具備明確的狀態(tài)轉(zhuǎn)移路徑，即在當(dāng)前狀態(tài)下，可根據(jù)特定的狀態(tài)轉(zhuǎn)移條件，轉(zhuǎn)移到下一個(gè)工作狀態(tài)。對(duì)于狀態(tài)轉(zhuǎn)移的限制條件，共有9個(gè)輸入變量，即Σ={cs_en，a_data，data_ready，data_cnt，rec_en，tran_en，per，tran_cnt，data_done}。
(1)系統(tǒng)模型
根據(jù)FSM的轉(zhuǎn)換條件，使用NuXMV工具對(duì)該ARINC429傳輸模塊進(jìn)行建模。建模過程中使用NuXMV的輸入語言，下面為模型的部分程序。
init(state) := idle;
next(state) :=
case
a_data=1 & cs_en=1 & data_ready=0 : get;
a_data=1 & cs_en=1 & data_ready=1 : judg;
per=0 & rec_en=1 & cs_en=1 & tran_en=1 : start;
tran_en=1 & rec_en=0 & tran_cnt < 7 : data_tran;
cs_en=1 & tran_en=1 & tran_cnt=7 : odd;
cs_en=1 & tran_en=1 & data_cnt=3 : end;
TRUE : idle;
esac;
(2)時(shí)態(tài)屬性
依據(jù)上述定義，按照同步FIFO系統(tǒng)模型狀態(tài)轉(zhuǎn)換關(guān)系定義LTL屬性如下：
T1:LTLSPEC G((tran_done_proc.cs_en=0) → X sta_proc.state=idle)
T2:LTLSPEC G((tran_done_proc.cs_en=1 & tran_done_proc.a_data=1 & sta_proc.data_ready=0) →
X sta_proc.state=get)
T3:LTLSPEC G((tran_done_proc.cs_en=1 & tran_done_proc.a_data=1 & sta_proc.data_ready=1 & per_proc.rec_en=0 & data_proc.per=1) → X sta_proc.state=judg)
T4:LTLSPEC G((tran_done_proc.cs_en=1 & tran_done_proc.a_data =1 & sta_proc.data_ready=1 & data_proc.per=0 & per_proc.rec_en=1 & tran_proc.tran_en=0) → X sta_proc.state=start)
T5:LTLSPEC G((tran_done_proc.cs_en=1 & tran_proc.tran_en=1 & per_proc.rec_en=1 & sta_proc.tran_cnt < 7) → X sta_proc.state=data_tran)
T6:LTLSPEC G((tran_done_proc.cs_en=1 & tran_proc.tran_en=1 & sta_proc.tran_cnt=7) →X sta_proc.state=odd)
T7:LTLSPEC G((tran_done_proc.cs_en=1 & tran_proc.tran_en=1 & sta_proc.data_cnt=3) → X sta_proc.state=end)
T8:LTLSPEC G((tran_done_proc.cs_en=1 & tran_proc.tran_en=1 & sta_proc.data_cnt < 3) → X sta_proc.state=start)
T9:LTLSPEC G((tran_done_proc.cs_en= & tran_proc.data_done= ) → X sta_proc.state=idle)
假設(shè)M=<S，Σ，→，f>是一個(gè)系統(tǒng)模型，λ=st1→st2→…是M中的一條轉(zhuǎn)移路徑，f、p是LTL公式，上述LTL公式中使用的關(guān)系╞包括：
λ╞f→p，當(dāng)且僅當(dāng)只要λ╞f，就有λ╞p；
λ╞X f，當(dāng)且僅當(dāng)λ2╞f；
λ╞G f，當(dāng)且僅當(dāng)對(duì)所有i≥1，λi╞f。
3.4 結(jié)果分析
使用NuXMV對(duì)ARINC429傳輸模塊模型進(jìn)行分析，檢驗(yàn)結(jié)果如圖4所示。根據(jù)模型檢驗(yàn)結(jié)果分析發(fā)現(xiàn)，文中描述的系統(tǒng)和ARINC429傳輸模塊關(guān)鍵屬性表述是正確的。在檢驗(yàn)階段，當(dāng)系統(tǒng)模型不滿足系統(tǒng)要求時(shí)，NuXMV會(huì)自動(dòng)生成不滿足系統(tǒng)屬性的反例，這些反例反映出模型或?qū)傩源嬖谌毕荩O(shè)計(jì)者可以根據(jù)反例進(jìn)行修改以滿足模型檢驗(yàn)的運(yùn)行。
依照該模型編寫詳細(xì)設(shè)計(jì)規(guī)范，并使用硬件描述語言（HDL）編碼，最終完成ARINC429傳輸模塊的設(shè)計(jì)。通過使用QuestaSim仿真工具對(duì)設(shè)計(jì)搭建驗(yàn)證平臺(tái)（TestBench）進(jìn)行系統(tǒng)功能仿真，仿真結(jié)果表明依據(jù)詳細(xì)設(shè)計(jì)規(guī)范完成的HDL設(shè)計(jì)符合設(shè)計(jì)預(yù)期。
此外，在編寫激勵(lì)測(cè)試過程中，通過在原模型檢驗(yàn)屬性基礎(chǔ)上構(gòu)建反例屬性，由模型檢驗(yàn)分析器提供經(jīng)典反例以達(dá)到提高結(jié)構(gòu)覆蓋率的目的。圖5給出了QuestaSim分析的FSM狀態(tài)轉(zhuǎn)移結(jié)果，圖上的數(shù)字標(biāo)識(shí)在仿真過程中命中的次數(shù)，結(jié)果表明相應(yīng)的設(shè)計(jì)實(shí)現(xiàn)了狀態(tài)機(jī)的100%狀態(tài)轉(zhuǎn)移覆蓋，符合高安全性硬件設(shè)計(jì)的需要。
4 結(jié)語
在適航性設(shè)計(jì)流程中，如何用無歧義的語言編制硬件設(shè)計(jì)規(guī)范是設(shè)計(jì)工作中的難點(diǎn)。文中分析了形式化方法的技術(shù)特點(diǎn)，選用模型檢驗(yàn)技術(shù)來輔助提取硬件的設(shè)計(jì)規(guī)范，并給出了具體的實(shí)施步驟。通過ARINC429傳輸模塊設(shè)計(jì)為例，對(duì)基于模型檢測(cè)的設(shè)計(jì)規(guī)范提取步驟進(jìn)行實(shí)踐，成功完成了設(shè)計(jì)建模以及時(shí)態(tài)邏輯屬性的建立；通過NuXMV工具對(duì)模型進(jìn)行了模型檢驗(yàn)，完成詳細(xì)設(shè)計(jì)規(guī)范；最后使用HDL完成設(shè)計(jì)，并用QuestaSim進(jìn)行仿真，仿真結(jié)果與預(yù)期設(shè)計(jì)一致。案例證明由于形式化方法采用規(guī)范化的語義描述，表述無歧義，得出的規(guī)范與設(shè)計(jì)意圖相同，基于模型檢驗(yàn)技術(shù)的設(shè)計(jì)規(guī)范提取方法利于快速、準(zhǔn)確地實(shí)現(xiàn)設(shè)計(jì)；同時(shí)也表明，構(gòu)建模型可以協(xié)助生成測(cè)試激勵(lì)，提高驗(yàn)證效率。
參考文獻(xiàn)
[1] 郭建.在數(shù)字系統(tǒng)設(shè)計(jì)中斷言驗(yàn)證的研究[D].西安：西安電子科技大學(xué)，2008.
[2] HUTH M，RYAN M.Logic in computer science modelling and reasoning about systems[M].2nd ed.Cambridge：University of Cambridge，2004.
[3] 楊軍，葛海通，鄭飛君，等.一種形式化驗(yàn)證方法：模型檢驗(yàn)[J].浙江大學(xué)學(xué)報(bào)，2006，33(4)：403-407.
[4] 董玲玲，關(guān)永，李曉娟，等.用LTL模型檢驗(yàn)的方法驗(yàn)證SpaceWire檢錯(cuò)機(jī)制[J].計(jì)算機(jī)工程與應(yīng)用，2012，48(22)：88-94.
[5] 蘇開樂，駱翔宇，呂關(guān)鋒，等.符號(hào)化模型檢測(cè)CTL[J].計(jì)算機(jī)學(xué)報(bào)，2005，28(11)：1798-1806.
[6] RTCA.DO-254 design assurance guidance for airborne electronic hardware[S].SC-180.Washington，DC.：RTCA，Inc.，2000：27-28.
[7] 羅莉，歐國(guó)東.異步FIFO的模型檢驗(yàn)方法[J].計(jì)算機(jī)科學(xué)，2012，39(3)：268-270.
[8] HOLZMANN G J，PELED D.The state of spin[C].Proceedings of the 8th International Conference on Computer-Aided Verification，1996，New Brunswick，NJ，USA，Berlin：Springer，2007.
[9] MCMILLAN K L.Getting started with SMV[M/OL].Berkeley：Candence Berkeley Labs.，(1998)[2015].http：//www.cs.indiana.edu/classes/p515/readings/smv/CadenceSMV-docs/smv/tutorial/.
[10] BRINKSMA E，LARSEN K G.Computer aided verification[C]:14th International Conference，CAV 2002 Copenhagen，Denmark，July 27-31，2002 Proceedings.Berlin：Springer，2002.
[11] 劉博，李蜀瑜.基于NuSMV的AADL行為模型驗(yàn)證的探究[J].計(jì)算機(jī)技術(shù)與發(fā)展，2012，22(2)：110-113.
[12] 魏小勇.符號(hào)模型驗(yàn)證的研究[D].西安：西安理工大學(xué)，2008.