@inbook{1286f8230b0e463ba79f1c9330e2e9fb,
title = "Safety verification of model helicopter controller using hybrid input/output automata",
abstract = "This paper presents an application of the Hybrid I/O Automaton (HIOA) framework [12] in verifying a realistic hybrid system. A supervisory pitch controller for a model helicopter system is designed and then verified. The design of the supervisor is limited by the actuator bandwidth, the sensor inaccuracies, and the sampling rates. Verification is carried out by induction over the length of an execution of the composed system automaton. The HIOA model makes the inductive proofs tractable by decomposing them into independent discrete and continuous parts. The paper also presents a set of language constructs for specifying hybrid I/O automata.",
author = "Sayan Mitra and Yong Wang and Nancy Lynch and Eric Feron",
year = "2003",
doi = "10.1007/3-540-36580-x_26",
language = "English (US)",
isbn = "3540009132",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "343--358",
editor = "Oded Maler and Amir Pnueli",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
address = "Germany",
}