The Assume Guarantee Reasoning Environment with Application to an Unmanned Helicopter

The Assume Guarantee Reasoning Environment (AGREE) is a compositional analysis tool for systems modeled in the Architecture Analysis and Design Language (AADL). It is compositional in that it can be used to prove properties about each layer of the architecture using properties of its components, continuing down the model hierarchy. The compositional analysis is performed in terms of assume-guarantee contracts that are attached to each component. Assumptions describe the expectations that a component has about its environment, while guarantees describe bounds on the behavior provided by the component. AGREE uses k-induction model checking as its underlying analysis algorithm. In this paper we describe the AGREE annex for adding assume-guarantee behavior contracts to AADL models. We demonstrate the capabilities of the AGREE analysis tool by using it to verify key properties of the command authorization logic for an unmanned helicopter.