基于模型检测的机载电子硬件验证方法研究

来源：核心期刊咨询网时间：12

摘要：摘 要： 模型检测技术已广泛应用于计算机硬件、通信協议、控制系统等领域，在民用航空领域如何采用模型检测技术开展硬件符合性验证，成为设计及验证人员待解决的问题。文中介绍模型检测方法的验证机理，并提出使用该方法作为机载电子硬件的补充验证方案。以P

　　摘 要： 模型检测技术已广泛应用于计算机硬件、通信協议、控制系统等领域，在民用航空领域如何采用模型检测技术开展硬件符合性验证，成为设计及验证人员待解决的问题。文中介绍模型检测方法的验证机理，并提出使用该方法作为机载电子硬件的补充验证方案。以PCI总线状态机模块作为验证对象，开展模型检测补充验证，确定了状态机各状态转移路径的正确，说明了该方法的合理性。

　　关键词： 民用航空; 模型检测; 机载电子硬件; 验证方案; PCI总线; 状态机

　　《深圳大学学报(理工版)》植根于深圳这块沃土，在创建自主创新型国家的宏伟目标中，日益受到海内外的关注。英国《科学文摘》(INSPEC)、荷兰《Scopus》、中国《中文核心期刊要目总览》综合性科学技术类核心期刊。

　　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总线对从设备的各操作事务，包括配置、读、写、重试、错误中断等。

转载请注明来自：http://www.qikan2017.com/lunwen/dzi/14659.html