0 引言

    隨著微電子技術的發展，人們對于數字產品的依賴日益提高。在航空航天、核反應堆控制、鐵路信號等高安全領域，由于系統的復雜度不斷增加，導致設計存在不同程度的安全隱患，為驗證工程師帶來了諸多挑戰。

    在航空領域，機載電子硬件的驗證工作中經常會發現待測設計邊界邏輯混亂、時序錯雜以及狀態轉移丟失等問題。在多數情況下，驗證人員難以對問題進行準確的定位，由此大幅度延長了設備的研制生命周期，給研制單位造成非必要的時間和經濟損失。因此，有必要在項目初期搭建并驗證系統架構，制定完善的詳細設計規范，避免研制過程中出現難以修改的錯誤，進而提高產品的設計保證。

    本文將討論形式化方法在機載電子硬件研制過程中的應用，并以ARINC429總線傳輸模塊為例，利用模型檢驗工具NuXMV實踐相關方法。實驗結果表明，在設計初期使用基于NuXMV的形式化方法搭建設計模型，能夠有效地對設計進行指導，并輔助后期驗證活動的進行，確保設計正確的基礎上縮短了研制周期。

1 形式化方法概述

    形式化方法借助數學中的自動機、邏輯、圖論、代數等基礎理論來抽象具體的邏輯行為。從工程角度講，形式化方法包括形式化描述(Formal Specification)和形式化驗證(Formal Verification)。

    形式化描述通過形式語言精確描述電路功能，是設計和編制電路的出發點，也是驗證電路是否完整的依據。通常，通過構造系統不同行為特征的計算模型進行系統建模，并且通過定義系統必須滿足的性質進行屬性描述。

    形式化驗證是基于已經搭建的形式化描述，對硬件相關屬性依據數學分析和證明進行評價，主要有三個方面：等價性檢查、模型檢驗和定理證明。等價性檢查主要是對一個經過變換的設計，窮盡地檢查變換前后功能的一致性。模型檢驗主要是通過顯式狀態搜索或隱式不動點計算來驗證有窮狀態或實時系統的屬性。定理證明主要是從系統的公理出發，使用推理規則逐步推導出其所期望的特性的證明過程^[1]。

    等價性檢查用于證明設計的變換沒有產生功能的變換。在整個設計流程中，該方法保證了設計規范在后面行為設計、結構設計以及物理設計中一步一步地實現和細化。此外，如果設計者要將原來設計的功能進行必要的修改，等價性檢查產生的信息可以幫助設計者確認所做的修改是否達到了目的。但是，對于最初規范的獲得，該方法有一定的局限性。

    定理證明就是定義一種數理邏輯系統（由公理和推理規則組成），利用這種邏輯語言分別表示被驗證的系統和其期望的屬性。由于證明過程中需要的步驟依賴于系統的公理和推理規則，并且在某種程度上也依賴于其派生定義和中間引理，因此自動化程度不高，難以大規模工程應用。

    模型檢測^[2，3]是一種自動的、基于模型的、屬性驗證的處理方法，關注于時態屬性和時態演化，從描述的模型開始，檢測用戶屬性（斷言）對于該模型是否有效。模型檢測基本思想是：假設模型Μ是一個狀態轉換系統抽象，屬性ф是時態邏輯公式表示，以Μ和ф作輸入模型檢查器，當Μ╞ф語義推導成立，則模型檢查器輸出“真”，否則輸出“失敗”。由于模型檢驗使用規范的描述語言抽象模型，并且使用LTL^[2，4]（線性時態邏輯）、CTL^[2，5]（計算樹邏輯）易于抽象相關屬性，檢驗過程具有自動運行、無外加測試激勵、檢驗速度快、反例定位準確的特點，適用于設計者獲取設計規范的活動。

    RTCA/DO-254《機載電子硬件設計保證指南》為機載電子硬件的研制提供設計保證指導，是航空領域電子硬件設計和驗證工作重要的參考之一^[6]。該標準在附錄B中第3.3節高級驗證方法中對設計保證的驗證方法進行了介紹，指出可使用形式化驗證方法作為機載電子硬件的符合性驗證方法，并說明在生命周期的開始階段使用會更加有效。

