DocumentCode
2186031
Title
Model-checking real-time control programs: verifying LEGO MINDSTORMSTM systems using UPPAAL
Author
Iversen, Torsten K. ; Kristoffersen, Kåre J. ; Larsen, Kim G. ; Laursen, Morten ; Madsen, Rune G. ; Mortensen, Steffen K. ; Pettersson, Paul ; Thomasen, Chris B.
Author_Institution
Dept. of Comput. Sci., Aalborg Univ., Aalborg, Denmark
fYear
2000
fDate
21-21 June 2000
Firstpage
147
Lastpage
155
Abstract
The authors present a method for automatic verification of real time control programs running on LEGO(R) RCXTM 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(R) RCXTM 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(R) bricks by color.
Keywords
automata theory; control engineering computing; multiprogramming; program verification; real-time systems; scheduling; LEGO MINDSTORMS systems verification; LEGO RCX bricks; UPPAAL; automatic verification; concurrent tasks; control programs; fixed scheduling algorithm; model checking; real time control programs; real time system; timed automata model; verification tool; Actuators; Algorithm design and analysis; Automata; Automatic control; Computer science; Control systems; Electronic mail; Real time systems; Scheduling algorithm; Sorting;
fLanguage
English
Publisher
ieee
Conference_Titel
Real-Time Systems, 2000. Euromicro RTS 2000. 12th Euromicro Conference on
Conference_Location
Stockholm
ISSN
1068-3070
Print_ISBN
0-7695-0734-4
Type
conf
DOI
10.1109/EMRTS.2000.854002
Filename
854002
Link To Document