loading...
Modeling and Verifying a Lego Car Using Hybrid I/O Automata
Dallas, Texas November 06-November 07
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QSIC.2003.1319112Third International Conference On Qua ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Ansgar Fehnker, Carnegie Mellon University, Pittsburgh, PA
Frits Vaandrager, University of Nijmegen, The Netherlands
Miaomiao Zhang, University of Nijmegen, The Netherlands
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
Usage of this product signifies your acceptance of the Terms of Use.