Invariance-Preserving Abstractions of Hybrid Systems: Applicationto User Interface Design∗Meeko Oishi1, Ian Mitchell2, Alexandre Bayen3, Claire Tomlin41American Institute of Biological Sciences, Washington, DC, [email protected]. of Computer Science, University of British Columbia, Vancouver, BC, [email protected] Engineering, University of California, Berkeley, CA, [email protected]. of Aeronautics and Astronautics, Stanford University, Stanford, CA, [email protected] 8, 2005AbstractHybrid systems combine discrete state dynamics which model mode switching, with con-tinuous state dynamics which model physical processes. Hybrid systems can be controlled byaffecting both their discrete mode logic and continuous dynamics: in many systems, such ascommercial aircraft, these can be controlled both automatically and using manual control. Ahuman interacting with a hybrid system is often presented, through information displays, witha simplified representation of the underlying system. This user interface should not overwhelmthe human with unnecessary information, and thus usually contains only a subset of informationabout the true system model, yet, if properly designed, represents an abstraction of the truesystem which the human is able to use to safely interact with the system. In safety-criticalsystems, correct and succinct interfaces are paramount: interfaces must provide adequate infor-mation and must not confuse the user. We present an invariance-preserving abstraction whichgenerates a discrete event system that can be used to analyze, verify, or design user-interfaces∗Research supported by a National Science Foundation Graduate Research Fellowship, by DARPA under theSoftware Enabled Control Program (AFRL contract F33615-99-C-3014), by the DoD Multidisciplinary UniversityResearch Initiative (MURI) program administered by the Office of Naval Research under Grant N00014-00-1-0637,and by Grant NCC2-798 from NASA Ames Research Center to the San Jose State University Foundation, as part ofNASA’s base research and technology effort, human-automation theory sub-element (RTOP 548-40-12).1for hybrid human-automation systems. This abstraction is based on hybrid system reachabilityanalysis, in which, through the use of a recently developed computational tool, we find con-trolled invariant regions satisfying a priori safety constraints for each mode, and the controllerthat must be applied on the boundaries of the computed sets to render the sets invariant. Byassigning a discrete state to each computed invariant set, we create a discrete event systemrepresentation which reflects the safety properties of the hybrid system. This abstraction, alongwith the formulation of an interface model as a discrete event system, allows the use of discretetechniques 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 anintersection, and an aircraft autopilot in a landing/go-around maneuver.1 IntroductionHuman-automation interaction is pervasive, occurring in consumer products (alarm clocks, VCRs,cellular phones), transportation systems (automobiles, commercial aircraft, air traffic control),scientific research platforms (unmanned ocean- and aerial-vehicles), and military systems (fleets ofsemi-autonomous and autonomous aircraft), among others. Often complicated by the underlyingdynamics of the physical system, human-automation interaction in aviation has been a controversialtopic since the advent of computers and their integration into the cockpit [1, 2, 3]. The aviationindustry has experienced many incidents and some accidents in which the pilot became confusedabout the current mode or could not anticipate the next mode in the automation [4, 5, 6, 7]. Thispotentially dangerous problem has been loosely termed mode confusion, and is often addressed inflight when the pilot has the time to devote attention to it, and resolved later with ad-hoc “fixes”.However, mode confusion may occur at critical times of flight: In 1994, all seven people on-boarddied during a test flight of the A-330 in Toulouse, France [8, 9]. The pilot had attempted tocomplete a go-around with a simulated engine failure, but an unanticipated combination of aircraftand engine dynamics, flight envelope protection schemes, and confusing interface indications ledto the aircraft’s stall. The accident involved the aircraft’s software, aerodynamics, as well as thepilot’s interaction with the combined system.We focus specifically on an aspect of this problem which we can quantify: the informationcontent presented in the interface. While graphical design of the interface is key in determininghow the user processes and interacts with information in the interface, we assume that the usercan and does process all information displayed. In human-automation systems, the interface allowsobservation of information regarding the underlying system dynamics and processes, as well ascontrol over specific behaviors through input devices in the interface. Too much information can2overwhelm the user; with too little information the user may not understand the system’s behavioror may not be able to perform the desired task. A key part of the problem of interface design andverification involves the appropriate selection of information from the underlying human-automationsystem which should be displayed to the human controlling the system.Although the engineering psychology community has historically dominated research on human-automation interaction, there have recently been efforts by the formal methods community [10,11, 12, 6, 13] as well as systems and control communities [14, 15] to address these safety-criticalproblems. Using model checkers, researchers in formal methods have evaluated such interfaces toidentify design problems [10, 11, 16] for discrete state models. In [12, 17, 18], the authors were notonly able to verify interfaces for a given task, but additionally formally determine the minimum setof information that must be displayed in the cockpit interface in order to safely complete a givenmaneuver. We believe that the continuous dynamics plays a crucial role in understanding anddesigning interfaces, and that it is necessary to introduce both a continuous dynamic component torepresent the physical dynamics of the underlying system, and a control component, into