Compositional Verification of Architectural Models
Loading...
View/Download File
Persistent link to this item
Statistics
View StatisticsJournal Title
Journal ISSN
Volume Title
Title
Compositional Verification of Architectural Models
Published Date
2012
Publisher
Springer-Verlag
Type
Report
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
Description
Associated research group: Critical Systems Research Group
Related to
Replaces
License
Series/Report Number
Funding information
Isbn identifier
Doi identifier
Previously Published Citation
Proceedings of the Fourth NASA Formal Methods Symposium, Norfolk, VA, April 3-5, 2012
Suggested citation
Cofer, Darren; Gacek, Andrew; Miller, Steven; Whalen, Michael. (2012). Compositional Verification of Architectural Models. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/217393.
Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.