Model-Checking Real-Time Control Programs. Verifying LEGO Mindstorms Systems Using UPPAAL

Abstract

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