The Assume Guarantee REasoning Environment (AGREE) is a compositional, assume-guarantee-style model checker for AADL models. It is compositional in that it attempts to prove properties about one layer of the architecture using properties allocated to subcomponents. The composition is performed in terms of assumptions and guarantees that are provided for each component. Assumptions describe the expectations the component has on the environment, while guarantees describe bounds on the behavior of the component. AGREE uses k-induction as the underlying algorithm for model checking.
AGREE
Assume Guarantee Reasoning Environment
Publications
- Efficient Generation of Inductive Validity Cores for Safety Properties. E. Ghassabani, A. Gacek, M. Whalen. Foundations of Software Engineering, November 2016.
- On Implementing Real-time Specification Patterns Using Observers. J. Backes, M. Whalen, A. Gacek, J. Komp. NASA Formal Methods Symposium, June 2016.
- Requirements Analysis of a Quad-Redundant Flight Control System. J. Backes, D. Cofer, S. Miller, M. Whalen. NASA Formal Methods Symposium, 2015.
- Towards realizability checking of contracts using theories. A. Gacek, A. Katis, M. Whalen, J. Backes, D. Cofer. NASA Formal Methods, 2015.
- Your "what" is my "how": iteration and hierarchy in system design. M. Whalen, A. Gacek, D. Cofer, A. Murugesan, M. Heimdahl, S. Rayadurgam. IEEE Software, vol. 30, no. 2, pp. 54-60, March-April 2013, doi:10.1109/MS.2012.173.
- Compositional verification of architectural models. D. Cofer, A. Gacek, S. Miller, M. Whalen, B. LaValley, L. Sha. NASA Formal Methods, 2012, pp. 126-140.