形式化方法在机载电子硬件研制中的应用研究  

Research of airborne electronic hardware design processes based on formal methods of NuXMV

作　　者：金志威[1] 刘万和[2] 薛茜男[1] 田毅[1] 

机构地区：[1]中国民航大学天津市民用航空器适航与维修重点实验室,天津300300 [2]中国民航大学安全科学与工程学院,天津300300

出　　处：《电子技术应用》2015年第6期143-146,共4页Application of Electronic Technique

基　　金：国家自然科学基金委员会与中国民用航空局联合资助项目(U1333120);中央高校基本科研业务费项目(3122014C025);中国民航大学科研启动基金项目(2012QD26X)

摘　　要：详细设计规范是机载电子硬件适航性设计流程中的关键文档。通过对形式化方法特点分析,给出基于模型检验的设计规范提取步骤,以提高设计的正确性和完整性。以ARINC429总线传输模块设计为例,基于形式化方法完成正向设计过程。试验结果表明,基于形式化方法的设计流程能够有效帮助制定详细设计规范并在后期提高验证效率,进而缩减研制周期。The critical design document in airborne electronic hardware design processes is detailed design specification. This paper analyzes the formal methods character, and then abstracts a process for detailed design specification to develop design＇s cor- rectness and completeness. Taking ARINC429 bus transmission module design as an example, it completes the forward design pro- cess based on formal methods. The result shows that the design process based on formal methods is useful for detailed design spec- ification and improving the efficiency of verification, so as to reduce the development cycle.

关 键 词：模型检验 形式化方法 NuXMV 机载电子硬件 

分 类 号：TP305[自动化与计算机技术—计算机系统结构]