## Main Features

In this section we walk through the main features involved with the AGREE tool suite.

### Import Existing Projects

To import an existing project into AGREE, users need to first select "Import" through the File menu as shown in Figure 1. This will open an Import dialog box, as shown in Figure 2. From there, users can choose to import from different sources. This section presents a few most commonly used sources. After the import project selection is done, you should see the project in the AADL Navigator in the left-hand-side pane in OSATE.

Figure 1: Import Project from the File Menu

Import Archived Projects. To import an archived project (previously exported project in the form of a zip or tar file format), choose "Existing Projects into Workspace" under the "General" category from the Import Dialog box in Figure 2 and click "Next". Choose "Select archive file", navigate to the location and select the archived project file, and click "Finish". An example is shown in Figure 3.

Figure 2: Import Dialog Box
Figure 3: Import Archived Projects

Import Projects from a Directory. To import a project from a directory, choose "Existing Projects into Workspace" under the "General" category from the Import Dialog box in Figure 2 and click "Next". Choose "Select root directory", navigate to the location and select the project folder, and click "Finish". An example is shown in Figure 4.

Figure 4: Import Projects from a Directory

Import Git Projects. To import a project from Git, choose "Projects from Git" under the "Git" category from the Import Dialog box in Figure 2 and click "Next". Choose the "Existing local repository", then select a local repository that contains the projects, and explore to the specific project folder to import.

Note: Example projects with AGREE contracts in the AADL models can be obtained from the SMACCM Git repository. These files are from GitHub and could be retrieved via the Git configuration control tool. More information about the Git tool and the download information can be found at Git-SCM.

### Create New Projects

After started OSATE, the AADL perspective should be the default. If not, the AADL perspective can be selected via selecting the "Window" menu -> "Perspective" -> "Open Perspective" -> "Other…" -> "AADL". (See the "AADL" text on the upper right corner of the OSATE window as shown in Agree Install Test.)

Create a new AADL project by selecting the "File" menu -> "New" -> "Project…", and select "AADL Project" under the "AADL" category. An example is shown in Figure 5. More detailed information about creating AADL models in a project can be found at Editing a First AADL Model.

Figure 5: Create a New AADL Project

### Verify Contracts

As described in the previous chapters, each of the system and component contracts in AGREE are formalized as Assumptions and Guarantees. A component’s contracts contain a set of Assumptions about the component's inputs and a set of Guarantees about the component's outputs. The Assumptions and Guarantees may also contain predicates that reason about how the state of a component evolves over time.

The goal of compositional verification is to prove that each component's contract is satisfied by the interaction of its direct subcomponents as described by their respective contracts. Users can start the verification by selecting a system implementation of a component in the outline pane on the right side of OSATE, and select either the "Verify Single Layer" or the "Verify All Layers" option from the right-click menu (shown in Verify All Layers from Right Click) or the AGREE menu (shown in Verify All Layers from AGREE Menu). As the names suggest, "Verify Single Layer" performs verification at the current layer of the architecture hierarchy, while "Verify All Layers" performs verification at the current layer and each layer below. For a given layer of the architecture, the verification uses the Assumptions and Guarantees of the direct lower level components as supporting evidence, to prove if the Assumptions and Guarantees at the current layer are satisfied.

Another verification option that is available through the right-click menu or AGREE menu when selecting a system implementation is "Verify Monolithically". This option utilizes Assumptions and Guarantees not only from the direct subcomponents at the lower level, but from components all levels below as evidence for the verification. This is needed when the constraints imposed by components lower in the hierarchy are needed in the proof, so users do not need to manually copy the Assumptions and Guarantees from those lower level components up to their parent components in the hierarchy.

To help clarify the difference between the co-verification options, consider the picture in Figure 6. In this Figure, the blocks represent AADL system implementations for different components. In compositional verification ("Verify Single Layer" and "Verify All Layers"), AGREE will only use the Assumptions and Guarantees of component 2 and 3 as evidence (`A``2`, `G``2`, `A``3`, and `G``4`) to prove the Assumptions and Guarantees of component 1 (`A``1` and `G``1`); the tool ignore any of the constraints posed by components 4 through 7. Monolithical verification, on the other hand, will use Assumptions and Guarantees of components 2 through 7 to prove the Assumptions and Guarantees of component 1.

