×

Safety verification of model helicopter controller using hybrid input/output automata. (English) Zbl 1032.93535

Maler, Oded (ed.) et al., Hybrid systems: Computation and control. 6th international workshop, HSCC 2003, Prague, Czech Republic, April 3-5, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2623, 343-358 (2003).
Summary: This paper presents an application of the Hybrid I/O Automaton (HIOA) framework in verifying a realistic hybrid system. A supervisory pitch controller for a model helicopter system is desigter 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.
For the entire collection see [Zbl 1017.00053].

MSC:

93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
93A30 Mathematical modelling of systems (MSC2010)
93C95 Application models in control theory

Software:

HyTech
PDFBibTeX XMLCite
Full Text: Link