by Elena De Santis, Maria Domenica Di Benedetto and Giordano Pola
We present a formal framework for analysing the impact of non-nominal operating modes on the safety of next generation ATM procedures under study in the SESAR 2020 Concept of Operation. Efficient complexity reduction algorithms are also derived for applying the proposed methodology to realistic large-scale ATM systems.
Air Traffic Management (ATM) is an important application domain exhibiting many features of CPS such as heterogeneity, complexity, and human operators in-the-loop.
Several disciplines are being used to assist ATM experts in the design of robust procedures; among these, of particular relevance is Resilience Engineering [3]. Resilience indicates that operations and organizations are capable of resisting a variety of demands and capable of recovering from variations, degradations, disruptions, and any condition affecting the stability of the operation or organization. In other words, Resilience Engineering addresses the design of joint cognitive systems, both in nominal and non-nominal conditions. However, because of the complexity of ATM joint cognitive systems, Resilience Engineering as applied to ATM is at an early stage of development. Formal mathematical models and analysis methods offer a key complementary approach that is needed to render Resilience Engineering effectively applicable to ATM systems. Making Resilience Engineering applicable to ATM was the main goal of the SESAR WP-E Research Project “Mathematical Approach towards Resilience Engineering in ATM (MAREA)”.
Figure 1: A possible scenario of the TMA T1 operation. Standard instrument departure routes are depicted in green, standard terminal arrival routes in red, and cruise routes at a lower flight level in blue.
Among the topics included in MAREA, of fundamental importance in the analysis of novel ATM procedures was the study of the impact of non-nominal operating modes on the safety of the overall system. To tackle this important problem we proposed in [2] a formal approach that is based on the use of a number of relevant hybrid systems’ techniques, including compositional hybrid systems’ modelling and hybrid observers’ synthesis.
While aircraft dynamics is commonly described by differential equations, pilots’ and air traffic controllers’ behaviours are well modelled by finite state machines, whose discrete states and transitions mimic the procedure the agents are requested to follow. Hybrid systems’ formalism, featuring both discrete and continuous dynamics, is characterized by an expressive power that we proved to be general enough to adequately describe ATM systems, both in nominal and non-nominal conditions. While nominal modes of operation are dictated by the procedure the agents are requested to follow, non-nominal modes may originate from several causes, including malfunction or disruption of technical devices or unpredictable behaviour of human operators in-the-loop. To study the impact of non-nominal operating modes on the safety of the ATM procedures we used the notion of critical observability [1]. This notion corresponds to the possibility of detecting whether the current discrete state of a hybrid system is in a critical set, representing unsafe, un-allowed or non–nominal situations. When a hybrid system exhibits this property, a hybrid observer can be constructed which automatically detects the criticality of the current discrete state.
Our first investigation of critical observability considered each agent of ATM systems in isolation. However, in multi-agent ATM scenarios, agents cannot be considered in isolation because their interaction is responsible for the occurrence of unsafe situations that cannot be captured in isolation. For this reason, we proposed a compositional hybrid systems framework that describes the behaviour of each agent as well as their interaction. This framework can be viewed as a generalization of the classical notion of serial composition to a multi-agent setting, and provides a systematic way to study critical observability of multi-agent systems. More precisely, models are first created of each agent with a hybrid system, then, by applying the compositional rules, a unique hybrid system is obtained. A critical relation is then defined which describes the occurrence of safety-critical situations in the composed hybrid system. Studying safety in multi-agent ATM scenarios then translates to studying critical observability of the obtained (composed) hybrid system with respect to the critical relation.
Although formally sound, this approach is hardly applicable to realistic scenarios because of the large number of variables involved. To overcome these difficulties we proposed algorithms based on bisimulation theory, widely used in the area of formal methods to mitigate software verification.
We analysed the Terminal Maneuvering Area (TMA) T1 operation, a procedure selected within the MAREA consortium as a benchmark, exhibiting most relevant features arising in the novel SESAR 2020 Concept of Operation. We considered a scenario involving 25 agents, comprising more than 1.68 x 1018 discrete states. We showed that this procedure is not critically observable. This implies that there are safety-critical configurations which cannot be detected by pilots or air traffic controllers. In other words, in some situations, not only is the human operator’s awareness of a safety critical situation incorrect, but furthermore, it cannot be improved before a safety-critical situation occurs. This analysis also proposed alternative solutions which ensure safety of the procedure.
We wish to thank Henk Blom and Mariken Everdij (NLR) for fruitful discussions on this paper.
Link: http://dews.univaq.it/
References:
[1] E. De Santis et al: “Critical Observability of a Class of Hybrid Systems and Application to ATM systems”, in “Stochastic Hybrid Systems: Theory and Safety Critical Applications”, LNCIS 337
[2] E. De Santis et al: “Final modelling and analysis of SESAR 2020 ConOps”, Report MAREA D4.4, http://complexworld.eu/wiki/File:D4.4-v1.0.pdf
[3] Resilience Engineering Perspectives, Preparation and Restoration, Vol. 2, Ashgate, England, 2009.
Please contact:
Elena De Santis, Maria Domenica Di Benedetto and Giordano Pola, Center of Excellence for Research DEWS, University of L’Aquila, Italy.
E-mail: {elena.desantis, mariadomenica.dibenedetto, giordano.pola} @univaq.it
