Information Technology Reference
In-Depth Information
3.3
Control Program
The design for the controller program is essentially a specication of a timed au-
tomaton, The program design is given in terms of the so called \implementables"
which are formulas that reflect properties of timed automata. When
;
1
;:::
de-
note states or
phases
of a control program, and
denote combinations
of sensor/actuator states or phase states, the implementable forms are:
'; '
1
;:::
de−!d_
1
__
n
e
Sequencing:
,where
n
= 0 means that the program is
stuck in phase
1 means that there is a choice of a successor phase.
Sequencing constraints specify non-deterministic transitions of an untimed au-
tomaton.
, while
n
>
d^'e
c
−! d : e
Progress:
holds
for
c
time units. A progress constraint species an upper bound on a transition.
Note that
c
is an upper bound, the transition may be taken earlier, if selection
allows it.
Progress also includes
active stability
of a state:
, where the phase
is left at the latest when
'
d ^ 'e
c
−! d e
.
Selection:
(
d:e
;
d ^'e^`
c
)
−! d _
1
_ :::_
n
e
, where the sequencing of
state
for
c
time units (or forever, if the
time-bound is omitted). If
n
= 0 the formula denes conditional, time-bounded
invariance
of the state. Note that
c
is a lower bound, an implementation may
keep the selection open for a longer time, but not for a shorter.
is constrained under the condition
'
d
1
_ ::: _
n
e
c
−! d ' e
Synchronization:
, where the combined state
1
_ ::: _
n
will cause
to hold after
c
time units. Note that
c
is an upper bound, an
implementation is allowed to cause
'
'
sooner but not later.
d:e
d^'e^`
−! d ' e
Framing:
(
;
c
)
, is dual to selection. It is a commitment
that the state
'
will remain stable for
c
time units if it is present when
is
entered.
These forms dene a timed automaton which observes (reads) plant states
or states of other automata through the
conditions in progress and selection
forms, and which changes control and plant states through synchronization and
framing.
'
If controlled states are kept disjoint then conjunction of implementables cor-
responds to parallel composition of automata.
3.4
Controller Design
In ProCoS, renement by phase splitting is pursued. We shall illustrate it by a
cyclic controller.
For a nite collection of exclusive modes
P
1
;:::;
P
n
, a detection phase
and
continuation phases
1
;:::;
n
, a cyclic controller with a
delay is specied by
Search WWH ::
Custom Search