@InProceedings{MWLF-hscc03,
  Title                    = {Safety Verification of Model Helicopter Controller using Hybrid {I}nput/{O}utput Automata},
  Author                   = {Sayan Mitra and Yong Wang and Nancy Lynch and Eric Feron},
  Booktitle                = {6th International Workshop on Hybrid Systems: Computation and Control (HSCC 2003)},
  Year                     = {2003},
  Pages                    = {343-358},

  Abstract                 = {This paper presents an application of the Hybrid Input/Output Automaton (HIOA) framework in verifying a realistic hybrid system. A supervisory pitch controller for a model helicopter system is designed and then verified. The design of the supervisory controller is limited by actuator bandwidth, sensor inaccuracies, and the sampling rates. Verification is carried out by induction over the length of an execution of the composed system. The HIOA model makes the inductive proofs tractable by decomposing them into independent discrete and continuous parts. The paper also presents language constructs for specifying HIOAs.},
  Biburl                   = {http://users.crhc.illinois.edu/mitras/research.html},
  Crossref                 = {HSCC2003},
  Keywords                 = {Hybrid systems, Verification},
  Pdfurl                   = {research/2003/paper033.pdf},
  Ppturl                   = {research/presentations/HSCC03.ppt},
  Url                      = {http://www.springerlink.com/content/9vlmduh36103d221/}
}