四重冗余飞行控制系统的需求分析
软件工程
2015-02-12 v1
摘要
在本文中，我们详述了在NASA的运输机级模型（TCM）内形式化并证明四重冗余飞行控制系统（QFCS）需求的工作。我们采用一种组合方法，使用假设-保证契约（assume-guarantee contracts）对应于嵌入在AADL系统架构模型中的软件组件需求。该方法旨在利用已在航空电子领域典型软件验证流程中的验证工作和产物。我们的方法由一个AADL附件支持，该附件允许契约的规约以及一个名为AGREE的工具用于执行组合验证。本文的目标是展示应用于真实航空电子系统的组合验证方法的优势，并证明AGREE工具执行此分析的有效性。
引用
@article{arxiv.1502.03343,
title = {Requirements Analysis of a Quad-Redundant Flight Control System},
author = {John Backes and Darren Cofer and Steven Miller and Mike Whalen},
journal= {arXiv preprint arXiv:1502.03343},
year = {2015}
}
备注
Accepted to NASA Formal Methods 2015