2 基于模型檢驗的設計規范提取

    一個標準的機載電子硬件研制過程包括需求捕獲、概念設計、詳細設計、設計實現、試生產五個步驟。而主要的設計規范提取工作是在概念設計到詳細設計階段，保證設計規范中定義的狀態機合理、各狀態可達、信號之間的關系協調等。如對于高級別（A/B級）的機載電子硬件，要求對于狀態機的狀態轉移進行完整覆蓋，以保證機載設備在異常情況下仍然在一個可控的狀態。具體的設計規范提取步驟如圖1所示。

    設計人員首先根據需求文檔進行概念設計，提出基本的狀態機、信號協議等，形成概念設計規范。然后用CTL或LTL表達電路的時序屬性，用FSM（有限狀態機）表示電路的狀態轉換的抽象結構，通過模型檢驗工具遍歷FSM來檢驗CTL或LTL公式的正確性。若正確，則依據轉移關系和設計約束編制詳細設計規范；否則，依據工具給出的反例重新進行概念設計，并將由此產生的衍生需求反饋到需求捕獲步驟中。待得到較為完整的詳細設計規范后，設計人員進入詳細設計流程，開展相應的編碼、調試、模擬、測試等工作。

3 案例實施

    ARINC429總線是最常用的航空數據總線之一，具有結構簡單、性能穩定、抗干擾能力強等特點。本文將以ARINC429總線傳輸模塊為例，實踐形式化方法在機載電子硬件研制中的應用。

3.1 案例描述

    ARINC429總線傳輸模塊是總線控制器的一部分，用于實現機載設備與上位機的通信，其設計架構圖如圖2所示。

    該模塊主要由兩部分組成，分別為ARINC429數據接收及緩存、數據判斷及解碼、數據轉換及校驗、RS232數據發送，以及RS232數據接收及緩存、數據轉換及校驗、數據編碼、ARINC429數據發送。

    數據在傳輸過程中，應考慮數據完整性、數據傳輸時延、FIFO存儲深度、數據校驗等功能需求。應按照適航性設計流程對模塊進行設計，并按照高安全性硬件的驗證要求，保證覆蓋度數據的滿足。

3.2 模型檢驗工具

    模型檢驗工具通常要求使用時序邏輯規范化的描述系統設計規范，利用BDD（二叉判定圖）表示電路實現的狀態及狀態間的轉移關系，通過遍歷BDD來檢驗電路設計是否滿足規范，如果不滿足則給出反例^[7]。目前可用的工具有Bell實驗室的SPIN^[8]、卡內基梅隆大學的SMV^[9]、NuSMV^[10]及NuXMV等。

    本案例將采用NuXMV作為分析工具。NuXMV是NuSMV在算法和驗證引擎上的擴展，支持LTL和CTL描述規范；通過定義良好的軟件體系結構，使得用戶操作更加簡單^[11]，是一款比較常用的形式化驗證工具。

