Safety criticality analysis of complex Air Traffic Management systems via compositional bisimulation*

The inherent complexity of Air Traffic Management (ATM) systems makes formal analysis a difficult task. Complexity of ATM systems is mainly due to their heterogeneity and to the large number of their sub–components. While heterogeneity in the diverse components of ATM systems has been effectively approached by resorting to compositional hybrid-system formalism, methods for the formal analysis of realistic large scale ATM systems are few at present. In this paper we provide an approach to deal with the analysis of safety criticality for complex ATM systems. The approach proposed is centered on a mathematical representation of ATM systems, termed arenas of finite state machines, which are effective in modeling the behavior of ATM agents both in nominal and non–nominal modes of operation, as well as their interaction. Complexity reduction techniques are then proposed as a tool to analyze realistic ATM scenarios.