Assume Guarantee REasoning Environment (AGREE)

The Assume Guarantee REasoning Environment (AGREE) is a compositional assume-guarantee-style model checker designed for Architecture Analysis and Design Language (AADL) models. Using k-induction as the underlying model checking algorithm, AGREE compositionally works to prove properties about a layer of the architecture using subcomponent properties. Component level assumptions and guarantees are used to perform the composition, with assumptions describing the component’s expectations of the environment and guarantees describing the bounds of the component’s behavior. 

AGREE is part of the BriefCASE toolchain. To explore and launch this tool within the full workflow, return to the BriefCASE page.