Information Technology Reference
In-Depth Information
1. Sequencing: The selection phase
is followed by the continuation phases.
de−!d_
W
j
=1
j
e
2. Sequencing: The continuation phases return to the selection phase.
V
j
=1
d
j
e−!d
j
_e
3. Progress: When
P
i
holds for
in the selection phase, it is left.
V
i
=1
d ^
P
i
e
−! d : e
j
,with
j
4. Progress: When
P
i
holds for
in
=
i
,itisleft.
V
i;j
=1
(
i
=
j
)
)
(
d
j
^
P
i
e
−! d :
j
e
)
5. Selection: The phase
i
is selected under
P
i
.
V
i
=1
(
d:e
;
d ^
P
i
e^`
)
−! d _
i
e
i
6. Selection: The phase
will be
-stable under
P
i
.
V
i
=1
(
d:
i
e
;
d
i
^
P
i
e^`
)
−! d
i
e
7. Progress: The phase
i
is maintained by
P
i
.
V
i
=1
d
i
^
P
i
e
−! d
i
e
A cyclic controller implements the progress constraint
_
W
j
=1
j
)
3
d
(
^
P
i
e
−! d
i
e
for an arbitrary index
i
. Within three delay periods control will be in the phase
corresponding to a stable external state. The worst case occurs when the selec-
tion phase is left after almost a
-period for another continuation phase (1,3).
Within
, control returns to the selection phase (2,4). The nal
-period ensures
transition to the correct phase (1,5,3), where it remains (6,7).
This controller can be extended with suitable actuators enabled in the con-
tinuation phases such that the
Transitive
law ensures a correct implementation
of progress commitments.
In the ProCoS case studies, designs were made more complex by a distributed
framework with CSP-like channels. It required a major eort by Schenke [13] to
develop systematic transformation rules from the level of implementables to this
framework.
Search WWH ::
Custom Search