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|
|Number of pages||15|
|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
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Other||7th International Symposium on NASA Formal Methods, NFM 2015|
|Period||4/27/15 → 4/29/15|
Bibliographical notePublisher Copyright:
© Springer International Publishing Switzerland 2015.