TY - JOUR AU - Iversen, Torsten K. AU - Kristoffersen, Kåre J. AU - Larsen, Kim G. AU - Laursen, Morten AU - Madsen, Rune G. AU - Mortensen, Steffen K. AU - Pettersson, Paul AU - Thomasen, Chris B. PY - 1999/12/23 Y2 - 2024/03/28 TI - Model-Checking Real-Time Control Programs. Verifying LEGO Mindstorms Systems Using UPPAAL JF - BRICS Report Series JA - BRICS VL - 6 IS - 53 SE - Articles DO - 10.7146/brics.v6i53.20123 UR - https://tidsskrift.dk/brics/article/view/20123 SP - AB - 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. ER -