3.3 系統模型與屬性

    模型檢驗是用于對有限狀態反應系統的自動化驗證技術^[12]，在這里將對模型進行抽象。

    將上述定義帶入ARINC429總線傳輸模塊設計過程中，以接收ARINC429、發送RS232數據為例，其狀態轉移過程描述如圖3所示，FSM狀態S={Idle，Get，Judg，Start，Data_trans，Odd，Ends}。其中初始狀態由Rst_n復位后進入{Idle}，此時模塊無操作；狀態{Get}表示數據接收；狀態{Judg}表示數據判斷；狀態{Start}表示數據轉換開始；狀態{Data_trans}表示數據轉換過程；狀態{Odd}表示進行數據校驗；狀態{Ends}表示數據轉換結束。

    由圖3可知，FSM中的7個狀態具備明確的狀態轉移路徑，即在當前狀態下，可根據特定的狀態轉移條件，轉移到下一個工作狀態。對于狀態轉移的限制條件，共有9個輸入變量，即Σ={cs_en，a_data，data_ready，data_cnt，rec_en，tran_en，per，tran_cnt，data_done}。

    (1)系統模型

    根據FSM的轉換條件，使用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)時態屬性

    依據上述定義，按照同步FIFO系統模型狀態轉換關系定義LTL屬性如下：

    T₁:LTLSPEC G((tran_done_proc.cs_en=0) → X sta_proc.state=idle)

    T₂:LTLSPEC G((tran_done_proc.cs_en=1 & tran_done_proc.a_data=1 & sta_proc.data_ready=0) → 

X sta_proc.state=get)

    T₃: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)

    T₄: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)

    T₅: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)

    T₆:LTLSPEC G((tran_done_proc.cs_en=1 & tran_proc.tran_en=1 & sta_proc.tran_cnt=7) →X sta_proc.state=odd)

    T₇:LTLSPEC G((tran_done_proc.cs_en=1 & tran_proc.tran_en=1 & sta_proc.data_cnt=3) → X sta_proc.state=end)

    T₈:LTLSPEC G((tran_done_proc.cs_en=1 & tran_proc.tran_en=1 & sta_proc.data_cnt < 3) → X sta_proc.state=start)

    T₉:LTLSPEC G((tran_done_proc.cs_en=  & tran_proc.data_done= ) → X sta_proc.state=idle)

    假設M=<S，Σ，→，f>是一個系統模型，λ=s_t1→s_t2→…是M中的一條轉移路徑，f、p是LTL公式，上述LTL公式中使用的關系╞包括：

    λ╞f→p，當且僅當只要λ╞f，就有λ╞p；

    λ╞X f，當且僅當λ²╞f；

    λ╞G f，當且僅當對所有i≥1，λⁱ╞f。

3.4 結果分析

    使用NuXMV對ARINC429傳輸模塊模型進行分析，檢驗結果如圖4所示。根據模型檢驗結果分析發現，文中描述的系統和ARINC429傳輸模塊關鍵屬性表述是正確的。在檢驗階段，當系統模型不滿足系統要求時，NuXMV會自動生成不滿足系統屬性的反例，這些反例反映出模型或屬性存在缺陷，設計者可以根據反例進行修改以滿足模型檢驗的運行。

    依照該模型編寫詳細設計規范，并使用硬件描述語言（HDL）編碼，最終完成ARINC429傳輸模塊的設計。通過使用QuestaSim仿真工具對設計搭建驗證平臺（TestBench）進行系統功能仿真，仿真結果表明依據詳細設計規范完成的HDL設計符合設計預期。

    此外，在編寫激勵測試過程中，通過在原模型檢驗屬性基礎上構建反例屬性，由模型檢驗分析器提供經典反例以達到提高結構覆蓋率的目的。圖5給出了QuestaSim分析的FSM狀態轉移結果，圖上的數字標識在仿真過程中命中的次數，結果表明相應的設計實現了狀態機的100%狀態轉移覆蓋，符合高安全性硬件設計的需要。

4 結語

    在適航性設計流程中，如何用無歧義的語言編制硬件設計規范是設計工作中的難點。文中分析了形式化方法的技術特點，選用模型檢驗技術來輔助提取硬件的設計規范，并給出了具體的實施步驟。通過ARINC429傳輸模塊設計為例，對基于模型檢測的設計規范提取步驟進行實踐，成功完成了設計建模以及時態邏輯屬性的建立；通過NuXMV工具對模型進行了模型檢驗，完成詳細設計規范；最后使用HDL完成設計，并用QuestaSim進行仿真，仿真結果與預期設計一致。案例證明由于形式化方法采用規范化的語義描述，表述無歧義，得出的規范與設計意圖相同，基于模型檢驗技術的設計規范提取方法利于快速、準確地實現設計；同時也表明，構建模型可以協助生成測試激勵，提高驗證效率。

參考文獻 

[1] 郭建.在數字系統設計中斷言驗證的研究[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] 董玲玲，關永，李曉娟，等.用LTL模型檢驗的方法驗證SpaceWire檢錯機制[J].計算機工程與應用，2012，48(22)：88-94.

[5] 蘇開樂，駱翔宇，呂關鋒，等.符號化模型檢測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].計算機技術與發展，2012，22(2)：110-113.

[12] 魏小勇.符號模型驗證的研究[D].西安：西安理工大學，2008.