基于模型检测的机载电子硬件验证方法研究
2019-08-23金志威田毅芦浩王鹏
金志威 田毅 芦浩 王鹏
摘 要： 模型检测技术已广泛应用于计算机硬件、通信協议、控制系统等领域，在民用航空领域如何采用模型检测技术开展硬件符合性验证，成为设计及验证人员待解决的问题。文中介绍模型检测方法的验证机理，并提出使用该方法作为机载电子硬件的补充验证方案。以PCI总线状态机模块作为验证对象，开展模型检测补充验证，确定了状态机各状态转移路径的正确，说明了该方法的合理性。
关键词： 民用航空; 模型检测; 机载电子硬件; 验证方案; PCI总线; 状态机
中图分类号： TN609?34; V243 文献标识码： A 文章编号： 1004?373X（2019）16?0006?04
0 引 言
随着科技的飞速发展，微电子技术的应用不断延伸到生活中的各个领域。由于其具有低功耗、高性能、高容量等优良特性，微电子技术在产品中实现信息存储、处理以及加工等重要功能。然而随着系统复杂度的不断增加，为了确保设计的安全性及可靠性，如何进行全面且完整的验证给验证工程师带来了巨大的挑战。
在民用航空等高安全性领域，电子硬件的功能覆盖率及代码覆盖率是衡量设计及验证工作的重要指标[1]。在高安全性等级的设计中，验证人员将花费大量的时间搭建验证平台，编制测试激励来获取100%的覆盖率数据。特别对于带有多状态、路径复杂的状态机设计，往往大量的测试激励也难以覆盖到所有的状态路径。由此一方面大幅度增加了验证人员的工作量，延长了项目的研制生命周期;另一方面从适航角度讲，对于A/B级机载电子硬件，在审查过程中若存在未覆盖到的状态转移路径，则无法满足代码覆盖的要求[2]。因此，有必要在验证过程中，针对复杂状态机采用更加有效的方法进行补充验证，提高项目的验证效率，进而提高设计的安全性指标。
本文将讨论模型检测方法在机载电子硬件验证过程中的应用，并以PCI总线从端口设计为例，利用模型检测工具NuXMV实践相关方法。实验结果表明，在机载电子硬件验证过程中，对状态机使用模型检测方法搭建模型，能够有效对状态机进行验证，对难以获取状态转移覆盖度的设计进行补充验证，有效提高了验证效率并确保了设计的安全及可靠。
1 模型检测方法
模型检测是通过搜索待验证系统模型的有穷状态空间来检验系统的行为是否具备预测属性的一种自动验证技术。该方法由E. A. Emerson等于1981年首次提出[3]，目前已经被广泛应用于计算机、软件、通信、微电子等多个领域。
模型检测基本思想是：假设模型Μ是一个有穷状态转换系统的抽象，属性φ是该系统的时态逻辑公式描述。可使用公式Μ╞φ来表示模型M是属性φ的一个模型，进而说明系统满足了所有期望属性。将Μ和φ输入模型检查器，当Μ╞ φ语义推导成立，模型检查器输出“TRUE”，否则输出“FALSE” [4]。由于模型检测使用系统描述语言对模型进行抽象，并且使用CTL（分支时序逻辑）或LTL[5]（线性时序逻辑）模型检测算法来抽象系统属性，因此该方法具有检验过程自动化、无需外加测试激励、检测速度快、反例定位准确等特点。
通常可将模型检测过程划分为3个步骤，分别为系统建模、属性描述和算法运行[6]，如图1所示。系统建模：对有穷状态转换系统采用Kripke结构或自动机等状态模型进行模型搭建，获得模型M。属性描述：采用CTL或LTL公式描述系统的属性，获得属性φ;算法运行：将模型M和属性φ输入到模型检测算法（工具）中并运行，对系统进行验证，若Μ╞φ，则输出TRUE，否则给出反例。
2 基于模型检测的补充验证
针对复杂机载电子硬件的设计，RTL层级的验证工作主要包括功能覆盖和代码覆盖两方面。代码覆盖用于检查设计中哪些代码在验证期间被执行过，是否存在冗余代码以及无法达到的路径等情况。功能覆盖也可称为基于需求的覆盖，是代码覆盖的补充，用于衡量验证对象是否实现了设计者所期望的功能。
功能覆盖率的要求需要达到100%，即证明此设计实现了所有功能需求。代码覆盖率根据机载电子硬件的设计保证等级（DAL）的高低有所不同，对于DAL为A和B等级的机载电子硬件，不但要求语句、分支、条件、表达式等覆盖率，还要求状态转移覆盖率达到100%，即应当覆盖到设计中状态机的所有状态转移路径。
图2为基于模型检测的补充验证流程。复杂设计验证中功能覆盖率和代码覆盖率的数据收集是反复迭代的过程。若硬件设计中存在大规模、多状态的有限状态机，当使用传统的验证方法难以收集到100%的状态转移覆盖率时，则可通过模型检测的方式对设计进行补充验证，当其他覆盖率也达到要求之后，则验证工作结束。
3 案例实施
PCI总线是先进的高性能局部总线，可同时支持多个外围设备。该总线不受制于处理器，其主要作用在于为中央处理器及高速外围设备提供一座运输桥梁，提高数据吞吐量。现如今基于PCI总线的VbPCI（Virtual backplane PCI）总线已被霍尼韦尔应用其PC架构中，同时PCI总线被广泛应用在航空测试系统中。
3.1 案例描述
图3所示为PCI从接口的系统框图，由图可知，此硬件设计分为8个功能模块，其核心部分为状态机模块。
IP核的控制状态机模块一方面按照PCI总线协议，结合总线的输入控制信号，经过分析，发送出相应的总线输出信号;另一方面，通过判断PCI总线事务，并结合本地端口的控制信号，完成PCI总线对从设备的各操作事务，包括配置、读、写、重试、错误中断等。
该模块的硬件程序为一个12状态的状态机，状态包括idle（空闲）、config_wait（配置等待）、config_ready（配置准备）、config（配置）、rw_wait（读写等待）、rw_ready（读写准备）、read_wait（读等待）、rw（读写）、last_rw（最后读写）、retry（重试）、abort（停止）和backoff（返回）。通过控制状态机各状态的跳转，完成总线的配置、读、写等操作的使能信号输出，进而实现总线的数据传输。
3.2 模型检测工具
模型检测方法的主要特点是能够自动化验证，因此该方法离不开成熟的模型检测工具的支持。模型检验工具通常要求采用时序逻辑来描述系统的设计规范，利用BDD（二叉判定图）表示电路实现的状态及状态之间的转移关系，通过遍历BDD来检验电路的设计是否满足规范，如果不满足则给出反例[7]。目前可用的工具如Bell实验室的SPIN[8]、瑞士的Uppsala大学和丹麦的Aalborg大学联合开发的UPPAAL[9]、新加坡國立大学PAT小组开发的PAT[10]工具，以及卡内基梅隆大学的SMV，NuSMV[11]及NuXMV等。
本案例将采用NuXMV作为模型检测工具。NuXMV扩展于NuSMV工具，其在算法和验证引擎上进行了进一步提升，支持LTL和CTL描述的所有规范;对于有限状态的情形，NuXMV特点是基于SAT算法的有效验证引擎;通过定义良好的软件体系结构，更方便用户操作[12]，是一款比较常用的模型检测工具。
3.3 模型搭建
3.3.1 模型检测算法
模型检测算法是通过遍历状态空间检测属性在系统模型中是否成立来实现。通常将模型检测算法分为CTL（分支时序逻辑）和LTL（线性时序逻辑）。CTL模型检测算法是采用分支时序逻辑来描述系统的属性。在CTL算法中，通常将系统模型描述为分支结构，在该结构中，“未来”的属性是未知的，会有多种可能发生。LTL算法是采用线性、离散且与自然数同构的时间结构，将时序逻辑与命题逻辑相结合，进而描述系统属性以及系统在执行路径上的性质[13]。
3.3.2 模型抽象
定义 假定Atoms是一组原子命题集合，在Atoms上定义Kripke结构模型M为一个四元组M=
将上述定义代入PCI总线从接口的状态机模块中，其状态转移过程描述如图4所示。FSM状态S={idle， config_wait， config_ready， config， rw_wait， rw_ready， read_wait， rw， last_rw， retry， abort， backoff}。其中：状态{idle}表示空闲;状态{retry}表示重试;状态{abort}表示终止;状态{backoff}表示返回;其他状态分别为PCI总线的配置、读、写等事务操作状态。
3.4 结果分析
使用NuXMV对PCI状态机模块模型进行分析，部分检测结果如图5所示。同样以配置操作为例，其结果输出显示该操作的属性描述为True，证明该条状态转移路径正确。
通过分析其他检测结果发现，PCI状态机模块中的所有状态转移路径均为正确，实现了对状态转移覆盖的补充验证。在模型检测过程中，当存在错误的状态转移路径时，工具会自动生成不满足系统属性的反例，即说明模型或属性存在缺陷。通过分析定位错误后，设计人员和验证人员进行修改，最终实现设计及验证的目标。
4 结 语
模型检测方法由于无需编写测试激励且可自动化开展验证等优点，广泛应用于有穷状态系统的验证过程。在民用航空领域，对于高安全等级的机载复杂电子硬件，当设计中存在大规模状态机时，为了满足代码覆盖要求，使用传统的验证方法将耗费大量的人力及时间。文中以PCI总线状态机模块为研究对象，采用模型检测作为设计的补充验证方法，使用NuXMV模型检测工具对设计开展验证，并获取验证结果。结果表明，采用模型检测方法对设计进行补充验证，能够快速有效地明确状态转移路径的正确性，对状态转移覆盖率进行补充，为验证人员提供了一种新的验证方案。
参考文献
[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] 林惠民，张文辉.模型检测：理论、方法与应用[J].电子学报，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] 化希耀，苏博妮，陈立平，等.模型检测技术研究综述[J].塔里木大学学报，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.
