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 is integrated into the OSATE AADL model development environment and uses k-induction as the underlying algorithm for the model checking.
The user’s guide for AGREE, including description of the plug-in for OSATE, assume-guarantee concepts, specification language reference manual, and examples is contained in the in-tool help. The source code for the help documentation is contained in the com.rockwellcollins.atc.agree.doc project.
See the main AGREE repository for information regarding developing and maintaining AGREE.
AGREE can be installed on Eclipse by following these steps: