Model-Checking Real-Time Control Programs. Verifying LEGO Mindstorms 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

doi:10.7146/brics.v6i53.20123

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

Authors

Torsten K. Iversen
Kåre J. Kristoffersen
Kim G. Larsen
Morten Laursen
Rune G. Madsen
Steffen K. Mortensen
Paul Pettersson
Chris B. Thomasen

DOI:

https://doi.org/10.7146/brics.v6i53.20123

Abstract

In this paper, we present a method for automatic verification
of real-time control programs running on LEGO
RCX 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 RCX 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 bricks by color.

Downloads

Published

1999-12-23

How to Cite

Iversen, T. K., Kristoffersen, K. J., Larsen, K. G., Laursen, M., Madsen, R. G., Mortensen, S. K., Pettersson, P., & Thomasen, C. B. (1999). Model-Checking Real-Time Control Programs. Verifying LEGO Mindstorms Systems Using UPPAAL. BRICS Report Series, 6(53). https://doi.org/10.7146/brics.v6i53.20123