Voltar
Artigo Acesso aberto
BIBTEX RIS

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

1999; Volume: 6; Issue: 53 Linguagem: Inglês

10.7146/brics.v6i53.20123

ISSN

1601-5355

Autores

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

Tópico(s)

Embedded Systems Design Techniques

Resumo

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.

Referência(s)