Information Technology Reference
In-Depth Information
6.2
Construction for Basic Modules — a Sketch
Consider a basic module
B
as described in Sect. 4. We shall assume that there
is a declaration of a global Uppaal variable for every variable in the signature
for the datapath including the primed register variables. Furthermore, for every
primed register, output port and signal (i.e. the assignable variables) there is a
status field describing whether or not the variable is defined.
For every expression
e
occurring as a guard in a transition of the controller
there is corresponding local Boolean Uppaal function
G
e
implementing
[[
e
]] , a n d
for every set of actions
as
occurring in a transition of the controller, there is a
local Uppaal function
P
as
of type
void
, which corresponds to the function
as
,
i.e. it can compute values for assigned variables whenever this is possible.
Every state
s
of the controller corresponds to a location (also called
s
)ofthe
timed automaton, and for every transition (
s
1
,e,as,s
2
) of the controller, a fresh
timed-automaton location
s
is introduced as shown in Fig. 7.
E
G_e()
input?
P_as()
sync?
s'
s1
s2
progress?
P_as()
Fig. 7.
Timed-automaton representation of the transition (
s
1
,e,as,s
2
)
6.3
Construction for Composition of Modules — A Sketch
Consider a composition
M
of
k
modules
m
1
,...,m
k
using a single assignment
program
p
as described in Sect. 5. Assume that
T
1
,...,T
k
are timed-automata
representations of
m
1
,...,m
k
, respectively. The timed automaton for
M
is given
by the parallel composition:
T
1
···
T
k
T
p
,
input?
P()
progress?
P()
sync?
Fig. 8.
Timed-automaton representation of the single assignment program
p
Search WWH ::
Custom Search