ACM SIGAda’s High Integrity Language Technology
International Workshop on
Model-Based Development and Contract-Based Programming
as part of Embedded Systems Week (ESWEEK)
The Assume Guarantee Reasoning Environment (AGREE) is a tool for compositional verification of architectural models described in the Architectural Analysis & Design Language (AADL). The tool has been developed by Rockwell Collins and the University of Minnesota.
AGREE has been used on multiple projects within both organizations; to date there have been 16 publications about different uses of the tool, and several current DARPA projects are using AGREE for reasoning about complex system and system≠of≠systems architectures.
AADL Models are used to describe the architecture of embedded systems. The language includes syntax for describing both the hardware and software components as well as their communication paths. AADL is an SAE Standard (AS≠5506), and the standardization committee has participation from many industrial partners and academic partners.
AGREE takes as input an AADL model with annotations describing a formal contract that each component in the model must obey. A contract consists of a set of assumptions and guarantees. A componentís assumptions are constraints about what inputs that the component expects to receive. A componentís guarantees are constraints about how the component responds to its inputs.
The tool translates an AADL model along with its AGREE contracts into a format that can be analyzed by modern SMT≠Based infinite state model checkers. The results are then presented back to the user in an easy to interpret format.
In this talk we will discuss how the tool is implemented and demonstrate it on a few examples of real systems.