Engineering topics

Heymann, Michael

Publications and source records attributed to Heymann, Michael.

13 records

NASA NTRS2004

UIVerify: A Web-Based Tool for Verification and Automatic Generation of User Interfaces

In this poster, we describe a web-based tool for verification and automatic generation of user interfaces. The verification component of the tool accepts as input a model of a machine and a model of its interface, and checks that the interface is adequate (correct). The generation component of the tool accepts a model of a given machine and the user's task, and then generates a correct and succinct interface. This write-up will demonstrate the usefulness of the tool by verifying the correctness of a user interface to a flight-control system. The poster will include two more examples of using the tool: verification of the interface to an espresso machine, and automatic generation of a succinct interface to a large hypothetical machine.

Shiffman, Smadar↗

NASA NTRS2002

On Abstractions and Simplifications in the Design of Human-Automation Interfaces

This report addresses the design of human-automation interaction from a formal perspective that focuses on the information content of the interface, rather than the design of the graphical user interface. It also addresses the issue of the information provided to the user (e.g., user-manuals, training material, and all other resources). In this report, we propose a formal procedure for generating interfaces and user-manuals. The procedure is guided by two criteria: First, the interface must be correct, that is, with the given interface the user will be able to perform the specified tasks correctly. Second, the interface should be succinct. The report discusses the underlying concepts and the formal methods for this approach. Two examples are used to illustrate the procedure. The algorithm for constructing interfaces can be automated, and a preliminary software system for its implementation has been developed.

Heymann, Michael↗

NASA NTRS2002

Formal verification of human-automation interaction

This paper discusses a formal and rigorous approach to the analysis of operator interaction with machines. It addresses the acute problem of detecting design errors in human-machine interaction and focuses on verifying the correctness of the interaction in complex and automated control systems. The paper describes a systematic methodology for evaluating whether the interface provides the necessary information about the machine to enable the operator to perform a specified task successfully and unambiguously. It also addresses the adequacy of information provided to the user via training material (e.g., user manual) about the machine's behavior. The essentials of the methodology, which can be automated and applied to the verification of large systems, are illustrated by several examples and through a case study of pilot interaction with an autopilot aboard a modern commercial aircraft. The expected application of this methodology is an augmentation and enhancement, by formal verification, of human-automation interfaces.

Aviation↗

NASA NTRS2001

On Abstractions and Simplifications in the Design of Human-Automation Interfaces

This report addresses the design of human-automation interaction from a formal perspective that focuses on the information content of the interface, rather than the design of the graphical user interface. It also addresses the, issue of the information provided to the user (e.g., user-manuals, training material, and all other resources). In this report, we propose a formal procedure for generating interfaces and user-manuals. The procedure is guided by two criteria: First, the interface must be correct, i.e., that with the given interface the user will be able to perform the specified tasks correctly. Second, the interface should be as succinct as possible. The report discusses the underlying concepts and the formal methods for this approach. Several examples are used to illustrate the procedure. The algorithm for constructing interfaces can be automated, and a preliminary software system for its implementation has been developed.

Heymann, Michael↗

NASA NTRS1998

Control of Rate-Bounded Hybrid Systems with Liveness Specifications

In the present paper we examine the control problem for a class of composite hybrid machines (CHMs) that consist of concurrent operation (employing synchronous composition) of elementary hybrid machines (EHMs), that allows both signal sharing and event synchronization. A controller can then be coupled with the plant by means of synchronous composition. We confine our attention to controllers that interact with the system only through event synchronization. We present an initial investigation of synthesis of liveness controllers for hybrid machines. To this end we define open hybrid machines as systems that can interact with the environment through event synchronization and can be therefor be "driven" to their marked configuration by user (controller). Liveness specifications must be associated with timing constraints. We may require that for a specified time limit, every run reach a marked configuration within that time limit. Alternatively, a more relaxed specification may be that, for some (unspecified) global time bound, every run of the system reach a marked configuration within that time bound. Finally, the least restrictive liveness requirement is that every run reach a marked configuration within a finite time limit (but we do not insist on the existence of a global time bound for all runs).

Heymann, Michael↗

NASA NTRS1998

Methodology for Examining the Operator and the System Concurrently: Pilot Interaction with Automation

