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