Semantics and Verification of a Language for Modelling Hardware Architectures - Formal Methods and Hybrid Real-Time Systems - page 313

Consider a module M =( i, o, Conf , conf 0 ,p, out, next ). We shall construct an
Uppaal model for M such that a transition

σ i ,σ o
−→ M conf 2 conf 1

of M is simulated by a sequence of transitions:

c 1 input ? c 1 progress ? c 2 progress ?

progress ?
−→ c n sync ? −→ −→ −→ ··· −→ c 2 ,

in the timed-automata model, where the Uppaal states c 1 and c 2 correspond
to conf 1 and conf 2 , respectively, and the broadcast channels input ? , progress ?
and sync ? have the following roles:

- All component modules synchronize on input ? to initiate the start of a clock
cycle simultaneously.
- Each component module, which has not yet definitions for all its assigned
variables, synchronizes on progress ?. Each such synchronization initiates
an attempt to compute values for undefined variables. Hence, p ( conf 1 ) σ i is
computed in the n steps from c 1 to c n .
- All component modules synchronize on sync ? to complete a clock cycle si-
multaneously.

We shall sketch the timed-automata construction for basic modules and com-
position of modules below. These timed automata run in parallel with a top-level
timed automaton Top shown in Fig. 6, which controls the synchronization in the
system.

input!
reset()

!done()
progress!

done()
sync!
update()

Fig. 6. The Timed Automaton Top

The three procedures reset , done and update have the following

explanations:

- The function reset has type void and it sets a status field for every assigned
variable in the system to undefined.
- The Boolean function done is true when all component modules have defin-
itions for their assigned variables.
- The function update has type void and updates the register values as defined
by the function update in the definition of next in Sect. 4.4.