Complex system description is problematic when considering operator task activities interacting with system dynamics. Engineering languages have matured sufficiently to allow machine system description at various levels of depth and breadth but without operator synergy. Concurrently, Task Analysis methods have evolved along diverse lines enabling a description of the operator in the system from various paradigms but not describing the system. A void exists when attempting to view the system and the operator in the same plane. We propose a methodology employing descriptive languages from different domains viewed in a single dimension. Finite Automata (FA) languages describe the machine system in the proposed approach. Operator task specifications, a form of task analysis output, examine the operator activities within the system. Operator task specifications were then selected for discrete task activities and overlaid on the system description to examine operator inputs and subsequently view system responses. Unexpected (surprise) and undesirable system behavior was expected to emerge from this analysis. In this paper we shall first describe the methodology and show how the two perspectives, machine model and operator task specifications are integrated. Following we describe the process of doing such analysis using an example from cockpit automation. The methodology was employed in the analysis of a new function that was added to an existing automatic flight control system. We begin by defining a flight scenario involving all aspects of pilot interaction with the new function. Then, we proceed to develop a basic model of the machine behavior, in the context of pilot actions. Finally we superimpose the operator task specification on the machine model and perform the analysis. The proposed methodology may have broad appeal to system designers and human factors specialists. A common language for engineers of diverse domains is a strong point of this approach. Systems engineers may not fully understand operational considerations and human limitations, and human factors specialists may not be exposed to the full extent of system behavior. We hope the proposed methodology is adopted by both disciplines and in the process each assimilates a common language to address potential shortcomings of either approach separately.

Austin, David↗

NASA NTRS1998

Formal Analysis of Human Automation Interaction: The Problem of Display Correctness

This presentation attempted to develop a quantitative method for evaluating the effectiveness of autoflight displays. Researchers sought to develop a methodology for evaluation of display correctness and develop a methodology for display synthesis. Topics covered included: mode awareness, industry/research contributions, human-machine interface analysis, research objectives, modeling, flight guidance project and evaluation.

Degani, Asaf↗

NASA NTRS1998

A Formal Approach for Designing and Evaluating Procedures

Operator interaction with modern control systems is a topic of great concern in high-risk industries such as nuclear power and commercial aviation. The issues associated with such systems focus on the ability of the operators (e.g., pilots) to achieve mission goals safely while containing failures. Operators must be able to interact safely and reliably with highly automatic and complex systems across the full spectrum of possible operating conditions, including normal, abnormal, and emergency situations. In environments such as commercial aviation, operator interaction with the machine is specified through a set of standard operating procedures (SOP). A procedure represents a collective agreement on the 'best' way to perform a given task. The intent of this paper is to suggest a formal methodology, for designing and evaluating procedures, that is both reliable and systematic. Our approach involves two major elements: a model of the machine and a list of the operator's task specifications (goals). We use formal modeling paradigms for describing the system and super-imposing on it the operator's tasks. Such paradigms, based on recent frameworks such as Statecharts and Hierarchical Hybrid Machines appear to be adequate methods for analyzing operator interaction with modern control systems. To illustrate this methodology, we model and analyze the sequence of actions for an emergency procedure. The procedure, Irregular Engine Start, for a medium-range aircraft, specifies the sequence of immediate actions that must be performed by the crew to avoid an uncontrolled rise in engine temperature during start-up. A model of engine behavior during a hot start is constructed. It also describes the various actions that can be taken by the crew and the resulting outcomes. The model is then opened up as a tree of all possible action sequences. This action tree allows us to trace the correct sequences necessary to achieve the desired end-goal (secure and shut down of the engine). In conclusion, we argue that the current process of designing and evaluating procedures can be improved. We discuss the implications of this approach for designing and evaluating this and other types of procedures. We conclude with insights about the benefits and limitation of this methodology, and offer suggestions for future research.

Degani, Asaf↗

NASA NTRS1998

Formal Aspects of Human-Automation Interaction

