基于NuSMV的AADL模型形式化验证技术  

Formal verification technology for AADL models based on NuSMV

作　　者：刘畅[1] 蒋永平 马春燕[2] 张涛[2] LIU Chang;JIANG Yongping;MA Chunyan;ZHANG Tao(China Aeronautical Radio Electronics Research Institute,Shanghai 200233,China;School of Software,Northwestern Polytechnical University,Xi'an 710072,China)

机构地区：[1]中国航空无线电电子研究所,上海200233 [2]西北工业大学软件学院,西安710072

出　　处：《航空学报》2022年第3期443-458,共16页Acta Aeronautica et Astronautica Sinica

基　　金：航空科学基金(20175553028,20185853038,201907053004)。

摘　　要：结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言,在航空航天领域广泛被应用。为验证AADL模型的任务关键属性和系统行为的正确性,提出基于NuSMV(新符号模型检查器)的AADL模型形式化验证方法。首先,覆盖AADL模型的所有软件构件和行为特征,提出了AADL模型到NuSMV模型的映射规则和转换算法;其次,采用图同构方法分析了转换算法的正确性;然后,在NuSMV模型中采用时态逻辑公式对AADL模型中待验证属性进行描述,以验证AADL模型中安全性、活性和嵌套模态配置的正确性;最后,以飞行控制系统为例,详细阐释了基于NuSMV的AADL模型形式化验证方法,并给出验证属性的统计信息。Architecture Analysis and Design Language(AADL)is a modeling language used to describe the architecture and behavior of mission critical embedded system,which is widely used in the aerospace field.To verify the correctness of the key attributes of AADL model and system behavior,this paper studies the formal verification method for the AADL model based on NuSMV(New Symbolic Model Verifier).Firstly,covering all the software components and behavior characteristics of AADL model,mapping rules and transformation algorithm from the AADL model to the NuSMV model are proposed.Secondly,correctness of the transformation algorithm is analyzed by the graph isomorphism method.Then,the temporal logic formula is used to describe the attributes to be verified in the NuSMV model,so as to verify the safety,activity and nested mode configuration in the AADL model.Finally,taking the flight control system as an example,the formal verification method of AADL model based on NuSMV is explained in detail,and the statistical information of verification attributes is given.

关 键 词：AADL模型 NUSMV 形式化验证 模型转换 飞行控制系统 

分 类 号：V328[航空宇航科学与技术—人机与环境工程] TP311[自动化与计算机技术—计算机软件与理论]