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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Cofer, D.D., Miller, S.P., Gacek, A.J., Whalen, M.W., LaValley, B., Sha, L., Al-Nayeem, A.: Complexity-Reducing Design Patterns for Cyber-Physical Systems. Air Force Research Laboratory Technical Report AFRL-RZ-WP-TR-2011-2098 (2011)
Kamp, J.A.W.: Tense Logic and the Theory of Order. Ph.D. Thesis, UCLA (1968)
The NuSMV Toolset Users Manual (2005), http://nusmv.irst.itc.it/
McMillan, K.L.: Circular Compositional Reasoning about Liveness. Technical Report 1999-02, Cadence Berkeley Labs, Berkeley CA (1999)
IEEE Standard for Property Specification Language (PSL). IEEE Std 1850-2005 (2005)
Whalen, M., Gacek, A., Cofer, D.: Circular Hierarchical Reasoning using Past Time LTL. Technical Report 2011-1, University of Minnesota Software Engineering Center (2011), http://www.umsec.umn.edu/publications
The Mathworks Inc. Simulink Product Web Site, http://www.mathworks.com/products/simulink
Nam, M.-Y., Pellizzoni, R., Sha, L., Bradford, R.M.: ASIIST: Application Specific I/O Integration Support Tool for Real-Time Bus Architecture Designs. In: 2009 14th IEEE International Conference on Engineering of Complex Computer Systems (June 2009)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 52–66. Springer, Heidelberg (2002)
Gilles, O., Hugues, J.: Expressing and Enforcing User-Defined Constraints of AADL Models. In: Engineering of Complex Computer Systems (ICECCS), pp. 337–342 (2010)
Ölveczky, P.C., Boronat, A., Meseguer, J.: Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude. In: Hatcliff, J., Zucca, E. (eds.) FMOODS/FORTE 2010. LNCS, vol. 6117, pp. 47–62. Springer, Heidelberg (2010)
Jahier, E., Halbwachs, N., Raymond, P., Nicollin, X., Lesens, D.: Virtual Integration of AADL models by a translation into synchronous programs. In: EMSOFT 2007. ACM (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L. (2012). Compositional Verification of Architectural Models. In: Goodloe, A.E., Person, S. (eds) NASA Formal Methods. NFM 2012. Lecture Notes in Computer Science, vol 7226. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28891-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-28891-3_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28890-6
Online ISBN: 978-3-642-28891-3
eBook Packages: Computer ScienceComputer Science (R0)