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
- Steal This Drone: DEF CON 29 Aerospace Village Activity. D. Cofer, I. Amundson, E. Barker, E. Hellman, M. Podhradsky, S. Zhuang. DEF CON Aerospace Village, August 2021.
- AADL-Based Safety Analysis Using Formal Methods Applied to Aircraft Digital Systems. D. Stewart, J. Liu, D. Cofer, M. Heimdahl, M. Whalen, M. Peterson. Reliability Engineering and System Safety, September 2021.
- Safety Annex for the Architecture Analysis and Design Language. D. Stewart, J. Liu, D. Cofer, M. Heimdahl, M. Whalen, M. Peterson. Embedded Real Time Systems Conference, January 2020.
- A Formal Approach to Constructing Secure Air Vehicle Software. D. Cofer, A. Gacek, J. Backes, M. Whalen, L. Pike, A. Foltzer, M. Podhradsky, G. Klein, I. Kuz, J. Andronick, G. Heiser, D. Stuart. IEEE Computer Magazine, November 2018.
- The JKind Model Checker. A. Gacek, J. Backes, M. Whalen, L. Wagner, E. Ghassabani. Computer Aided Verification 2018.
- Proof-Based Coverage Metrics for Formal Verification. E. Ghassabani, M. Whalen, M. Heimdahl, A. Gacek, L. Wagner. Automated Software Engineering, October 2017.
- Secure Mathematically-Assured Composition of Control Models. D. Cofer, J. Backes, A. Gacek, D. DaCosta, M. Whalen, I. Kuz, G. Klein, G. Heiser, L. Pike, A. Foltzer, M. Podhradsky, D. Stuart, J. Grahan, B. Wilson. HACMS Final Report, October 2017.
- Architectural Modeling and Analysis for Safety Engineering. D. Stewart, M. Whalen, D. Cofer, M. Heimdahl. International Symposium on Model-Based Safety and Assessment, September 2017.
- Efficient Generation of Inductive Validity Cores for Safety Properties. E. Ghassabani, A. Gacek, M. Whalen. Foundations of Software Engineering, November 2016.
- Requirements and Architectures for Secure Vehicles. M. Whalen, D. Cofer, A. Gacek. IEEE Software 33(4):22-25, June 2016, doi:10.1109/MS.2016.94.
- From Design Contracts to Component Requirements Verification. J. Liu, J. Backes, D. Cofer, A. Gacek. NASA Formal Methods Symposium, June 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.