In this paper, we present a method for automatic verification
of real-time control programs running on
LEGO
R
RCX
T
M bricks using the verification tool U
PPAAL. The control programs, consisting of a number of tasks running
concurrently, are automatically translated into the timed automata model of
U
PPAAL. The fixed scheduling algorithm used by the
LEGO
R
RCX
T
M processor is modeled in U
PPAAL,
and supply of similar (sufficient) timed automata models for the environment
allows analysis of the overall real-time system using the tools of U
PPAAL. To illustrate our techniques we have constructed, modeled and
verified a machine for sorting LEGO
R
bricks by color