Creating Contracts based Specifications for Components
Components are used both as specification of requirements as well as for modeling the architecture.
Whenever we use components, we can specify their black-box behavior with the help of contracts.
In AF3 we distinguish among four kinds of contracts:
- Assumptions represent invariants over the input ports of a component. Simply said, assumptions are what a certain component
expects as valid input from the environment (e.g. a certain input port has values within a certain range;
some input port has a value that is always bigger than the value of another port).
- Guarantees represent invariants over the output ports of a component. Guarantees are conditions that a certain component
promises to its environment.
- Basic Contracts represent logical expressions of the form "if inputs satisfy assumption A then component outputs will satisfy the guarantee G
(after a certain number of steps)"
- Advanced Contracts represent complex conditions about the relation between the inputs of a component and the outputs
(e.g. after output X had value 5, whenever input A is bigger than 3, then output Y will be bigger than 0)
A temporal logics specification is made of one or more contracts (assumptions, guarantees, basic/advanced contracts).
The main place where the assumptions, guarantees and basic contracts are defined during the specification phase is the "Contracts Specification" view.
The advanced contracts can be defined and saved in the
Semantic Inspector view (just choose the proper pattern, fill in the fields
with the conditions and click on the Save button). The term will be added to the temporal logics specification, if
it already exists, if none exists yet a new one will be created.
The Assumptions/Guarantees and Contracts View
The A/G, Contracts View provides the possibility to access, change or check the saved assumptions, guarantees or contracts on a component.
As we can see in the lower part of the figure, this view has five tabs: the first tab contains the assumptions, the second the guarantees,
the third the basic contracts, the fourth the advanced contracts and finally the fifth contains all specifications.
By clicking on the corresponding entry from the table, one can change different properties of a specification atom: the specification itself or
the verification context in which this specification will be checked. All assumptions attached to the component selected as verification context
are taken into account when the verification is performed.