Model-checking real-time control programs: verifying Lego(R) MindstormsTM systems using UPPAAL. - Torsten K. Iversen; Kåre J. Kristoffersen; Kim Guldstrand Larsen; Morten Laursen; Rune G. Madsen; Steffen K. Mortensen; Paul Pettersson; Chris B. Thomasen (ECRTS, 2000)