Computational techniques for the verification of hybrid systems

TitleComputational techniques for the verification of hybrid systems
Publication TypeJournal Article
Year of Publication2003
AuthorsTomlin, C. J., I. Mitchell, A. M. Bayen, and M. Oishi
JournalProceedings of the IEEE
Volume91
Pagination986 - 1001
Date Publishedjul.
ISSN0018-9219
Keywordsaircraft collision avoidance protocols, aircraft control, automata, automata theory, autopilot logic, collision avoidance, computer science verification, continuous dynamical systems, control theory, discrete state systems, formal verification, game theory, hybrid system theory, hybrid systems, reachability, reachability analysis, system theory, two-person zero-sum game, verification
Abstract

Hybrid system theory lies at the intersection of the fields of engineering control theory and computer science verification. It is defined as the modeling, analysis, and control of systems that involve the interaction of both discrete state systems, represented by finite automata, and continuous state dynamics, represented by differential equations. The embedded autopilot of a modern commercial jet is a prime example of a hybrid system: the autopilot modes correspond to the application of different control laws, and the logic of mode switching is determined by the continuous state dynamics of the aircraft, as well as through interaction with the pilot. To understand the behavior of hybrid systems, to simulate, and to control these systems, theoretical advances, analyses, and numerical tools are needed. In this paper, we first present a general model for a hybrid system along with an overview of methods for verifying continuous and hybrid systems. We describe a particular verification technique for hybrid systems, based on two-person zero-sum game theory for automata and continuous dynamical systems. We then outline a numerical implementation of this technique using level set methods, and we demonstrate its use in the design and analysis of aircraft collision avoidance protocols and in verification of autopilot logic.

URLhttp://dx.doi.org/10.1109/JPROC.2003.814621
DOI10.1109/JPROC.2003.814621

a place of mind, The University of British Columbia

Electrical and Computer Engineering
2332 Main Mall
Vancouver, BC Canada V6T 1Z4
Tel +1.604.822.2872
Fax +1.604.822.5949
Email:

Emergency Procedures | Accessibility | Contact UBC | © Copyright 2021 The University of British Columbia