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.