Requirements Analysis of a Quad-Redundant Flight Control System

TL;DR

This paper presents a formal, compositional verification approach for a quad-redundant flight control system using assume-guarantee contracts within an AADL model, demonstrating its effectiveness with the AGREE tool.

Contribution

It introduces a formal verification method using assume-guarantee contracts in AADL for avionics systems, showcasing its application to a NASA flight control system.

Findings

Successful formalization and verification of QFCS requirements.

Demonstrated benefits of compositional verification in avionics.

Effective use of AGREE tool for system analysis.

Abstract

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.