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