Information Technology Reference
In-Depth Information
The formulation of contracts supports separation of views, but the different views
have to be consistent. A contract
Ctr
is
consistent
, indicated through a predicate
Cons
(
Ctr
)
, if it will never enter a deadlock state if its environment interacts with
it according to its protocol, that is, for all
?
op
1
(
x
1
)
,...,
?
op
k
(
x
k
)
∈Ctr.Prot
,
Init
;
g
1
&
D
1
[
x
1
/in
1
];
...
;
g
k
&
D
k
[
x
k
/in
k
]
,
¬wait ∧∃op ∈ MDec•g
(
op
)
wp
=
true
Note that this formalization takes both synchronization conditions and function-
alities into account, as an execution of a method with its precondition falsified
will diverge and a divergent state can cause deadlock too.
We have proven the following
theorem of separation of concerns
:
Theorem 1 (Separation of Concerns)
1. If
Cons
(
I, Init, MSpec, Prot
i
)
,then
Cons
(
I, Init, MSpec, Prot
1
∪ Prot
2
)
,
i ∈{
1
,
2
}
2. If
Cons
(
I, Init, MSpec, Prot
1
)
and
Prot
2
⊆ Prot
1
,then
Cons
(
I, Init, MSpec, Prot
2
)
3. If
Cons
(
I, Init, MSpec, Prot
)
and
MSpec
MSpec
1
,then
Cons
(
I, Init, MSpec
1
, Prot
)
This allows us to refine the specification and the protocol separately.
We are now current working on an extension to the model of contracts for
specification of the timing information of a component. An interesting and im-
portant point that we would like to make is that the notation for timing aspect
at the contract level should be different from that used for the model of the de-
sign of components. At the contract level, we propose the use of interval based
notation to describe the minimal time and maximal time
[
t
e
,T
e
]
that the envi-
ronment has to wait when calling an interface method (that is the worst case
execution time of the interface methods), and the minimal time and maximal
time
[
t
w
,T
w
]
that the component is willing to wait for a method to be invoked.
Zhou Chaochen's Duration Calculus [32] is an obvious choice for reasoning about
these interval based timing properties. However, for the design and verification
of the implementation of a component, clocks or timers in the timed automata
model are more feasible. This indicates the use of different notations at differ-
ent levels of abstraction in system development. A challenge is to link the clock
time model for the design of components to the interval-based time model of its
contract. Initial results on this work can be found [26].
Contract Refinement.
A contract
Ctr
has a denotational semantics in terms
of its
failure set
F
(
Ctr
)
and divergence set
F
(
Ctr
1
)
, that is same as the failure-
divergence semantics for CSP (but we do not use the CSP language) [6].
Ctr
1
is
refined
by contract
Ctr
2
, denoted by
Ctr
1
Ctr
2
, if the later offers the same
provided methods,
Ctr
1
.MDec
=
Ctr
2
.MDec
, is not more likely to diverge than
the former,
D
(
Ctr
1
)
⊇D
(
Ctr
2
)
, and not more likely to deadlock than the former,
F
(
Ctr
1
)
⊇F
(
Ctr
2
)
. We have established a complete proof techniques of refine-
ment by simulation.
Theorem 2 (Refinement by Simulation)
Ctr
1
Ctr
2
if there exists a total mapping
ρ
(
u, v
):
FDec
1
−→
FDec
2
such that
Search WWH ::
Custom Search