Third International Conference On Quality Software
Modeling and Verifying a Lego Car Using Hybrid I/O Automata
Dallas, Texas
November 06-November 07
ISBN: 0-7695-2015-4
We illustrate the application of the hybrid I/O automata framework of Lynch, Segala & Vaandrager by using it to model and analyze the behavior of a simple Lego car with caterpillar treads. We derive constraints on the values of the parameters that occur in our hybrid model that guarantee that the car will always move forward along a black tape, and will never get off the tape or move backward. In order to simplify the correctness proof, we introduce a transition systems that abstracts from the hybrid automaton in a rather drastic manner, but still preserves validity of the correctness properties in which we are interested. Even though our original model does not involve any disturbances, the general parametric analysis of the system allows us to extend our results in a trivial manner to a hybrid model in which several disturbances are allowed (mistakes in measurements of lengths, drift and jitter of the hardware clock, velocity, and distance between the two caterpillar treads).
Citation:
Ansgar Fehnker, Frits Vaandrager, Miaomiao Zhang, "Modeling and Verifying a Lego Car Using Hybrid I/O Automata," qsic, pp.280, Third International Conference On Quality Software, 2003