Symbolic-numeric methods in reasoning about the design of future air traffic management

In our busy skies and airports, commercial aviation critically depends on air traffic management (ATM). ATM forms a complex Cyber Physical Human System (CPHS) that involves dynamic interactions under uncertainties (e.g. weather) between distributed human decision makers (e.g. pilots and air traffic controllers), dynamical systems (e.g. aircraft control and decision-support systems) and infrastructure (e.g. airports). Over decades, this complex CPHS has evolved to its current form through systematic learning from incident and accident investigations. This has made current ATM resilient and safe under a broad spectrum of disturbances. Novel technology and growing demands in commercial air transport form strong drivers for the design and implementation of significant changes in ATM's complex CPHS. Due to dynamic interactions between distributed CPHS entities, such changes may trigger unforeseen emergent behaviour. The challenge is to identify such behaviour already during the early design phase of future ATM. This asks for symbolic-numerical methods for reasoning about the performance, including incidents and accidents, of a future ATM's CPHS design, and to feedback such performance learning to the CPHS design. This presentation explains how the identification and understanding of unknown emergent behaviour of a CPHS design for future ATM can be accomplished through making integrated use of various formal methods, such as compositional model development of large stochastic hybrid systems [1], managing bi-similarity transformations [2-3], as well as conducting probabilistic reachability analysis through rare event simulation [4-5]. The practical use of these methods is illustrated to CPHS designs of future ATM, where the role of air traffic control is replaced by advanced decision-support to pilots. Results obtained for this future ATM design reveal remarkable emergent behavior [6] that was not foreseen by the CPHS design team. This challenging ATM application also illustrates needs for further development of symbolic-numeric methods for the evaluation of complex CPHS designs.