@inproceedings{2c9415830e9e4b7999f32f89be33d239,
title = "Compositional verification of architectural models",
abstract = "This paper describes a design flow and supporting tools to significantly improve the design and verification of complex cyber-physical systems. We focus on system architecture models composed from libraries of components and complexity-reducing design patterns having formally verified properties. This allows new system designs to be developed rapidly using patterns that have been shown to reduce unnecessary complexity and coupling between components. Components and patterns are annotated with formal contracts describing their guaranteed behaviors and the contextual assumptions that must be satisfied for their correct operation. We describe the compositional reasoning framework that we have developed for proving the correctness of a system design, and provide a proof of the soundness of our compositional reasoning approach. An example based on an aircraft flight control system is provided to illustrate the method and supporting analysis tools.",
keywords = "AADL, Cyber-physical systems, DARPA, META, SysML, compositional verification, design patterns, formal methods, model checking",
author = "Darren Cofer and Andrew Gacek and Steven Miller and Whalen, {Michael W.} and Brian LaValley and Lui Sha",
year = "2012",
doi = "10.1007/978-3-642-28891-3_13",
language = "English (US)",
isbn = "9783642288906",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "126--140",
booktitle = "NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings",
note = "4th NASA Formal Methods Symposium, NFM 2012 ; Conference date: 03-04-2012 Through 05-04-2012",
}