Model-checking real-time control programs: verifying LEGO MINDSTORMSTM systems using UPPAAL
Torsten K. Iversen, Kåre J. Kristoffersen, Kim G. Larsen, Morten Laursen, Rune G. Madsen, Steffen K. Mortensen, Paul Pettersson, Chris B. Thomasen · 2000
The authors present a method for automatic verification of real time control programs running on LEGO(R) RCXTMbricks 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) RCXTMprocessor 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.