Requirements Analysis of a Quad-Redundant Flight Control System. Backes, J., Cofer, D., Miller, S., & Whalen, M. W. In Havelund, K., Holzmann, G., & Joshi, R., editors, NASA Formal Methods, of Lecture Notes in Computer Science, pages 82–96, Cham, 2015. Springer International Publishing. doi abstract bibtex 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.
@inproceedings{backes_requirements_2015,
address = {Cham},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Requirements {Analysis} of a {Quad}-{Redundant} {Flight} {Control} {System}},
isbn = {978-3-319-17524-9},
doi = {10/ghv57c},
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.},
language = {English},
booktitle = {{NASA} {Formal} {Methods}},
publisher = {Springer International Publishing},
author = {Backes, John and Cofer, Darren and Miller, Steven and Whalen, Michael W.},
editor = {Havelund, Klaus and Holzmann, Gerard and Joshi, Rajeev},
year = {2015},
keywords = {Actuator Signal, Compositional Reasoning, Computer Science - Software Engineering, Handling Quality, Model Checker, Requirement Analysis},
pages = {82--96},
}
Downloads: 0
{"_id":"RvH52fK6CJrBakEFL","bibbaseid":"backes-cofer-miller-whalen-requirementsanalysisofaquadredundantflightcontrolsystem-2015","author_short":["Backes, J.","Cofer, D.","Miller, S.","Whalen, M. W."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"Cham","series":"Lecture Notes in Computer Science","title":"Requirements Analysis of a Quad-Redundant Flight Control System","isbn":"978-3-319-17524-9","doi":"10/ghv57c","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.","language":"English","booktitle":"NASA Formal Methods","publisher":"Springer International Publishing","author":[{"propositions":[],"lastnames":["Backes"],"firstnames":["John"],"suffixes":[]},{"propositions":[],"lastnames":["Cofer"],"firstnames":["Darren"],"suffixes":[]},{"propositions":[],"lastnames":["Miller"],"firstnames":["Steven"],"suffixes":[]},{"propositions":[],"lastnames":["Whalen"],"firstnames":["Michael","W."],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Havelund"],"firstnames":["Klaus"],"suffixes":[]},{"propositions":[],"lastnames":["Holzmann"],"firstnames":["Gerard"],"suffixes":[]},{"propositions":[],"lastnames":["Joshi"],"firstnames":["Rajeev"],"suffixes":[]}],"year":"2015","keywords":"Actuator Signal, Compositional Reasoning, Computer Science - Software Engineering, Handling Quality, Model Checker, Requirement Analysis","pages":"82–96","bibtex":"@inproceedings{backes_requirements_2015,\n\taddress = {Cham},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Requirements {Analysis} of a {Quad}-{Redundant} {Flight} {Control} {System}},\n\tisbn = {978-3-319-17524-9},\n\tdoi = {10/ghv57c},\n\tabstract = {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.},\n\tlanguage = {English},\n\tbooktitle = {{NASA} {Formal} {Methods}},\n\tpublisher = {Springer International Publishing},\n\tauthor = {Backes, John and Cofer, Darren and Miller, Steven and Whalen, Michael W.},\n\teditor = {Havelund, Klaus and Holzmann, Gerard and Joshi, Rajeev},\n\tyear = {2015},\n\tkeywords = {Actuator Signal, Compositional Reasoning, Computer Science - Software Engineering, Handling Quality, Model Checker, Requirement Analysis},\n\tpages = {82--96},\n}\n\n","author_short":["Backes, J.","Cofer, D.","Miller, S.","Whalen, M. W."],"editor_short":["Havelund, K.","Holzmann, G.","Joshi, R."],"key":"backes_requirements_2015","id":"backes_requirements_2015","bibbaseid":"backes-cofer-miller-whalen-requirementsanalysisofaquadredundantflightcontrolsystem-2015","role":"author","urls":{},"keyword":["Actuator Signal","Compositional Reasoning","Computer Science - Software Engineering","Handling Quality","Model Checker","Requirement Analysis"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/SilverSylvester","dataSources":["YCBcQPneB9oxahSnp"],"keywords":["actuator signal","compositional reasoning","computer science - software engineering","handling quality","model checker","requirement analysis"],"search_terms":["requirements","analysis","quad","redundant","flight","control","system","backes","cofer","miller","whalen"],"title":"Requirements Analysis of a Quad-Redundant Flight Control System","year":2015}