University of Minnesota
Software Engineering Center

You are here

Compositional Verification of Architectural Models

Date of Publication: 
April 2012
Associated Research Groups: 
Publication Files: 
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.
Proceedings of the Fourth NASA Formal Methods Symposium, Norfolk, VA, April 3-5, 2012
@inproceedings{NFM2012:CoGaMiWhLaLu, author = {Darren D. Cofer and Andrew Gacek and Steven P. Miller and Michael W. Whalen and Brian LaValley and Lui Sha}, title = {Compositional Verification of Architectural Models}, booktitle = {Proceedings of the 4th NASA Formal Methods Symposium (NFM 2012)}, volume = {7226}, editor = {Alwyn E. Goodloe and Suzette Person}, location = {Norfolk, VA, USA}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, pages = {126--140}, month = {April}, year = {2012} }