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