NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Discrete Abstractions of Hybrid Systems: Verification of Safety and Application to User-Interface DesignHuman interaction with a complex control system involves the user, the automation’s discrete
mode logic, and the underlying continuous dynamics of the physical system. The user-interface
of such systems always displays a reduced set of information about the entire system. Designing
interfaces such that all the pertinent information is available and assuring that this information
is correct is important for any user-interface, but especially so for safety-critical systems such as
automotive systems and autopilots. Here we describe a methodology for the analysis of hybrid
control systems that incorporate user interaction, with the goal of assuring that the information
provided to the user is correct. That is, the user-interface must contain all information necessary
to safely complete a desired procedure or task.

We begin with a hybrid system model which incorporates discrete mode logic as well as
nonlinear continuous dynamics. Using a hybrid computational tool for reachability, we find the
largest region of the state-space in which we can guarantee the state of the system can always
remain – this is the safe region of operation. By implementing a controller for safety which
arises from this computation, we mathematically guarantee that this safe region is invariant,
meaning that the system will always remain within the safe region if the determined controller
is used on the boundary of the safe region. Verification within a hybrid framework allows us
to account for the continuous dynamics underlying the discrete representations displayed to
the user. Using the computed invariant regions as discrete states, we can abstract a discrete
event system from this hybrid system with safety restrictions. This abstraction can be used to
determine what information must be provided on the display. Furthermore, in cases in which
an interface already exists, the abstraction provides the necessary input into existing interface
verification methods.

We provide two examples: a car traveling through a yellow light at an intersection and an
aircraft autopilot in an automatic landing/go-around maneuver. The examples demonstrate
the applicability of this methodology to hybrid systems that have operational constraints we
can pose in terms of safety. This methodology differs from existing work in hybrid system
verification in that we directly account for the user’s interactions with the system.
Document ID
20040000797
Acquisition Source
Ames Research Center
Document Type
Technical Memorandum (TM)
Authors
Meeko Oishi
(Stanford University Stanford, California, United States)
Claire Tomlin
(Stanford University Stanford, California, United States)
Asaf Degani
(Ames Research Center Mountain View, California, United States)
Date Acquired
August 21, 2013
Publication Date
November 1, 2003
Subject Category
Aircraft Communications And Navigation
Funding Number(s)
PROJECT: RTOP 548-40-12
CONTRACT_GRANT: NCC2-798
CONTRACT_GRANT: N00014-00-1-06637
CONTRACT_GRANT: N66001-01-C-8080
Distribution Limits
Public
Copyright
Public Use Permitted.
Document Inquiry

Available Downloads

There are no available downloads for this record.
No Preview Available