Modeling and verifying a Lego car using hybrid I/O automata

Ansgar Fehnker; Frits W. Vaandrager; Miaomiao Zhang

doi:10.1109/QSIC.2003.1319112

Modeling and verifying a Lego car using hybrid I/O automata

Ansgar Fehnker, Frits W. Vaandrager, Miaomiao Zhang

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

8 Citations (Scopus)

Abstract

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 always moves forward along a black tape, and never gets off the tape or move backward. In order to simplify the correctness proof, we introduce a transition system 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).

Original language	English
Title of host publication	Proceedings, Third International Conference on Quality Software, QSIC 2003
Place of Publication	Piscataway, NJ
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	280-289
Number of pages	10
ISBN (Print)	0769520154
DOIs	https://doi.org/10.1109/QSIC.2003.1319112
Publication status	Published - 2003
Externally published	Yes
Event	3rd International Conference on Quality Software, QSIC 2003 - Dallas, United States Duration: 6 Nov 2003 → 7 Nov 2003

Conference

Conference	3rd International Conference on Quality Software, QSIC 2003
Abbreviated title	QSIC 2003
Country/Territory	United States
City	Dallas
Period	6/11/03 → 7/11/03

Access to Document

10.1109/QSIC.2003.1319112

Cite this

@inproceedings{bfb088ed486d4feea3d2c6432befba7e,

title = "Modeling and verifying a Lego car using hybrid I/O automata",

abstract = "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 always moves forward along a black tape, and never gets off the tape or move backward. In order to simplify the correctness proof, we introduce a transition system 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).",

author = "Ansgar Fehnker and Vaandrager, {Frits W.} and Miaomiao Zhang",

year = "2003",

doi = "10.1109/QSIC.2003.1319112",

language = "English",

isbn = "0769520154",

pages = "280--289",

booktitle = "Proceedings, Third International Conference on Quality Software, QSIC 2003",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

address = "United States",

note = "3rd International Conference on Quality Software, QSIC 2003, QSIC 2003 ; Conference date: 06-11-2003 Through 07-11-2003",

}

Fehnker, A, Vaandrager, FW & Zhang, M 2003, Modeling and verifying a Lego car using hybrid I/O automata. in Proceedings, Third International Conference on Quality Software, QSIC 2003. Institute of Electrical and Electronics Engineers (IEEE), Piscataway, NJ, pp. 280-289, 3rd International Conference on Quality Software, QSIC 2003, Dallas, Texas, United States, 6/11/03. https://doi.org/10.1109/QSIC.2003.1319112

Modeling and verifying a Lego car using hybrid I/O automata. / Fehnker, Ansgar; Vaandrager, Frits W.; Zhang, Miaomiao.
Proceedings, Third International Conference on Quality Software, QSIC 2003. Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), 2003. p. 280-289.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Modeling and verifying a Lego car using hybrid I/O automata

AU - Fehnker, Ansgar

AU - Vaandrager, Frits W.

AU - Zhang, Miaomiao

PY - 2003

Y1 - 2003

N2 - 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 always moves forward along a black tape, and never gets off the tape or move backward. In order to simplify the correctness proof, we introduce a transition system 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).

AB - 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 always moves forward along a black tape, and never gets off the tape or move backward. In order to simplify the correctness proof, we introduce a transition system 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).

U2 - 10.1109/QSIC.2003.1319112

DO - 10.1109/QSIC.2003.1319112

M3 - Conference proceeding contribution

SN - 0769520154

SP - 280

EP - 289

BT - Proceedings, Third International Conference on Quality Software, QSIC 2003

PB - Institute of Electrical and Electronics Engineers (IEEE)

CY - Piscataway, NJ

T2 - 3rd International Conference on Quality Software, QSIC 2003

Y2 - 6 November 2003 through 7 November 2003

ER -

Modeling and verifying a Lego car using hybrid I/O automata

Abstract

Conference

Access to Document

Fingerprint

Cite this