The philosophy of the compositional verification option is that component contracts should yield the minimum constraints necessary in order to prove the guarantees of the direct parents. This aids the model checker by explicitly hiding information that may be unnecessary to prove top level claims. Compositional verification should be used as the default verification option with AGREE.

Figure 6: A Hierarchical Model

Note 1: Details of lower level components (e.g., implementation details besides the assumptions and guarantees on the interface of the components) are abstracted away during verification of higher level component contracts.

Note 2: Component contracts at the lowest level of the architecture are assumed to be true by AGREE. Verification of these component contracts must be performed outside of the AADL/AGREE environment, as demonstrated in AGREE to Simulink Exporter.

When the verification starts, a results view appears at the bottom of the screen with the status of all the contracts being checked. Results for each component are grouped by guarantees, assumptions, and consistency. The consistency check verifies if the composition of the subcomponents are consistent, and if the contracts being analyzed for a component is consistent. For example, it checks if the conjunction of a system’s guarantees is satisfiable.

If a counterexample for a contract is found then it will have a red icon next to it in the results dialog. Right-clicking on one of these results will bring up a menu where you can choose to view the counterexample in the console, in a spreadsheet, or in a collapsible menu.

Note: Some Guarantees may take longer than the set analysis time to produce a "Valid" or "Invalid" result. In such a case, users may extend the timeout time (e.g., from 100 seconds to 1000 seconds) and/or enlarge the maximum depth for k-induction to use, in OSATE "Window" menu -> "Preferences" -> "Agree" -> "Analysis", as shown in SMT Solver Selection.

### Check Realizability

The need for the realizability checking can be motivated through the following example. In the Microwave AADL model, the following two requirements were imposed:

Requirement 1: While the microwave is in cooking mode, seconds_to_cook shall decrease.

Requirement 2: If the display is quiescent (no buttons pressed) and the keypad is enabled, the seconds_to_cook shall not change.

On input conditions that satisfy both requirements (i.e., when the microwave is in cooking mode, the display is quiescent and the keypad is enabled), there is a conflict in the value of the seconds_to_cook variable, resulting in the two requirements not being able to be satisfied at the same time in those input conditions.

Realizability checking determines whether or not the component works in all input environments that satisfy the component assumptions. It can be invoked by selecting the system implementation of a component in the outline pane on the right side of OSATE, and select either the "Check Realizability" from the right-click menu (shown in Verify All Layers from Right Click) or the AGREE menu (shown in Verify All Layers from AGREE Menu).

### AGREE/AADL to Simulink Exporter

Component contracts at the lowest level of the architecture are assumed to be true by AGREE. Verification of these component contracts must be performed outside of the AADL/AGREE environment. The Exporter feature automatically exports the AGREE contracts into properties in a MATLAB function. The MATLAB function can be connected to the component’s Simulink model and serves as a synchronous observer for its behavior. Simulink Design Verifier can be invoked to check if the component’s Simulink model satisfies the properties exported.

The Exporter feature works with two Simulink models: the implementation model, which contains the subsystem that encapsulates the behavior of the component, and a verification model, which connects the exported AGREE contracts to the implementation.

The implementation model can be auto-generated from the AADL model, if desired, or can be manually created. When auto-generated it contains the inputs and outputs specified in the AADL model and an empty subsystem, ready for the modeler to insert the behavioral logic into. The auto-generated model should be hand edited to contain the implementation of the behavioral aspects of the component, and can be used to generate the code for the target.

The verification model uses the implementation model (as a Simulink model reference block) to create a model suitable for verification. It creates an observer block to wrap the MATLAB function that contains the AGREE contracts as MATLAB properties. It also creates input and output ports according to the AADL model, instantiates a reference to the implementation model, and connects the observer block to the implementation model. The verification model is not suitable for code generation for the target, but is suitable for verification of the implementation. Since the model being verified is a model reference (and not a copy), formal credit may be taken from the verification activity.

The Exporter does not directly generate Simulink models, but rather generates MATLAB scripts which will generate the models. This allows the exporter to remain largely isolated from issues associated with Simulink versions, as well as providing visibility to the model generation actions should it be necessary for debugging purposes.

The Exporter automatically updates the AADL model with the appropriate path and file name information via the “Source_Text” AADL property. This associates the information of the component implementation in the design model, and allows users to proceed directly to action selection in subsequent exports, if no changes to the saved information.

Note that Real-time patterns (as seen in Real Time Patterna) in AGREE cannot be exported to MATLAB functions, and should not be. These patterns refer to the scheduling and performance of the component, rather than its specific behavior. Thus, the model will need to be decomposed further (i.e., so the real-time constraints will be turned into behavioral constraints on each individual component’s inputs and outputs) before generating a Simulink implementation.

To use the Exporter feature, follow the steps below:

1. Specify the data type to be mapped from AGREE to Simulink through the "Window" menu -> "Preferences" -> "Agree" -> "Code Generation". Users may select one of the MATLAB supported integer types (i.e., (u)int8, (u)int16, (u)int32, (u)int64) to represent integers in AGREE and one of the MATLAB supported floating point types (i.e., single, double) to represent reals in AGREE. Note that this option only applies to the abstract “integer” and “real” AADL types; concrete types with a size specification are automatically mapped to the corresponding MATLAB type;

2. Select the system implementation of the component whose contracts are to be exported, and select the "Generate Simulink Models" option in either the right-click menu (shown in Verify All Layers from Right Click) or the AGREE menu (shown in Verify All Layers from AGREE Menu).

3. The dialog box shown in Figure 7 will be presented. After completing the data fields, select the activity to be performed by clicking on one of the action buttons. The fields and actions are described in detail below.

Figure 7: General Simulink Models Dialog

Output Directory Path: This is the location of the exported MATLAB scripts that, when executed, will actually generate the Simulink models (either the implementation or verification model).

Implementation Model Path: This is the location of the implementation model in Simulink. If the model does not exist, the script can generate an empty subsystem with the interface consistent with the AADL model. Note that the implementation model must exist before the verification model can be generated. If the inputs/outputs to the implementation model contain aggregate types or structured data, these IO data will be represented in Simulink by bus objects. These bus objects are auto saved in a file with a filename of the form “<ImplementationModel>_busobjs.m” in this directory.

Verification Model Name: This is the file name for the verification model that will be generated. It will be placed in the output directory specified above.

Subsystem to Verify: This is the name of the subsystem in the verification model that the observer block connects to. The subsystem contains the implementation logic for the chosen component. An auto generated implementation model will contain only the subsystem named after the text entered in this field. A manually created implementation model may contain multiple subsystems, and the subsystem name entered in the field selects the specific subsystem to verify.

Export Contracts – This button will generate the MATLAB script containing the AGREE contracts, translated into MATLAB properties. This script will be wrapped inside an observer block in the generated Verification model. The script will be placed in the Output Directory.

Generate Implementation – This button will generate the script to create an implementation model. When the script is running in MATLAB, an error will be reported if the implementation model already exists. The script will be placed in the Output Directory.

The implementation model is considered non-overwritable (and will not be overwritten with an export). If users wish to regenerate the implementation model, they will first need to delete the existing model (and its bus object storage file, if applicable).

Generate Verification -- This button will generate the script containing the AGREE contracts (as in Export Contracts) as well as the script to create a verification model. The generated scripts will be placed in the Output Directory.

The verification model is considered overwriteable and can be regenerated at-will. This is because the verification model contains no logic that is not already captured in other locations (the AGREE contracts or the implementation model contents). If the AGREE contracts (but not the inputs/outputs) are changed, users can click this button to regenerate the verification model with the new contracts.

Verify Subsystem – This button will generate the script containing the AGREE contracts (as in Export Contracts), as well as the script to create a verification model (as in Generate Verification) and run Simulink Design Verifier on the generated verification model. Note that Design Verifier can still be run from the Simulink environment as needed – the generated script automates all the steps needed to verify an implementation model against its AGREE contracts, completing the verification workflow.