Safety verification of model helicopter controller using hybrid input/output automata

Sayan Mitra, Yong Wang, Nancy Lynch, Eric Feron

Research output: Contribution to journalArticle


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.

Original languageEnglish (US)
Pages (from-to)343-358
Number of pages16
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
StatePublished - Dec 1 2003
Externally publishedYes

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Safety verification of model helicopter controller using hybrid input/output automata'. Together they form a unique fingerprint.

  • Cite this