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

In this paper, we present a method for automatic verificationof real-time control programs running on LEGO RCX bricks using the verification tool UPPAAL. The controlprograms, consisting of a number of tasks running concurrently,are automatically translated into the timed automatamodel of UPPAAL. The fixed scheduling algorithmused by the LEGO RCX processor is modeled in UPPAAL,and supply of similar (sufficient) timed automatamodels for the environment allows analysis of the overallreal-time system using the tools of UPPAAL. To illustrateour techniques we have constructed, modeled and verifieda machine for sorting LEGO bricks by color