tl_specification.html 3.39 KB
Newer Older
Daniel Ratiu's avatar
Daniel Ratiu committed
1
2
3
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">

<!--
4
Contracts-based Specification for Components.
Daniel Ratiu's avatar
Daniel Ratiu committed
5
6
7
8
 
 @author becker
 @author $Author: becker $
 @version $Rev: 3250 $
9
 @ConQAT.Rating GREEN Hash: F45C3DE9A654E93163AC0C9149FA9CB6
Daniel Ratiu's avatar
Daniel Ratiu committed
10
11
12
13
14
-->
 
<html>
<head>
	<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
15
	<title>Contracts-based Specification for Components</title>
Daniel Ratiu's avatar
Daniel Ratiu committed
16
17
18
</head>
<body>

Daniel Ratiu's avatar
Daniel Ratiu committed
19
<h2><u><font color="#336699">Creating Contracts based Specifications for Components</font></u></h2>
Daniel Ratiu's avatar
Daniel Ratiu committed
20

Daniel Ratiu's avatar
Daniel Ratiu committed
21
Components are used both as specification of requirements as well as for modeling the architecture. 
22
23
24
25
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: 
<ul>
<li><b>Assumptions</b> represent invariants over the input ports of a component. Simply said, assumptions are what a certain component
Daniel Ratiu's avatar
Daniel Ratiu committed
26
expects as valid input from the environment (e.g. a certain input port has values within a certain range; 
27
28
some input port has a value that is always bigger than the value of another port).</li>
<li><b>Guarantees</b> represent invariants over the output ports of a component. Guarantees are conditions that a certain component
Daniel Ratiu's avatar
Daniel Ratiu committed
29
promises to its environment. </li>
30
31
32
33
34
35
36
<li><b>Basic Contracts</b> 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)"</li>
<li><b>Advanced Contracts</b> 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)</li>
</ul>
            
A temporal logics specification is made of one or more contracts (assumptions, guarantees, basic/advanced contracts). 
Daniel Ratiu's avatar
Daniel Ratiu committed
37
The main place where the assumptions, guarantees and basic contracts are defined during the specification phase is the "Contracts Specification" view.
38
39
40
41
42
43

<br><br>
<img src="./pictures//Model.Checking.Contracts.Specification.View.png">
<br><br>

The advanced contracts can be defined and saved in the   
Daniel Ratiu's avatar
Daniel Ratiu committed
44
<a href="model_checking_with_af3.html">Semantic Inspector </a> view (just choose the proper pattern, fill in the fields 
45
with the conditions and click on the <b>Save</b> button). The term will be added to the temporal logics specification, if 
Daniel Ratiu's avatar
Daniel Ratiu committed
46
47
48
49
50
51
52
it already exists, if none exists yet a new one will be created. 

<br><br>
<img src="./pictures/tl_specification_creation.png">
<br><br>


53
54
55
56
57
<h2><u><font color="#336699">The Assumptions/Guarantees and Contracts View</font></u></h2>

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.
Daniel Ratiu's avatar
Daniel Ratiu committed
58

59
By clicking on the corresponding entry from the table, one can change different properties of a specification atom: the specification itself or
60
61
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.
Daniel Ratiu's avatar
Daniel Ratiu committed
62
63

<br><br>
64
<img src="./pictures/Model.Checking.Contracts.Specification.png">
Daniel Ratiu's avatar
Daniel Ratiu committed
65
66
67
68
69
<br><br>

</font>
</body>
</html>