Using formal methods to reason about taskload and resource conflicts in simulated air traffic scenarios

• Published in: Innovations in systems and software engineering 2018-03, Vol.14 (1), p.1-14
• Main Authors: Houser, Adam, Ma, Lanssie Mingyue, Feigh, Karen M., Bolton, Matthew L.
• Format: Article
• Language: English
• Subjects: Air traffic; Architecture; Artificial Intelligence; Complex systems; Complexity; Computer Applications; Computer Science; Computer simulation; Human behavior; Original Paper; Queues; Simulation; Software Engineering; Taskload; Traffic conflicts
• ISSN: 1614-5046; 1614-5054
• DOI: 10.1007/s11334-017-0305-2

In complex environments, like the modern air traffic system, interactions between human operators and other system agents can profoundly impact system performance. System complexity can make it difficult to determine all of the situations where issues can arise. Simulation and formal verification have been used separately to explore the role of humans in complex systems. However, both have problems that limit their usefulness. In this paper, we describe a method that allows interesting conditions related to human taskload and resource conflicts between agents to be discovered and evaluated in high fidelity through the synergistic use of formal verification and simulation. The core of this method is based on a formal modeling architecture that represents original, agent-based simulation constructs using computationally efficient abstractions that ensure the temporal and ordinal relationships between simulation events (actions) are represented realistically. Taskload for each agent is represented using a priority queue model where only a limited number of actions can be performed or remembered by a human at a given time. Resources affected by agent behaviors are associated with actions so that resources can be reasoned about at the action level. We discuss our method and its formal architecture. We describe how the method can be used to find taskload and resource conflict conditions through the use of formal, checkable specification properties. We then use a simple air traffic example to demonstrate the ability of our method to find interesting taskload and resource conflict conditions around a simulation trace. The implications of this method are discussed and directions for future work are explored.