航空学报 > 2022, Vol. 43 Issue (3): 325196-325196   doi: 10.7527/S1000-6893.2021.25196

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

刘畅1, 蒋永平2, 马春燕2, 张涛2   

  1. 1. 中国航空无线电电子研究所, 上海 200233;
    2. 西北工业大学 软件学院, 西安 710072
  • 收稿日期:2020-12-31 修回日期:2021-01-27 出版日期:2022-03-15 发布日期:2021-03-09
  • 通讯作者: 马春燕 E-mail:machunyan@nwpu.edu.cn
  • 基金资助:
    航空科学基金(20175553028,20185853038,201907053004)

Formal verification technology for AADL models based on NuSMV

LIU Chang1, JIANG Yongping2, MA Chunyan2, ZHANG Tao2   

  1. 1. China Aeronautical Radio Electronics Research Institute, Shanghai 200233, China;
    2. School of Software, Northwestern Polytechnical University, Xi'an 710072, China
  • Received:2020-12-31 Revised:2021-01-27 Online:2022-03-15 Published:2021-03-09
  • Supported by:
    Aviation Science Foundation (20175553028, 20185853038, 201907053004)

摘要: 结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言,在航空航天领域广泛被应用。为验证AADL模型的任务关键属性和系统行为的正确性,提出基于NuSMV(新符号模型检查器)的AADL模型形式化验证方法。首先,覆盖AADL模型的所有软件构件和行为特征,提出了AADL模型到NuSMV模型的映射规则和转换算法;其次,采用图同构方法分析了转换算法的正确性;然后,在NuSMV模型中采用时态逻辑公式对AADL模型中待验证属性进行描述,以验证AADL模型中安全性、活性和嵌套模态配置的正确性;最后,以飞行控制系统为例,详细阐释了基于NuSMV的AADL模型形式化验证方法,并给出验证属性的统计信息。

关键词: AADL模型, NuSMV, 形式化验证, 模型转换, 飞行控制系统

Abstract: 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.

Key words: AADL model, NuSMV, formal verification, model transformation, flight control system

中图分类号: