Requirements analysis of a quad-redundant flight control system

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

doi:10.1007/978-3-319-17524-9_7

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 proceeding › Conference contribution

23 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 language	English (US)
Title of host publication	NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings
Editors	Klaus Havelund, Gerard Holzmann, Rajeev Joshi
Publisher	Springer- Verlag
Pages	82-96
Number of pages	15
ISBN (Print)	9783319175232
DOIs	https://doi.org/10.1007/978-3-319-17524-9_7
State	Published - Jan 1 2015
Event	7th International Symposium on NASA Formal Methods, NFM 2015 - Pasadena, United States Duration: Apr 27 2015 → Apr 29 2015

Publication series

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

Other

Other	7th International Symposium on NASA Formal Methods, NFM 2015
Country/Territory	United States
City	Pasadena
Period	4/27/15 → 4/29/15

Bibliographical note

Publisher Copyright:
© Springer International Publishing Switzerland 2015.

Publisher link

10.1007/978-3-319-17524-9_7

Find It

Find It at U of M Libraries

Cite this

Backes, J., Cofer, D., Miller, S., & Whalen, M. W. (2015). Requirements analysis of a quad-redundant flight control system. In K. Havelund, G. Holzmann, & R. Joshi (Eds.), NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings (pp. 82-96). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9058). Springer- Verlag. https://doi.org/10.1007/978-3-319-17524-9_7

Requirements analysis of a quad-redundant flight control system. / Backes, John; Cofer, Darren; Miller, Steven et al.
NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings. ed. / Klaus Havelund; Gerard Holzmann; Rajeev Joshi. Springer- Verlag, 2015. p. 82-96 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9058).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Backes, J, Cofer, D, Miller, S & Whalen, MW 2015, Requirements analysis of a quad-redundant flight control system. in K Havelund, G Holzmann & R Joshi (eds), NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9058, Springer- Verlag, pp. 82-96, 7th International Symposium on NASA Formal Methods, NFM 2015, Pasadena, United States, 4/27/15. https://doi.org/10.1007/978-3-319-17524-9_7

Backes J, Cofer D, Miller S, Whalen MW. Requirements analysis of a quad-redundant flight control system. In Havelund K, Holzmann G, Joshi R, editors, NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings. Springer- Verlag. 2015. p. 82-96. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-17524-9_7

Backes, John ; Cofer, Darren ; Miller, Steven et al. / Requirements analysis of a quad-redundant flight control system. NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings. editor / Klaus Havelund ; Gerard Holzmann ; Rajeev Joshi. Springer- Verlag, 2015. pp. 82-96 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{62388a9430cc467dac20df70e344642c,

title = "Requirements analysis of a quad-redundant flight control system",

abstract = "In this paper we detail our effort to formalize and prove requirements for the Quad-redundant Flight Control System (QFCS) within NASA{\textquoteright}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.",

author = "John Backes and Darren Cofer and Steven Miller and Whalen, {Michael W.}",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 7th International Symposium on NASA Formal Methods, NFM 2015 ; Conference date: 27-04-2015 Through 29-04-2015",

year = "2015",

month = jan,

day = "1",

doi = "10.1007/978-3-319-17524-9_7",

language = "English (US)",

isbn = "9783319175232",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer- Verlag",

pages = "82--96",

editor = "Klaus Havelund and Gerard Holzmann and Rajeev Joshi",

booktitle = "NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings",

}

TY - GEN

T1 - Requirements analysis of a quad-redundant flight control system

AU - Backes, John

AU - Cofer, Darren

AU - Miller, Steven

AU - Whalen, Michael W.

PY - 2015/1/1

Y1 - 2015/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84942568711&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84942568711&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-17524-9_7

DO - 10.1007/978-3-319-17524-9_7

M3 - Conference contribution

AN - SCOPUS:84942568711

SN - 9783319175232

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 82

EP - 96

BT - NASA Formal Methods - 7th International Symposium, NFM 2015, Proceedings

A2 - Havelund, Klaus

A2 - Holzmann, Gerard

A2 - Joshi, Rajeev

PB - Springer- Verlag

T2 - 7th International Symposium on NASA Formal Methods, NFM 2015

Y2 - 27 April 2015 through 29 April 2015

ER -

Requirements analysis of a quad-redundant flight control system

Abstract

Publication series

Other

Bibliographical note

Publisher link

Find It

Other files and links

Fingerprint

Cite this