While new versions of automated control systems such as flight guidance systems are introduced at a rapid pace, it is widely recognized that user interaction with these machines is increasingly problematic. One cause for this difficulty that is commonly cited in the literature, is the discrepancy between the machine's behavior and the operator's (e.g., pilot) expectations. This paper discusses a formal approach to the analysis of operator's interaction with complex automated control systems. We focus attention on the issue of interface correctness; that is, on the question whether the display provides adequate information about the machine's configurations (states, modes, and associated parameters) and transitions, so as to enable the operator to successfully perform the specified set of tasks. To perform the analysis several assumptions are made: (1) A complete formal model of the machine's behavior is available (e.g., as a state transition system, or as a hybrid-machine); (2) A specification of operator's tasks is available and can be formally described (e.g., the reliable and predictable transition between activities involved in executing a climb to a new altitude); (3) The pilot is well trained and has a correct 'mental' model of the machine's response-map. By 'comparing' the machine's model with the set of operator's tasks we formally (i.e., mathematically) evaluate two questions: 1) does the machine's output interface (display) enable the operator to determine, unambiguously, what the current configuration (e.g., mode) of the machine is, and 2) does the display enable the operator to determine, unambiguously, what the next configuration of the machine will be, in response to a specified interaction by the operator (e.g., engaging a mode or changing a parameter such as a speed or target altitude). This paper describes a methodology for conducting such an evaluation using examples from automated flight control systems of modem 'glass cockpit' jetliners. Taxonomy of the different types of discrepancies that lead to pilot inability to resolve the current and next configuration of the machine is suggested. Data from incident reports involving 'mode confusion' is used to corroborate these discrepancies. Finally, means for compensating, either by augmenting the display and/or the operator's 'mental model' are briefly mentioned.

Degani, Asaf↗

NASA NTRS1998

Some Formal Aspects of Human-Machine Interaction

While automated control systems such as autopilots and medical devices are introduced at a rapid pace, it is widely recognized that user interaction with these machines is problematic (Abbott, Slotte, & Stimson, 1996). One factor commonly cited in the literature is the discrepancy between the machine's behavior and the user's expectations. Design guidelines to reduce this discrepancy focus on two elements: (1) improvement of the "feedback" about what the automation is actually doing, and (2) improvement of the user's "mental model" of the automation (Norman, 1990; Sarter and Woods, 1995). This presentation describes a methodology for investigating these two elements via a formal (Le., mathematical) approach. The method involves two representations: (1) a finite state model of the machine's behavior (2) a finite state model of the user's knowledge and expectations about the machine's behavior. In the analysis phase we compare these two models and identify discrepancies. Such discrepancies can be compensated by augmenting the display and/or the user's model. A taxonomy of these discrepancies will be discussed using examples from automated Eight control systems of modern "glass cockpit" jetliners.

Degani, Asaf↗

NASA NTRS1997

Control Synthesis for a Class of Hybrid Systems Subject to Configuration-Based Safety Constraints

We examine a class of hybrid systems which we call Composite Hybrid Machines (CHM's) that consists of the concurrent (and partially synchronized) operation of Elementary Hybrid Machines (EHM's). Legal behavior, specified by a set of illegal configurations that the CHM may not enter, is to be achieved by the concurrent operation of the CHM with a suitably designed legal controller. In the present paper we focus on the problem of synthesizing a legal controller, whenever such a controller exists. More specifically, we address the problem of synthesizing the minimally restrictive legal controller. A controller is minimally restrictive if, when composed to operate concurrently with another legal controller, it will never interfere with the operation of the other controller and, therefore, can be composed to operate concurrently with any other controller that may be designed to achieve liveness specifications or optimality requirements without the need to reinvestigate or reverify legality of the composite controller. We confine our attention to a special class of CHM's where system dynamics is rate-limited and legal guards are conjunctions or disjunctions of atomic formulas in the dynamic variables (of the type x less than or equal to x(sub 0), or x greater than or equal to x(sub 0)). We present an algorithm for synthesis of the minimally restrictive legal controller. We demonstrate our approach by synthesizing a minimally restrictive controller for a steam boiler (the verification of which recently received a great deal of attention).

Heymann, Michael↗

NASA NTRS1991

An algebra of discrete event processes

This report deals with an algebraic framework for modeling and control of discrete event processes. The report consists of two parts. The first part is introductory, and consists of a tutorial survey of the theory of concurrency in the spirit of Hoare's CSP, and an examination of the suitability of such an algebraic framework for dealing with various aspects of discrete event control. To this end a new concurrency operator is introduced and it is shown how the resulting framework can be applied. It is further shown that a suitable theory that deals with the new concurrency operator must be developed. In the second part of the report the formal algebra of discrete event control is developed. At the present time the second part of the report is still an incomplete and occasionally tentative working paper.

Heymann, Michael↗

NASA NTRS1990

Concurrency and discrete event control

Much of discrete event control theory has been developed within the framework of automata and formal languages. An alternative approach inspired by the theories of process-algebra as developed in the computer science literature is presented. The framework, which rests on a new formalism of concurrency, can adequately handle nondeterminism and can be used for analysis of a wide range of discrete event phenomena.

Heymann, Michael↗