Requirements analysis of a quad-redundant flight control system

John Backes, Darren Cofer, Steven Miller, Michael W. Whalen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationNASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings
EditorsKlaus Havelund, Gerard Holzmann, Rajeev Joshi
PublisherSpringer- Verlag
Pages82-96
Number of pages15
ISBN (Print)9783319175232
DOIs
StatePublished - Jan 1 2015
Event7th International Symposium on NASA Formal Methods, NFM 2015 - Pasadena, United States
Duration: Apr 27 2015Apr 29 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9058
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other7th International Symposium on NASA Formal Methods, NFM 2015
CountryUnited States
CityPasadena
Period4/27/154/29/15

Bibliographical note

Publisher Copyright:
© Springer International Publishing Switzerland 2015.

Fingerprint Dive into the research topics of 'Requirements analysis of a quad-redundant flight control system'. Together they form a unique fingerprint.

Cite this