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

Sayan Mitra, Yong Wang, Nancy Lynch, Eric Feron

Research output: Chapter in Book/Report/Conference proceedingChapter

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.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsOded Maler, Amir Pnueli
PublisherSpringer
Pages343-358
Number of pages16
ISBN (Print)3540009132, 9783540009139
DOIs
StatePublished - 2003
Externally publishedYes

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2623
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

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