Model-based spacecraft fault management design & formal validation
Model-based spacecraft fault management design & formal validation
复制标题
基于模型的航天器故障管理设计
DOI：
10.1109/aero.2015.7119110
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Jean
中科院分区：
文献类型：
--
作者：
Corrina Gibson;M. Bonnici;Jean
将讨论一种基于模型的软件系统逻辑设计和形式化验证方法，以在整个项目生命周期中应用故障管理。我们已经证明，当在项目的设计阶段对故障保护系统行为进行建模时，可以通过执行模型在早期验证预期的行为。在模型中正确地捕获预期的行为可以改进系统设计，以便在实现时更好地定义和完成。此外，执行模型检查会根据正确性属性（断言）正式验证行为模型。从故障保护逻辑行为模型生成和链接其他基于模型的故障管理产品的潜力是项目采用模型驱动设计和保留单一事实来源的关键。在对传统系统建模或需要字典型数据库时，故障管理参数的机器可读导入/导出标准允许飞行软件和基于模型的产品之间更轻松地集成。根据在开发行为模型时是否存在可用的故障管理信息，可以使用用于自动生成模型的方法，该方法减少人为错误并加速建模过程。
A model-based method of software system logical design and formal validation will be discussed for the application of fault management throughout the project lifecycle. We have demonstrated that when modeling fault protection system behaviors during the design phases of a project, the expected behavior can be verified early on by executing the model. Correctly capturing the expected behavior in the model improves the system design so that is better defined and complete upon implementation. Additionally, performing model checking formally validates the behavior model against properties of correctness (assertions). The potential to generate and link additional model-based fault management products from the fault protection logical behavior model is key to projects adopting model driven design and retaining a single source of truth. When modeling heritage systems or if a dictionary-type database is needed, a standard for machine-readable import/export of fault management parameters allows for easier integration between flight software and the model-based products. Depending on if there is fault management information available while developing a behavior model, a method for auto-generating the model can be used that reduces human errors and speeds up the modeling process.