| 基于NuSMV的AADL模型形式化验证技术 |
| |
| 引用本文： | 刘畅,蒋永平,马春燕,张涛.基于NuSMV的AADL模型形式化验证技术[J].航空学报,2022,43(3):451-466. |
| |
| 作者姓名： | 刘畅 蒋永平 马春燕 张涛 |
| |
| 作者单位： | 中国航空无线电电子研究所,上海 200233,西北工业大学软件学院,西安 710072 |
| |
| 基金项目： | 航空科学基金(20175553028,20185853038,201907053004)~~； |
| |
| 摘 要： | 结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言，在航空航天领域广泛被应用。为验证AADL模型的任务关键属性和系统行为的正确性，提出基于NuSMV(新符号模型检查器)的AADL模型形式化验证方法。首先，覆盖AADL模型的所有软件构件和行为特征，提出了AADL模型到NuSMV模型的映射规则和转换算法；其次，采用图同构方法分析了转换算法的正确性；然后，在NuSMV模型中采用时态逻辑公式对AADL模型中待验证属性进行描述，以验证AADL模型中安全性、活性和嵌套模态配置的正确性；最后，以飞行控制系统为例，详细阐释了基于NuSMV的AADL模型形式化验证方法，并给出验证属性的统计信息。
|
| 关 键 词： | AADL 模型 NuSMV 形式化验证 模型转换 飞行控制系统 |
Formal verification technology for AADL models based on NuSMV |
| |
| LIU Chang,JIANG Yongping,MA Chunyan,ZHANG Tao.Formal verification technology for AADL models based on NuSMV[J].Acta Aeronautica et Astronautica Sinica,2022,43(3):451-466. |
| |
| Authors: | LIU Chang JIANG Yongping MA Chunyan ZHANG Tao |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
