Invariance-Preserving Abstractions of Hybrid Systems: Application to User Interface Design

TitleInvariance-Preserving Abstractions of Hybrid Systems: Application to User Interface Design
Publication TypeJournal Article
Year of Publication2008
AuthorsOishi, M., I. M. Mitchell, A. M. Bayen, and C. J. Tomlin
JournalControl Systems Technology, IEEE Transactions on
Pagination229 -244
Date Publishedmar.
Keywordscontinuous state dynamics, continuous systems, discrete event system, discrete event systems, discrete mode logic, discrete state dynamics, formal verification, human computer interaction, human-automation systems, human-hybrid system interaction, hybrid systems, information display, interface analysis, interface verification, invariance-preserving abstraction, mode switching, reachability analysis, safety constraints, safety-critical software, safety-critical system, user interface design, user interfaces

Hybrid systems combine discrete state dynamics which model mode switching, with continuous state dynamics which model physical processes. Hybrid systems can be controlled by affecting both their discrete mode logic and continuous dynamics: in many systems, such as commercial aircraft, these can be controlled both automatically and using manual control. A human interacting with a hybrid system is often presented, through information displays, with a simplified representation of the underlying system. This user interface should not overwhelm the human with unnecessary information, and thus usually contains only a subset of information about the true system model, yet, if properly designed, represents an abstraction of the true system which the human is able to use to safely interact with the system. In safety-critical systems, correct and succinct interfaces are paramount: interfaces must provide adequate information and must not confuse the user. We present an invariance-preserving abstraction which generates a discrete event system that can be used to analyze, verify, or design user-interfaces for hybrid human-automation systems. This abstraction is based on hybrid system reachability analysis, in which, through the use of a recently developed computational tool, we find controlled invariant regions satisfying a priori safety constraints for each mode, and the controller that must be applied on the boundaries of the computed sets to render the sets invariant. By assigning a discrete state to each computed invariant set, we create a discrete event system representation which reflects the safety properties of the hybrid system. This abstraction, along with the formulation of an interface model as a discrete event system, allows the use of discrete techniques for interface analysis, including existing interface verification and design methods. We apply the abstraction method to two examples: a car traveling through a yellow light at an intersection, and a- n aircraft autopilot in a landing/go-around maneuver.


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

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