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

Forfattere

  • 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

Resumé

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

Publiceret

1999-12-23

Citation/Eksport

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

Nummer

Nr. 53 (1999): RS-53 Model-Checking Real-Time Control Programs. Verifying LEGO Mindstorms Systems Using UPPAAL

Sektion

Artikler

Licens

Authors who publish with this journal agree to the following terms:

    1. Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.

    1. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.

  1. Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).