## Tool Suite Overview

Figure 1 shows an overview of the AGREE/OSATE tool suite. As presented in the figure, OSATE is installed as an Eclipse plugin that serves as the IDE for creating AADL models. AGREE runs as a plugin inside OSATE that provides both a language (AADL annex to annotate the models with assume-guarantee behavioral contracts) and a tool (for compositional verification of the contracts reside in AADL models). AGREE translates an AADL model and its contract annotations into Lustre and then queries the JKind model checker to perform the verification. JKind invokes a backend Satisfiability Modulo Theories (SMT) solver (e.g., Yices or Z3) to validate if the guarantees are valid in the compositional setting.

Figure 1: Overview of AGREE/OSATE Tool Suite