Search NASASearch

Engineering topics

Mercer, Eric

Publications and source records attributed to Mercer, Eric.

An Approach to Quantify Workload in a System of Agents

The role of humans in aviation and other domains continues to shift from manual control to automation monitoring. Studies have found that humans are often poorly suited for monitoring roles, and workload can easily spike in off-nominal situations. Current workload measurement tools, like NASA TLX, use human operators to assess their own workload after using a prototype system. Such measures are used late in the design process and can result in ex- pensive alterations when problems are discovered. Our goal in this work is to provide a quantitative workload measure for use early in the design process. We leverage research in human cognition to de ne metrics that can measure workload on belief-desire-intentions based multi-agent systems. These measures can alert designers to potential workload issues early in design. We demonstrate the utility of our approach by characterizing quantitative differences in the workload for a single pilot operations model compared to a traditional two pilot model.

Single Pilot Operations

Symbolically Modeling Concurrent MCAPI Executions

Improper use of Inter-Process Communication (IPC) within concurrent systems often creates data races which can lead to bugs that are challenging to discover. Techniques that use Satisfiability Modulo Theories (SMT) problems to symbolically model possible executions of concurrent software have recently been proposed for use in the formal verification of software. In this work we describe a new technique for modeling executions of concurrent software that use a message passing API called MCAPI. Our technique uses an execution trace to create an SMT problem that symbolically models all possible concurrent executions and follows the same sequence of conditional branch outcomes as the provided execution trace. We check if there exists a satisfying assignment to the SMT problem with respect to specific safety properties. If such an assignment exists, it provides the conditions that lead to the violation of the property. We show how our method models behaviors of MCAPI applications that are ignored in previously published techniques.

Fischer, Topher