文章摘要:针对可重构分布式综合模块化航空电子（Distributed Integrated Modular Avionics， DIMA）系统在设计初期缺少仿真与验证手段的问题。首先分析了可重构DIMA软件体系的架构特征以及支持动态重构的层次化通用系统管理（Generic System Management， GSM）的组件功能划分。接下来，使用架构分析与设计语言（Architecture Analysis&Design Language， AADL）及其相关附件对DIMA动态重构的架构基础以及行为细节等要素进行建模。在此基础上，设计了一种基于形式化定义的模型转换规则，该规则将AADL动态重构模型转换成可执行的时间自动机模型。最后，利用模型验证工具UPPAAL验证了可重构DIMA系统逻辑及时序的正确性和不安全控制行为的可达性。结果表明本文提出的仿真与验证方法具有可行性和有效性，并且能够为后续DIMA动态重构的形式化安全性评估提供模型基础。

文章关键词:

项目基金: