## Main Features{#sec:agree_osate_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 @fig:import_project_from_file_menu. This will open an
Import dialog box, as shown in @fig:import_project_dialog. 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.

![Import Project from the File Menu](../../media/image23.png){#fig:import_project_from_file_menu width="1.9375in" height="2.9254615048118984in"}

**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 @fig:import_project_dialog 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 @fig:import_archived_projects.

![Import Dialog Box](../../media/image24.png){#fig:import_project_dialog width="3.3333333333333335in"
height="3.485133420822397in"}

![Import Archived Projects](../../media/image25.png){#fig:import_archived_projects width="3.125in" height="4.096283902012249in"}

**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 @fig:import_project_dialog and click "Next".
Choose "Select root directory", navigate to the location and select the
project folder, and click "Finish". An example is shown in @fig:import_projects_from_directory.

![Import Projects from a Directory](../../media/image26.png){#fig:import_projects_from_directory width="4.020833333333333in" height="5.199353674540682in"}

**Import Git Projects.** To import a project from Git, choose "Projects
from Git" under the "Git" category from the Import Dialog box in @fig:import_project_dialog
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](https://github.com/smaccm/smaccm/tree/master/models).
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](https://git-scm.com/).

### 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](04.02-Installation.html#fig: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 @fig:create_new_aadl_project_dialog. More detailed information
about creating AADL models in a project can be found at
[Editing a First AADL Model](https://wiki.sei.cmu.edu/aadl/index.php/Editing_a_first_AADL_model).

![Create a New AADL Project](../../media/image27.png){#fig:create_new_aadl_project_dialog width="4.78125in" height="4.430501968503937in"}

### 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](02.00-Brief-Overview-of-AADL-and-AGREE.html#fig:verify_all_layers_from_right_click))
or the AGREE menu
(shown in
[Verify All Layers from AGREE Menu](02.00-Brief-Overview-of-AADL-and-AGREE.html#fig: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 @fig:a_hierarchical_model. 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.

![A Hierarchical Model](../../media/image28.png){#fig:a_hierarchical_model .class width=80%}

**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](#sec: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](04.02-Installation.html#fig: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](02.00-Brief-Overview-of-AADL-and-AGREE.html#fig:verify_all_layers_from_right_click))
or the AGREE menu
(shown in
[Verify All Layers from AGREE Menu](02.00-Brief-Overview-of-AADL-and-AGREE.html#fig:verify_all_layers_from_agree_menu)).

### AGREE/AADL to Simulink Exporter{#sec:agree_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](03.06-Statements.html#sec:real_time_patterns))
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](02.00-Brief-Overview-of-AADL-and-AGREE.html#fig:verify_all_layers_from_right_click))
or the AGREE menu
(shown in
[Verify All Layers from AGREE Menu](02.00-Brief-Overview-of-AADL-and-AGREE.html#fig:verify_all_layers_from_agree_menu)).

3\. The dialog box shown in @fig:general_simulink_models_dialog 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.

![General Simulink Models Dialog](../../media/image29.png){#fig:general_simulink_models_dialog .class width=90%}

***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.

