四余度飞行控制系统需求分析
Requirements Analysis of a Quad-Redundant Flight Control System
摘要：
在本文中，我们详细介绍了我们的努力，形式化和证明的四余度飞行控制系统（QFCS）在美国宇航局的运输类模型（TCM）的要求。我们使用的组合方法与假设保证合同，对应于嵌入在AADL系统架构模型的软件组件的要求。这种方法的目的是利用验证工作和工件，已经在航空电子领域的典型软件验证过程的一部分。我们的方法是支持AADL附件，允许规格的合同，以及一个工具，称为AGREE，用于执行成分验证。本文的目标是显示的组合验证方法应用于一个现实的航空电子系统的好处，并证明在执行这种分析的AGREE工具的有效性。
英文摘要：
In this paper we detail our effort to formalize and prove requirements for the Quad-redundant Flight Control System (QFCS) within NASA's Transport Class Model (TCM). We use a compositional approach with assume-guarantee contracts that correspond to the requirements for software components embedded in an AADL system architecture model. This approach is designed to exploit the verification effort and artifacts that are already part of typical software verification processes in the avionics domain. Our approach is supported by an AADL annex that allows specification of contracts along with a tool, called AGREE, for performing compositional verification. The goal of this paper is to show the benefits of a compositional verification approach applied to a realistic avionics system and to demonstrate the effectiveness of the AGREE tool in performing this analysis.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
