Information Technology Reference
In-Depth Information
top-level contract
C
II
for our system in Figure 1 guarantees the 40
ms
delay under
assumptions that the rotational speed
s
en
and values for the throttle angle
a
tr
are
within certain ranges:
⎨
⎨
⎩
inputs
s
en
,
a
tr
variables
parameters
−
outputs
⎩
t
in
,
t
ig
C
II
=
types
s
en
,
a
tr
,
t
in
,
t
ig
∈
N
(
≥
s
en
≤
)
∧
(
≥
a
tr
≤
)
assumptions
0
6400
0
100
t
ig
−
t
in
>
40
guarantees
Based on this structure, we can link properties between dependent components
in a similar way it is done when wiring components using connectors (i.e. links be-
tween their input/output variables). Figure 3 shows our example system modelled
using contracts. Every component provides certain guarantees which stay in rela-
tion to assumptions of dependent components. These components in turn provide
guarantees based on their own assumptions, and so forth. In this way, all proper-
ties within a system hierarchy can be linked together. In Figure 3, we have also
highlighted different types of relations between contracts, required to build such a
hierarchy (see Section 2.2). These are:
•
Composition
: two contracts can interact when after connecting their guaran-
tees and assumptions both contracts can function correctly (we discuss this
in more detail in Section 3.3). We use the operator
to define a composi-
tion (Benveniste et al (2012)). An example of such relations is shown in Fig-
ure 3, where contracts
C
FS
,
C
IS
,and
C
IIAS
form a composite contract, i.e.
(
⊗
C
FS
⊗
C
IS
)
⊗
C
IIAS
)
.
•
Refinement/abstraction
: similar to refinement of properties, contracts refine other
contracts in terms of refined assumptions and guarantees. We use the operator
for this relation. The top-level contract
C
II
has such a relation with the contained
System Contract C
II
A
C
AFS
G
A
G
A
C
FS
G
A
C
FS
G
Alternatives
A
C
IIAS
G
A
A
C
IS
G
A
G
Refinement/
Abstraction
Composition
Fig. 3
The Engine Controller system represented using contracts and their basic relations (A
- assumptions, G - guarantees, C - contracts)
Search WWH ::
Custom Search