Menschenrechtsbildung im Zeitalter der Digitalisierung

Von Ulrike Zeigermann Im Zeitalter der Digitalisierung verändern neue Technologien, digitale Medien und online-Kommunikationskanäle in rasantem Tempo die Inhalte, Methoden, pädagogischen Praxen und theoretischen Grundlagen der Menschenrechtsbildung. Worin liegen Chancen und Herausforderungen dieser Entwicklung?

Menschenrechtsbildung im Wandel

In den letzten zehn Jahren hat es einen enormen Zuwachs an digitalen Lern-, Informations-und Kommunikationstechnologien gegeben, durch die mehr Menschen unabhängig von ihrer Herkunft, ihrem Bildungsabschluss, ihrem Einkommen und ihrer persönlichen Lebensumstände erreicht werden können.

Digitalisierung der Menschenrechtsbildung

Bereits heute werden neue digitale Angebote im Bereich der Menschenrechtsbildung zum Teil ergänzend, zum Teil an Stelle traditioneller direkter und interaktiver Kommunikation zwischen Lehrenden und Lernenden eingesetzt. Sie decken eine breite Palette von Formaten für diverse Zielgruppen auf unterschiedlichen Ebenen und in vielen Sprachen ab:

Herausforderungen und Spannungsfelder

Die neuen eLearning-Angebote im Bereich Menschenrechtspolitik erweitern nicht nur den Zugang durch Zeit-, Ort-und Situationsunabhängigkeit, sondern ermöglichen prinzipiell auch lebenslanges Lernen. Für junge Menschen, die mit digitalen Informations-und Kommunikationstechnologien aufgewachsen sind ("Digital Natives") können die neuen Formate ein Bildungsangebot sein, das näher an ihrer Lebensrealität ist und nebenbei zur Ausbildung technischer Qualifikationen dient, die gesellschaftlichen Teilhabe erleichtert notwendig ist. Forschung zu eLearning unterstreicht zudem,

• dass dadurch die Qualität der Lernerfahrungen besser werden kann [START_REF] Garrison | E-Learning in the 21st Century: A Framework for Research and Practice[END_REF];

•

  Abb. 1: Implementierung und Fragmentierung der Menschenrechtsbildung

  eLearning eine Chance für Nutzer*innen und Bildungsanbieter ist, um auf globalen Wettbewerb zu reagieren[START_REF] Anderson | The Theory and Practice of Online Learning[END_REF]);• eLearning kosteneffizienter als andere Bildungsformate ist[START_REF] Twigg | Improving Learning and Reducing Costs: Outcomes from Changing the Equation[END_REF]); • und weniger Zugangsbarrieren bestehen[START_REF] Bates | Technology, E-Learning and Distance Education[END_REF].Grundsätzlicher Vorteil sind die vereinfachten Möglichkeiten für internationale Interaktion und Kommunikation bei offenen Zugriff auf online-basierte Lernplattformen. Aber durchaus auch die transparente Zurechenbarkeit von Lerninhalten (Accountability).Gleichzeitig bedeutet dieVerfügbarkeit digitaler Informations-und Kommunikationstechnik (ICT) nicht automatisch mehr oder qualitativ bessere Menschenrechtsbildung oder gar gesellschaftliche Teilhabe. Die PISA-Studie von 2015 unterstreicht, dass sich sozio-ökonomisch bedingte Bildungsunterschiede in der Gesellschaft auch bei der Nutzung von ICT im Bildungssystem widerspiegeln (OECD 2015a). Es muss deshalb gefragt werden, wer von digitalen Bildungsangeboten nicht profitiert. Welche Personen haben keinen Zugang? Die Studie "Students, Computers and Learning. Making the connection" weist darauf hin, dass ohne solide naturwissenschaftliche und literarische Grundkenntnisse die meisten digitalen Bildungsangebote nicht zielführend genutzt und umfänglich ausgeschöpft werden können (OECD 2015b). Digitale Bildungsangebote werden zumeist individuell ausgewählt, was bei potenziell abnehmendem direkten Kontakt zwischen Lehrenden und Lernenden und einer durchaus zu beobachtenden abnehmenden Regulierung des Curriculums komplexes Lernen und inhaltliches Verständnis nicht unbedingt erleichtert. Die oben angeführten Beispiele für eLearning haben außerdem gezeigt, dass diese vor allem auf Englisch und von namhaften Bildungseinrichtungen aus dem globalen Norden angeboten werden. Kritiker*innen sprechen daher von einer zunehmenden hegemonialen Monopolisierung von Bildungsinhalten, Schwerpunktsetzungen im Curriculum, Serviceangeboten sowie verstärkter technologischer und pädagogischer Uniformität. Die Erklärung der Vereinten Nationen über Menschenrechtsbildung und -training bekräftigt, dass Staaten die Hauptverantwortung für die Förderung und Bereitstellung von Menschenrechtsbildung tragen, "die in einem Geist der Partizipation, Inklusion und Verantwortung zu entwickeln und umzusetzen ist" (Artikel 7). Gleichzeitig werden eLearning-Angebote zunehmend von privaten Anbieter*innen zur Verfügung gestellt, was ein paralleles Konkurrenzangebot zu den staatlichen Dienstleistern darstellt. Hierbei kann es zu einer Verschiebung der Bildungskosten auf die Lernenden kommen, was wiederum gesellschaftliche Ungleichheiten und neoliberale Logiken sowie den individuellen Druck nach Selbstoptimierung in lebenslangem Lernen verstärkt. eLearning kann somit auch die Gefahr der Kommerzialisierung von Lehre und Lernen verstärken. Zudem ist im Gegensatz zu klassischen Bildungsformaten bei der Nutzung von blended-Learning insbesondere der Schutz der Privatsphäre eine Herausforderung. Staaten bzw. deren öffentliche Institutionen haben eine menschenrechtliche Verantwortung (Accountability), jedoch können private, unternehmerische oder zivilgesellschaftliche Anbieter von eLearning-Formaten nach bisherigem internationalen Recht nicht für diskriminierende Praktiken oder (Daten-)Missbrauch zur Rechenschaft gezogen werden. Abschließend lässt sich feststellen, dass Menschenrechtsbildung in den letzten Jahrzehnten kontinuierlich weiterentwickelt und im formellen und informellen Bildungssektor verbreitet wurde und heute als eigenständiges Menschenrecht diskutiert wird. Die Herausforderungen haben sich dabei im Kontext neuer digitaler Informations-und Kommunikationstechnologien deutlich verändert. Das betrifft auch Anforderungen an Wissens-und Kompetenzziele (z.B. Mediensensibilität) und an eine kritische Auseinandersetzung mit Technik (z.B. Technikfolgenabschätzung, Industrialisierung 4.0). Die wesentlichen Chancen und Herausforderungen fasst Tabelle 1 noch einmal zusammen.

•

  Für Smartphone, Tablet oder Computer gibt es Apps mit denen Menschenrechtsfragen an verschiedene Zielgruppen adressiert werden können. Die Downloadstatistiken der Hersteller deuten darauf hin, dass bis zu 50.000 Installationen vorgenommen wurden (Amnesty Mag, Stand Oktober 2017). In den meisten Fällen bleibt die Zahl der Nutzer*innen aber deutlich darunter (z.B. UN Human Rights und UDHR Human Rights jeweils 5.000-10.000, Women's Human Rights und Geneva Human Rights Agenda jeweils 1.000-5.000 oder Human Rights Mapper und Child Rights Monitor 500 -1.000 Installationen, Stand Oktober 2017). • Darüber hinaus gibt es zunehmend Online-Spiele, die Abwägungsprozesse bei kritischen Menschenrechtsfragen simulieren und durch Rollenspiele für die Lage von Menschen sensibilisieren. Diverse Online-Spiele wurden zum Teil von Organen der Vereinten Nationen, wie "Against all Odds" von UNHCR, entwickelt, aber auch von zivilgesellschaftlichen Organisationen, wie Amnesty International (RespectMyRights), DoSomething (Karma Tycoon) oder Breakthrough (ICED) entwickelt. • Im Bereich der Hochschulbildung werden online immer häufiger sogenannte Massive Open Online Courses (MOOCs) als besondere Form der Fortbildung und Erweiterung von Fähigkeiten und Wissen von Universitäten, internationalen Organisationen und Forschungsinstituten angeboten, für die sich Menschen überall auf der Welt in Kurse aus den unterschiedlichen Disziplinen und Fächergruppen einschreiben können. Im Bereich Menschenrechte, wie auch in den anderen angebotenen Fächergruppen, wird der überwiegende Anteil der Online-Kurse auf Englisch und zum Erwerb eines Zertifikats kostenpflichtig angeboten.

Die aufgeführten Beispiele für onlinebasierte Lern-und Bildungsformate zeigen, dass Menschenrechtsbildung durch neue Technologien zu diversen Themen über Grenzen hinweg verfügbar ist und der Zugang zu diesen durch das Internet erleichtert wird. Die öffentlichen Statistiken über Installationen, Spieler*innen und eingeschriebene Personen sowie Kommentare und online-Bewertungen der E-Learning Programme deuten zudem darauf hin, dass diese Formate von einem wachsenden Personenkreis genutzt werden.


Jean-Baptiste Jeannin

Khalil Ghorbal

Yanni Kouskoulas

Ryan Gardner

Aurora Schmidt

Erik Zawadzki

André Platzer

A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System

come

Introduction

With growing air traffic, the airspace becomes more crowded, and the risk of airborne collisions between aircraft increases. In the 1970s, after a series of mid-air collisions, the Federal Aviation Administration (FAA) decided to develop an onboard collision avoidance system: the Traffic Alert and Collision Avoidance System (TCAS). This program had great success, and prevented many mid-air collisions over the years. Some accidents still happened; for example, a collision over Überlingen in 2002 occurred due to conflicting orders between TCAS and air traffic control. Airspace management will evolve significantly over the next decade with the introduction of the next-generation air traffic management system; this will create new requirements for collision avoidance. To meet these new requirements, the FAA has decided to develop a new system: the Next-Generation Airborne Collision Avoidance System, known as ACAS X [START_REF]Introduction to TCAS II[END_REF][START_REF] Holland | Optimizing the next generation collision avoidance system for safe, suitable, and acceptable operational performance[END_REF][START_REF] Kochenderfer | Next generation airborne collision avoidance system[END_REF].

Like TCAS, ACAS X avoids collisions by giving vertical guidance to an aircraft's pilot. A typical scenario involves two aircraft: the ownship where ACAS X is installed, and another aircraft called the intruder that is at risk of colliding with the ownship.

Table 1. Sample advisories and their modeling variables; full table in Technical Report [START_REF] Jeannin | A formally verified hybrid system for the next-generation airborne collision avoidance system[END_REF] ACAS X Specification [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF] Our ACAS X is designed to avoid Near Mid-Air Collisions (NMACs), situations where two aircraft come within r p = 500 ft horizontally and h p = 100 ft vertically [START_REF] Kochenderfer | Next generation airborne collision avoidance system[END_REF] of each other. The NMAC definition describes a volume centered around the ownship, shaped like a hockey puck of radius r p and half-height h p . In order to be accepted by pilots, and thus operationally suitable, ACAS X needs to strike a balance between giving advice that helps pilots avoid collisions but also minimizes interruptions. These goals oppose each other, and cannot both be perfectly met in the presence of unknown pilot behavior. This paper focuses on precisely characterizing the circumstances in which ACAS X gives advice that is safe. An integral part of the ACAS X development process, this work is intended to help ensure that the design of ACAS X is correct, potentially by identifying ways it should be adjusted.

Airborne Collision Avoidance System ACAS X. In order to prevent an NMAC with other aircraft, ACAS X uses various sensors to determine the position of the ownship, as well as the positions of any intruders [5]. It computes its estimate of the best pilot action by linearly interpolating a precomputed table of actions, and, if appropriate, issuing an advisory to avoid potential collisions [START_REF]Algorithm design description for the threat resolution module of ACAS X[END_REF] through a visual display and a voice message.

An advisory is a request to the pilot of the ownship to alter or maintain her vertical speed. ACAS X advisories are strictly vertical, and never request any horizontal maneuvering. Table 1 shows a sample of the advisories ACAS X can issue. For example, Do-Not-Climb (DNC) requests that the pilot not climb, and Climb-1500 (CL1500) requests that the pilot climb at more than 1500 ft/min. ACAS X can issue a total of 16 different advisories plus Clear-of-Conflict (COC), which indicates that no action is necessary. To comply with an advisory, the pilot must adjust her vertical rate to fall within the corresponding vertical rate range. Based on previous research [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF], the pilot is assumed to do so using a vertical acceleration of strength at least a r starting after a delay of at most d p after the advisory has been announced by ACAS X.

At the heart of ACAS X is a table whose domain describes possible configurations for the current state of an encounter, and whose range is a set of scores for each possible action [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF][START_REF] Kochenderfer | Compression of optimal value functions for Markov decision processes[END_REF]. The table is obtained from a Markov Decision Process (MDP) approximating the dynamics of the system in a discretization of the state-space, and optimized using dynamic programming to maximize the expected value of events over all future paths for each action [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF]. Near Mid-Air Collision events, for example, are associated with large negative values and issuing an advisory is associated with a small negative value. The policy is to choose the action with the highest expected value from a multilinear interpolation of grid points in this table. ACAS X uses this table, along with some heuristics, to determine the best action to take for the geometry in which it finds itself. Identifying Formally Verified Safe Regions. Since ACAS X involves both discrete advisories to the pilot and continuous dynamics of aircraft, it is natural to formally verify it using hybrid systems. However the complexity of ACAS X, which uses at its core a large lookup table-defining 29,212,664 interpolation regions within a 5-dimensional state-space-makes the direct use of hybrid systems verification techniques intractable. Our approach is different. It identifies safe regions in the state space of the system where the current positions and velocities of the aircraft ensure that a particular advisory, if followed, prevents all possible NMACs. Then it compares these regions to the configurations where the ACAS X table returns this same advisory. Moreover our safe regions are symbolic in their parameters, and can thus be easily adapted to new parameters.

Our results provide independent characterizations of the ACAS X behavior to provide a clear and complete picture of its performance. Our method can be used by the ACAS X development team in two ways. It provides a mathematical proof-with respect to a model-that ACAS X is absolutely safe for some configurations of the aircraft. Additionally, when ACAS X is not safe, it is able to identify unsafe or unexpected behaviors and suggests ways of correcting them.

Our approach of formally deriving safe regions then comparing them to the behavior of an industrial system is, as far as we are aware, the first of its kind in the formal verification of hybrid systems. The approach may be valuable for verifying or assessing properties of other systems with similar complexities, or also using large lookup tables, which is a common challenge in practice. Finally, the constraints we identified for safety are fairly general and could be used to analyze other collision avoidance systems.

The paper is organized as follows. After an overview of the method in Sect. 2, we start with a simple two-dimensional model assuming immediate reaction of the pilot in Sect. 3. We extend the model to account for the reaction time of the pilot in Sect. 4, and extend the results to a three-dimensional model in Sect. 5. In Sect. 6, we conduct an initial analysis of ACAS X whereby we compare the advisory recommended by a core component of ACAS X with our safe regions, identifying the circumstances where safety of those ACAS X advisories is guaranteed within our model.

Overview of the ACAS X Modelling Approach

To construct a safe region of an advisory for an aircraft, imagine following all allowable trajectories of the ownship relative to the intruder, accounting for every possible position of the ownship and its surrounding puck at every future moment in time. The union of all such positions of the puck describes a potentially unsafe region; for each point there exists a trajectory that results in an NMAC. Dually, if the intruder is outside this set, i.e., in the safe region, an NMAC cannot occur in the model. Fig. 1 depicts an example of a head-on encounter and its associated safe region for the advisory CL1500, projected in a vertical plane with both aircraft. It is plotted in a frame fixed to the intruder and centered at the initial position of the ownship. The ownship, surrounded by the puck, starts at position 1 and traces out a trajectory following the red curve. It first accelerates vertically with g/4 until reaching the desired vertical velocity of +1500 ft/min at position 3. It then climbs at +1500 ft/min, respecting the specification of Table 1. The green safe-region indicates starting points in the state space for which the aircraft will remain safe for the duration of the encounter. Note that no safe region exists above the trajectory since the ownship could accelerate vertically at greater than g/4 or climb more than +1500 ft/min, in accordance with Table 1.

Model of Dynamics.

Let us consider an encounter between two planes-ownship O and intruder I, as portrayed in Fig. 2. Following the notation of the ACAS X community [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF], let r be the horizontal distance between the aircraft and h the height of the intruder relative to the ownship. We assume that the relative horizontal velocity r v of the intruder with respect to the ownship is constant throughout the encounter. I.e., from a top view, the planes follow straight-line trajectories. Let θ v be the non-directed angle between r v and the line segment r. In the vertical dimension, we assume that the ownship's vertical velocity ḣ0 can vary at any moment, while the intruder's vertical velocity ḣ1 is fixed throughout the encounter. Moreover, we assume that the magnitude of the vertical acceleration of the ownship cannot exceed a d in absolute value.

For a typical encounter, r varies between 0 nmi and 7 nmi,3 h between -4,000 ft and 4,000 ft, r v between 0 kts and 1,000 kts, and ḣ0 and ḣ1 between -5,000 ft/min and +5,000 ft/min. The acceleration a d is usually g/2, where g is Earth's gravitational acceleration. The NMAC puck has radius r p = 500 ft and half-height h p = 100 ft.

Model of Advisories.

Recall that ACAS X prevents NMACs by giving advisories to the ownship's pilot. Every advisory, except COC, has a vertical rate range of the form (-∞, ḣf ] or [ ḣf , +∞) for some vertical rate ḣf (Table 1), which we call the target vertical velocity. We model any advisory by its corresponding target vertical velocity ḣf , and a binary variable w for its orientation, whose value is -1 if the vertical rate range of the advisory is (-∞, ḣf ] and +1 if it is [ ḣf , +∞). This symbolic encoding can represent many advisories and is robust to changes in the ACAS X advisory set.

Following ACAS X design work [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF], we assume that the ownship pilot complies with each advisory within d p seconds, and that she accelerates with acceleration at least a r to reach the target vertical velocity.

Safe Region for an Immediate Pilot Response

We present in this section a simplified version of the dynamics from Sect. 2. We give a hybrid model for this simplified system and prove its safety. The new assumptions will be relaxed in later sections to achieve the safety verification of the full model of Sect. 2.

Model. In this section, we assume that the ownship and intruder are flying headon (θ v = 180 • ). We also assume that the pilot reacts immediately to any advisory (d p = 0 s), and that the advisory COC is not allowed. These assumptions will be relaxed in Sect. 4 and Sect. 5. We assume that r is a scalar: if r ≥ 0 then the ownship is flying towards the intruder, otherwise it is flying away from it. Both cases could require an advisory. Since the ownship and intruder are flying head-on with straight line trajectories, there exists a vertical plane containing both their trajectories. In this plane, the puck becomes a rectangle centered around the ownship, of width 2r p and height 2h p , and there is an NMAC if and only if the intruder is in this rectangle (in gray on Fig. 1).

Differential Dynamic Logic and KeYmaera. We model our system using Differential Dynamic Logic dL [START_REF] Platzer | Differential dynamic logic for hybrid systems[END_REF][START_REF] Platzer | Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics[END_REF][START_REF] Platzer | Logics of dynamical systems[END_REF], a logic for reasoning about hybrid programs. The logic dL allows discrete assignments, control structures, and execution of differential equations. It is implemented in the theorem prover KeYmaera [START_REF] Platzer | KeYmaera: A hybrid theorem prover for hybrid systems[END_REF], that we use to verify our safe regions with respect to our models. All the KeYmaera models and proofs of this paper can be found at http://www.ls.cs.cmu.edu/pub/acasx.zip, and statistics in Technical Report [START_REF] Jeannin | A formally verified hybrid system for the next-generation airborne collision avoidance system[END_REF].

The dL formula for the model that we use in this section is given in Eq. ( 1).

1 rp ≥ 0 ∧ hp > 0 ∧ rv ≥ 0 ∧ ar > 0 ∧ (w = -1 ∨ w = 1) ∧ C impl (r, h, ḣ0) → 2 [( ( ?true ∪ ḣf := * ; (w := -1 ∪ w := 1); ?C impl (r, h, ḣ0); advisory := (w, ḣf ) ); 3 a := * ; {r = -rv, h = -ḣ0, ḣ 0 = a & w ḣ0 ≥ w ḣf ∨ wa ≥ ar} 4 ) * ] (|r| > rp ∨ |h| > hp) (1)
This formula of the form p → [α]q says all executions of program α starting in a state satisfying logical formula p end up in a state satisfying q. It is akin to the Hoare triple {p}α{q} with precondition p and postcondition q. The precondition in Eq. ( 1) imposes constraints on several constants, as well as the formula C impl (r, h, ḣ0 ) (defined below) that forces the intruder to be in a safe region for an initial advisory (w, ḣf ). We cannot guarantee safety if the intruder starts initially in an unsafe region. The postcondition encodes absence of NMAC. Line 2 expresses the action of the ACAS X system. The nondeterministic choice operator ∪ expresses that the system can either continue with the same advisory by doing nothing-just testing ?true-this ensures it always has a valid choice and cannot get stuck. Otherwise it can choose a new advisory (w, ḣf ) that passes the safety condition C impl (r, h, ḣ0 )-advisory will be the next message to the pilot. Line 3 expresses the action of the ownship, first nondeterministically choosing an arbitrary acceleration (a := * ) then following the continuous dynamics. The evolution of the variables r, h and ḣ0 is expressed by a differential equation, and requires (using the operator &) that the ownship evolves towards its target vertical velocity ḣf at acceleration a r (condition wa ≥ a r ), unless it has already reached vertical velocity ḣf (condition w ḣ0 ≥ w ḣf ). Finally, the star * on line 4 indicates that the program can be repeated any number of times, allowing the system to go through several advisories.

Implicit Formulation of the Safe Region. As explained in Sect. 2, we use a frame fixed to the intruder and with its origin at the initial position of the ownship (see Fig. 1).

First case: if w = +1 and ḣf ≥ ḣ0 . Fig. 1 shows, in red, a possible trajectory of an ownship following exactly the requirements of ACAS X. This nominal trajectory of the ownship is denoted by N . The pilot reacts immediately, and the ownship starts accelerating vertically with acceleration a r until reaching the target vertical velocity ḣf -describing a parabola-then climbs at vertical velocity ḣf along a straight line. Horizontally, the relative velocity r v remains constant. Integrating the differential equations in Eq. ( 1) line 3, the ownship position (r t , h t ) at time t along N is given by:

(r t , h t ) =    r v t , ar 2 t 2 + ḣ0 t if 0 ≤ t < ḣf -ḣ0 ar (a) r v t , ḣf t - ( ḣf -ḣ0) 2 2ar if ḣf -ḣ0 ar ≤ t (b) (2)
Recall that in the ACAS X specification, the ownship moves vertically with acceleration of at least a r , then continues with vertical velocity of at least ḣf . Therefore all possible future positions of the ownship are above the red nominal trajectory. An intruder is safe if its position is always either to the side of or under any puck centered on a point in N , that is:

∀t.∀r t .∀h t . (r t , h t ) ∈ N → |r -r t | > r p ∨ h -h t < -h p (3)
We call this formulation the implicit formulation of the safe region. It does not give explicit equations for the safe region border, but expresses them instead implicitly with respect to the nominal trajectory.

Generalization. The reasoning above is generalized to the case where ḣf < ḣ0 , and symmetrically to the case w = -1. The most general implicit formulation of the safe region is C impl in Fig. 3, and verified to be safe in KeYmaera:

Theorem 1 (Correctness of implicit safe regions). The dL formula given in Eq. (1) is valid. That is as long as the advisories obey formula C impl there will be no NMAC.

Explicit Formulation of the Safe Region. The implicit formulation of the safe region gives an intuitive understanding of where it is safe for the intruder to be. However, because it still contains quantifiers, its use comes at the extra cost of eliminating the quantifiers. An efficient comparison with the ACAS X table, as described in Sect. 6, can only be achieved with a quantifier-free, explicit formulation, that we present in this section. We show that both formulations are equivalent. As for the implicit formulation, we derive the equations for one representative case before generalizing them.

Implicit formulation

A(t, ht, ḣ0) ≡ 0 ≤ t < max(0, w( ḣf -ḣ0)) ar ∧ ht = war 2 t 2 + ḣ0t ∨ t ≥ max(0, w( ḣf -ḣ0)) ar ∧ ht = ḣf t - w max(0, w( ḣf -ḣ0)) 2 2ar C impl (r, h, ḣ0) ≡ ∀t.∀rt.∀ht. rt = rvt ∧ A(t, ht, ḣ0) → (|r -rt| > rp ∨ w(h -ht) < -hp) Explicit formulation case1(r, ḣ0) ≡ -rp ≤ r < -rp - rv min(0, w ḣ0) ar bound1(r, h, ḣ0) ≡ wr 2 v h < ar 2 (r + rp) 2 + wrv ḣ0(r + rp) -r 2 v hp case2(r, ḣ0) ≡ -rp - rv min(0, w ḣ0) ar ≤ r ≤ rp - rv min(0, w ḣ0) ar bound2(r, h, ḣ0) ≡ wh < - min(0, w ḣ0) 2 2ar -hp case3(r, ḣ0) ≡ rp - rv min(0, w ḣ0) ar < r ≤ rp + rv max(0, w( ḣf -ḣ0)) ar bound3(r, h, ḣ0) ≡ wr 2 v h < ar 2 (r -rp) 2 + wrv ḣ0(r -rp) -r 2 v hp case4(r, ḣ0) ≡ rp + rv max(0, w( ḣf -ḣ0)) ar < r bound4(r, h, ḣ0) ≡ (rv = 0) ∨ wrvh < w ḣf (r -rp) - rv max(0, w( ḣf -ḣ0)) 2 2ar -rvhp case5(r, ḣ0) ≡ -rp ≤ r < -rp + rv max(0, w( ḣf -ḣ0)) ar bound5(r, h, ḣ0) ≡ wr 2 v h < ar 2 (r + rp) 2 + wrv ḣ0(r + rp) -r 2 v hp case6(r, ḣ0) ≡ -rp + rv max(0, w( ḣf -ḣ0)) ar ≤ r bound6(r, h, ḣ0) ≡ (rv = 0 ∧ r > rp) ∨ wrvh < w ḣf (r + rp) - rv max(0, w( ḣf -ḣ0)) 2 2ar -rvhp C expl (r, h, ḣ0) ≡ w ḣf ≥ 0 → 4 i=1 (casei(r, ḣ0) → boundi(r, h, ḣ0)) ∧ w ḣf < 0 → 6 i=5
(casei(r, ḣ0) → boundi(r, h, ḣ0)) Fig. 3. Implicit and explicit formulations of the safe region for an immediate response

First case: if w = +1, r v > 0, ḣ0 < 0 and ḣf ≥ 0. We are in the case shown in Fig. 1 and described in detail above. The nominal trajectory N is given by Eq. (2)(a) and Eq. ( 2)(b). The boundary of the (green) safe region in Fig. 1 is drawn by either the bottom left hand corner, the bottom side or the bottom right hand corner of the puck. This boundary can be characterized by a set of equations: 0. positions left of the puck's initial position (r < -r p ) are in the safe region; 1. then the boundary follows the bottom left hand corner of the puck as it is going down the parabola of Eq. (2)(a); therefore for -r p ≤ r < -r p -rv ḣ0 ar , the position (r, h) is safe if and only if h < ar

2r 2 v (r + r p ) 2 + ḣ0
rv (r + r p ) -h p ; 2. following this, the boundary is along the bottom side of the puck as it is at the bottom of the parabola of Eq. (2)(a); therefore for -r p -rv ḣ0 a ≤ r ≤ r p -rv ḣ0 ar , the position (r, h) is in the safe region if and only if h < -

h < ḣf rv (r -r p ) - ( ḣf -ḣ0) 2 2ar -h p .
Generalization. The general case is given in the formula C expl of Fig. 3. The cases 1-4 and their associated bounds are for the case w ḣf ≥ 0, whereas cases 5 and 6 and associated bounds are for w ḣf < 0. We again use KeYmaera to formally prove that this explicit safe region formulation is equivalent to its implicit counterpart.

Lemma 1 (Correctness of explicit safe regions). If w = ±1, r p ≥ 0, h p > 0, r v ≥ 0 and a r > 0, then the conditions C impl (r, h, ḣ0 ) and C expl (r, h, ḣ0 ) are equivalent.

Safe Region for a Delayed Pilot Response

We generalize the model of Sect. 3 to account for a non-deterministic, non-zero pilot delay, and for periods of time where the system does not issue an advisory (i.e., COC).

Model. In this section, we still assume that the ownship and intruder are flying headon (θ v = 180 • ). We use the same conventions as in Sect. 3 for r and r v . The model includes an initial period where there is no compliance with any advisory-the ownship accelerates non-deterministically (within limits) in the vertical direction. As before, we derive the safe regions by considering all possible positions of the ownship's puck in all possible trajectories that might evolve in the encounter. To represent pilot delay for an advisory, the model assumes an immediate advisory, and period of non-compliance d p , representing the time it takes the pilot to respond. To represent COC, the model looks for a safe advisory it can issue d in the future if necessary, (d being the system delay, and shortest COC) so the period of non-compliance is d p + d .

≥ 0 ∧ h p > 0 ∧ r v ≥ 0 ∧ a r > 0 ∧ a d ≥ ∧d p ≥ 0 ∧ d ≥ 0 2 ∧(w = -1 ∨ w = 1) ∧ D impl (r, h, ḣ0 ,
7 {r = -r v , h = -ḣ0 , ḣ 0 = a, d = -1, t = 1 & 8 (t ≤ d ) ∧ (d ≤ 0 → w ḣ0 ≥ w ḣf ∨ wa ≥ a r )} 9 ) * ] (|r| > r p ∨ |h| > h p ) (4)
We modify the model of Eq. ( 1) to capture these new ideas, and obtain the model of Eq. ( 4), highlighting the differences in bold. The structure, precondition (lines 1 and 2) and postcondition (line 9) are similar. The clock d, if positive, represents the amount of time until the ownship pilot must respond to the current advisory to remain safe. Lines 3 to 5 represent the actions of the ACAS X system. As before, the system can continue with the same advisory (?true). Otherwise it can select a safe advisory (w, ḣf ) to be applied after at most delay d p ; or it can safely remain silent, displaying COC, if it knows an advisory (w, ḣf ) that is safe if applied after delay d p + d . In line 6, the pilot non-deterministically chooses an acceleration (a := * ), within some limit (wa ≥ -a d ). The set of differential equations in line 7 describes the system's dynamics, and the conditions in line 8 use the clock t to ensure that continuous time does not evolve longer than system delay d without a system response (t ≤ d ). Those conditions also ensure that when d ≤ 0 the pilot starts complying with the advisory. The model is structured so that the pilot can safely delay responding to an advisory for up to d p , and to an advisory associated with COC for up to d p + d -considering upper bounds on the reaction delay is necessary to get a formal proof of safety. Because of the loop in our model (line 9), the safety guarantees of this theorem apply to encounters whose advisories change as the encounter evolves, encounters with periods of no advisory, and encounters where the pilot exhibits some non-deterministic behavior.

In the rest of the section we use the same approach as in Sect. 3: we first derive an implicit formulation, then an equivalent explicit formulation of the safe region, and prove that the safe region guarantees that the intruder cannot cause an NMAC.

Formulations of the Safe Region. As in Sect. 3, let us place ourselves in the referential centered on the current position of the ownship and where the intruder is fixed, and let us first assume that the ownship receives an advisory (w, ḣf ) such that w = +1, and that Implicit formulation

B(t, ht, ḣ0, d) ≡ 0 ≤ t < max(0, d) ∧ ht = - wa d 2 t 2 + ḣ0t const ≡ h d = - wa d 2 max(0, d) 2 + ḣ0 max(0, d) ∧ ḣd -ḣ0 = -wa d max(0, d) D impl (r, h, ḣ0, d) ≡ ∀t.∀rt.∀ht.∀h d .∀ ḣd . rt = rvt ∧ (B(t, ht, ḣ0, d) ∨ const ∧ A(t -max(0, d), ht -h d , ḣd )) → (|r -rt| > rp ∨ w(h -ht) < -hp)
Explicit formulation

r d = rv max(0, d) ḣd = ḣ0 -wa d max(0, d) h d = - wa d 2 max(0, d) 2 + ḣ0 max(0, d) case7(r) ≡ -rp ≤ r ≤ rp bound7(r, h) ≡ wh < -hp case8(r) ≡ rp < r ≤ r d + rp case9(r) ≡ -rp ≤ r < r d -rp bound8(r, h) ≡ wr 2 v h < - a d 2 (r -rp) 2 + wrv ḣ0(r -rp) -r 2 v hp bound9(r, h) ≡ wr 2 v h < - a d 2 (r + rp) 2 + wrv ḣ0(r + rp) -r 2 v hp D expl (r, h, ḣ0, d) ≡ 9 i=7 (casei(r) → boundi(r, h)) ∧ C expl (r -r d , h -h d , ḣd )
Fig. 5. Implicit and explicit formulations of the safe region for a delayed response d ≥ 0. Let us focus on the period of time before the pilot reacts, which we henceforth call delay. During the delay, the ownship can take any vertical acceleration less than a d in absolute value, therefore its nominal trajectory N d is to accelerate the opposite way of the advisory, at acceleration -a d . Horizontally, its speed is constant at r v . It thus describes a delay parabola, in red on Fig. 4, and its position (r t , h t ) along the nominal trajectory for 0 ≤ t < d is given by (r t , h t ) = r v t, -a d 2 t 2 + ḣ0 t . After the delay, i.e., after time d, the nominal trajectory N d is the same as a nominal trajectory N from Sect. 3, translated by time d and by its position at time d given by r d = r t (d) and h d = h t (d), and starting with vertical velocity ḣd = ḣ0 -a d d. As in Sect. 3, we can now express the implicit formulation of the safe region:

∀t.∀r t .∀h t . (r t , h t ) ∈ N d → |r -r t | > r p ∨ h -h t < -h p
Symmetrically, the reasoning of this section extends to the case where w = -1. Moreover, we can handle cases where d < 0, i.e., after the pilot has reacted, by replacing d by max(0, d). The generalized implicit formulation of the safe region is given as D impl in Fig. 5. Note that it involves the expression A(t -max(0, d), h t -h d , ḣd ) from Fig. 3 capturing the implicit safe region of Sect. 3 translated by time max(0, d), vertical height h d , and starting at vertical speed ḣd . It is proved correct in KeYmaera.

Theorem 2 (Correctness of delayed safe regions). The dL formula given in Eq. (4) is valid. That is as long as the advisories obey formula D impl there will be no NMAC.

Similarly as in Sect. 4, we determine an explicit formulation of the safe region, called D expl in Fig. 5 based on Fig. 3, and prove it correct in KeYmaera.

Lemma 2 (Correctness of delayed explicit safe regions). If w = -1 or w = +1, r p ≥ 0, h p > 0, r v ≥ 0, a r > 0, a d ≥ 0, d p ≥ 0 and d ≥ 0 then the two conditions D impl (r, h, ḣ0 , d) and D expl (r, h, ḣ0 , d) are equivalent.

Reduction from 3D Dynamics to 2D Dynamics

In this section, we show that, with respect to our assumptions, any 3-dimensional encounter (Sect. 2) can be reduced to a 2-dimensional encounter (Sect. 3) without loss of generality. This is done using a change of reference frame and a dimension reduction.

For the sake of clarity, let us use a reference frame (O, i, j, k) fixed to the ownship (O). In this reference frame, the position of an intruder I is represented by the tuple (x, y, h), and the differential equation system that governs its motion is given by ẋ = r x , ẏ = r y , ḧ = a, where r x , r y and a remain constant as time evolves. Therefore, the motion of the encounter can be decoupled into a 2-dimensional horizontal encounter in the reference frame (O, i, j) (horizontal plane) and a 1-dimensional vertical encounter in the reference frame (O, k). In what follows, we reduce the horizontal encounter from a 2-dimensional motion to a 1-dimensional motion, thereby simplifying the problem conceptually and computationally by reducing its number of variables. First suppose r v > 0. The idea is to choose a reference frame (O , i , j ) in which one axis i is aligned with r v , such that no relative motion happens in the other direction j . Its fixed center O is defined as the orthogonal projection of point O on the direction of r v . The unit vector i is defined as rv rv , and j is a unit such that (O , i , j ) is positively oriented.

Let v |O (resp. v |O ) denote the coordinates of a vector v relative to the reference frame (O, i, j) (resp. (O , i , j )). Then, the coordinates for r and r v are: r |O = (x, y), r v |O = (r x , r y ), r |O = (s, n) and r v |O = (-r v , 0). The scalar product r • r v and the cross product r × r v are independent of the horizontal reference frame, therefore:

xr x + yr y = -sr v xr y -yr x = nr v (5)
Given r x and r y , Eqns. (5) imply that the coordinates (x, y) are uniquely determined by the choice of (s, n), as long as r v = 0 (using r 2 v = r 2 x + r 2 y ). For any 2-dimensional configuration, the encounter can thus be considered a head-on encounter where s plays the role of r and where a new puck radius, denoted s p , plays the role of r p .

Let us now determine the radius s p of the dimension-reduced encounter, and prove that the absence of NMAC in (O, i, j)-characterized by r 2 > r 2 p -is equivalent to the absence of NMAC in (O , i , j )-characterized by s 2 > s 2 p . Using (5): Since r v = 0, this implies r 2 = s 2 + n 2 . Therefore, r 2 > r 2 p if and only if s 2 + n 2 > r 2 p or equivalently s 2 > r 2 p -n 2 . If r 2 p -n 2 < 0, the direction of the vector r v does not intersect the puck, the inequality s 2 > r 2 p -n 2 is trivially true, and the encounter is safe. If r 2 p -n 2 ≥ 0, we choose the new puck radius s p for the dimension-reduced encounter as s p = r p 2 -n 2 ≥ 0, and the safety condition in (O , i , j ) becomes s 2 ≥ s 2 p . When θ v = 180 • , one has s = r, n = 0 and s p = r p as in Sect. 3-4. As the encounter evolves in (O, i, j) along ẋ = r x , ẏ = r y , its dimension-reduced version evolves in (O , i , j ) along the differential equations ṡ = -r v , ṅ = 0, obtained by differentiating Eqns. (5) and canceling r v . The following proposition, proved in KeYmaera, combines both dynamics and shows that the absence of an NMAC of radius r p in (O, i, j) is equivalent to the absence of an NMAC of radius s p in (O , i , j ).

r 2 v r 2 = r 2 v (x 2 + y 2 ) = (xr x + yr y ) 2 + (xr y -yr x ) 2 = r 2 v (s 2 + n 2 ) .
Proposition 1 (Horizontal Reduction). The following dL formula is valid

xr x + yr y = -sr v ∧ xr y -yr x = nr v ∧ x 2 + y 2 = n 2 + s 2 ∧ r 2 v = r 2 x + r 2 y → [ ẋ = r x , ẏ = r y , ṡ = -r v , ṅ = 0] x 2 + y 2 > r 2 p ↔ s 2 > r 2 p -n 2 (6)
Observe that the horizontal NMAC condition in (O , i , j ) only depends on the change of one variable rather than two. The proposition also applies to the special case r v = 0.

In this case the origin O is no longer defined, and Eqns. (5) are trivially true. The variables s and n are constants ( ṡ = 0, ṅ = 0), their initial values are only restricted by the condition n 2 + s 2 = x 2 + y 2 in the assumption of the proposition, but they are not unique. When the relative position between the two aircraft does not evolve over time, if the intruder is at a safe distance initially, the encounter is still safe for all time.

6 Initial Examination of the Safety of ACAS X

In this section, we use Theorem 1 to check the safety of advisories given by ACAS X. We focus on Run 12 (July 2014) of the optimized logic tables, a core component of ACAS X. The full policy of the system is built on these lookup tables and incorporates additional components to handle various operational scenarios. We compare the ACAS X table to the explicit regions where the pilot reacts immediately (Sect. 3). For a given initial state of an encounter, we query the first advisory issued by ACAS X and check its safety as identified in Theorem 1. In a real scenario, ACAS X could later strengthen or reverse the first advisory as the encounter evolves. But the safety of the first advisory is critical from an operational prospective as later changes are undesirable.

Our initial analysis considers a nominal set of discrete states-summarized in Table 2-of the ACAS X MDP model where no advisory has yet been issued. All compared states are head-on encounters: in a sense, they are the most obviously dangerous configurations. For those states, the ACAS X advisories are compared against the safe regions stated in Fig. 3. Overall, 4,461,600 discrete states were examined, among which 44,306 states (1.2%) did not meet the conditions of Fig. 3: 11,524 of these were unresolvable, i.e., the intruder was too close for any advisory to avoid NMAC; while 32,782 could have been resolved with a different safe advisory that satisfies Theorem 1.

Our analysis led to the identification of unexpected behavior in the ACAS X lookup tables. In some cases, the ACAS X advisory seems to induce an NMAC (Fig. 7), i.e., if the initial advisory is not strengthened or reverted later, an NMAC will occur. In other cases, the advisory does not seem to have any benefit, that is flying at vertical rates disallowed by the advisory would actually avoid NMAC while not all allowed vertical rates are safe. Of course, such unsafe advisories would be disallowed by our safe regions. Notice that these behaviors are not necessarily all deemed undesirable, as ACAS X tries to minimize alerting the pilot unless it has to do so; for some cases, ACAS X will strengthen the advisory later and hence does not issue a disruptive alert immediately. Fig. 7 depicts a typical example where the ACAS X advisory induces an NMAC. The ownship is flying from the left and the intruder from the right. As time counts down, the intruder evolves towards the ownship and an NMAC happens at t = 0. The original path of the ownship does not lead to an NMAC. However, ACAS X gives a Do-Not-Climb advisory. If the pilot, following this advisory, decides to stop climbing, its trajectory will cause an NMAC. (Other examples are in Technical Report [START_REF] Jeannin | A formally verified hybrid system for the next-generation airborne collision avoidance system[END_REF].)

The development of the safe regions gave an insight into possible improvements for the ACAS X system. Although we are not analyzing the complete system, nor the subsequent advisories, we automatically pointed out some subregions of the state space worth looking at. Some of those problems were independently identified by the ACAS X team using simulation-based testing, and will be addressed in subsequent revisions of the system. When extended to check contiguous regions of the state space, our approach will have the potential for a complete analysis of the system over all potential encounter configurations, thereby reducing vulnerability to the sampling of encounter scenarios.

Related Work

Kochenderfer and Chryssanthacopoulos [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF] describe the design of the ACAS X lookuptables. Their principled approach, based on optimizing an MDP, guarantees the selec-tion of optimal advisories according to a cost model. The state space and dynamics are discretized. Their notion of optimality depends on costs assigned to various events.

Von Essen and Giannakopoulou [START_REF] Von Essen | Analyzing the next generation airborne collision avoidance system[END_REF] use probabilistic model-checking to analyze an MDP based on [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF]. They investigate the probability of several undesirable events occurring. Because they ostensibly analyze an MDP, their work inherits many of the assumptions of ACAS X, including discretized dynamics. Their analysis depends heavily on the MDP considered and thus needs to be redone on every version of ACAS X.

Lygeros and Lynch [START_REF] Lygeros | On the formal verification of the TCAS conflict resolution algorithms[END_REF] use hybrid techniques to formally verify the TCAS conflict resolution algorithms. They assume-rather than prove-that TCAS ends up in a state where one aircraft has a climbing advisory and the other a descending advisory. They then prove (by hand) a lower bound on the vertical separation of both aircraft at the point of closest approach. In contrast, we do not assume anything on ACAS X's advisories.

Holland et al. [START_REF] Holland | Optimizing the next generation collision avoidance system for safe, suitable, and acceptable operational performance[END_REF] and Chludzinski [START_REF] Chludzinski | Evaluation of TCAS II version 7.1 using the FAA fast-time encounter generator model[END_REF] simulate large numbers of encounters, including tracks from recorded flight data, to evaluate the performance of ACAS X. These simulations account for high-fidelity details of an encounter, but they only cover a finite set of the continuous state space with no formal guarantees.

Tomlin et al. [START_REF] Tomlin | Conflict resolution for air traffic management: A study in multiagent hybrid systems[END_REF], Platzer and Clarke [START_REF] Platzer | Formal verification of curved flight collision avoidance maneuvers: A case study[END_REF], Loos et al. [15] and more recently Ghorbal et al. [START_REF] Ghorbal | Hybrid theorem proving of aerospace systems: Applications and challenges[END_REF] use hybrid systems approaches to design safe horizontal maneuvers for collision avoidance. Dowek et al. [START_REF] Dowek | Provably safe coordinated strategy for distributed conflict resolution[END_REF] and Galdino et al. [START_REF] Galdino | Formal verification of an optimal air traffic conflict resolution and recovery algorithm[END_REF] describe and verify in the PVS theorem prover a collision avoidance system of their design called KB3D.

Overall, our approach is different from previous complementary work in that:

unlike [START_REF] Von Essen | Analyzing the next generation airborne collision avoidance system[END_REF][START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF], we rely on an independent model from the one used to design ACAS X; unlike [START_REF] Dowek | Provably safe coordinated strategy for distributed conflict resolution[END_REF][START_REF] Galdino | Formal verification of an optimal air traffic conflict resolution and recovery algorithm[END_REF][START_REF] Ghorbal | Hybrid theorem proving of aerospace systems: Applications and challenges[END_REF]15,[START_REF] Platzer | Formal verification of curved flight collision avoidance maneuvers: A case study[END_REF][START_REF] Tomlin | Conflict resolution for air traffic management: A study in multiagent hybrid systems[END_REF] we analyze an independent industrial system and not a safeby-design system; unlike [START_REF] Dowek | Provably safe coordinated strategy for distributed conflict resolution[END_REF][START_REF] Von Essen | Analyzing the next generation airborne collision avoidance system[END_REF][START_REF] Galdino | Formal verification of an optimal air traffic conflict resolution and recovery algorithm[END_REF] our analysis uses realistic, continuous dynamics; unlike [START_REF] Lygeros | On the formal verification of the TCAS conflict resolution algorithms[END_REF][START_REF] Tomlin | Conflict resolution for air traffic management: A study in multiagent hybrid systems[END_REF] we provide universal safe regions that can be reused for new versions of ACAS X or even for new systems; unlike [START_REF] Chludzinski | Evaluation of TCAS II version 7.1 using the FAA fast-time encounter generator model[END_REF][START_REF] Holland | Optimizing the next generation collision avoidance system for safe, suitable, and acceptable operational performance[END_REF][START_REF] Kochenderfer | Correlated encounter model for cooperative aircraft in the national airspace system version 1[END_REF][START_REF] Lygeros | On the formal verification of the TCAS conflict resolution algorithms[END_REF][START_REF] Tomlin | Conflict resolution for air traffic management: A study in multiagent hybrid systems[END_REF], we provide mechanized proofs of correctness of our model.

Conclusion and Future Work

We developed a general strategy for analyzing the safety of complicated, real-world collision avoidance systems, and applied it to ACAS X. Our strategy identifies safe regions where an advisory is proved to always keep the aircraft clear of NMAC, under some assumptions. We identified states where ACAS X is provably safe, and fed others showing unexpected behaviors back to the ACAS X development team. The identified safe regions are independent from the version of ACAS X and can thus be reused for future versions. In future work, we plan to extend our hybrid model to account for curved trajectories of both aircraft as well as vertical acceleration of the intruder.

Fig. 1 .

 1 Fig. 1. Trajectory of ownship (red) and safe region for the intruder (green), immediate response

Fig. 2 .

 2 Fig. 2. Top view (left) and side view (right) of an encounter, with NMAC puck in gray

2 v

 2 ḣ2 0 2ar -h p ; 3. then the boundary follows the bottom right hand corner of the puck as it is going up the parabola of Eq. (2)(a); therefore for r p -rv ḣ0 ar < r ≤ r p + rv( ḣf -ḣ0) ar , the position (r, h) is safe if and only if h < ar 2r (r -r p ) 2 + ḣ0 rv (r -r p ) -h p ; 4. finally the boundary follows the bottom right hand corner of the puck as it is going up the straight line of Eq. (2)(b); therefore for r p + rv( ḣf -ḣ0) ar < r, the position (r, h) is in the safe region if and only if

Fig. 4 .

 4 Fig.4. Trajectory of the ownship (red) and safe region for the intruder (green), delayed response1 r p ≥ 0 ∧ h p > 0 ∧ r v ≥ 0 ∧ a r > 0 ∧ a d ≥ ∧d p ≥ 0 ∧ d ≥ 0 2 ∧(w = -1 ∨ w = 1) ∧ D impl (r, h, ḣ0 , d) → 3 [( ?true ∪ ḣf := * ; (w := -1 ∪ w := 1);

  d) → 3 [( ?true ∪ ḣf := * ; (w := -1 ∪ w := 1); 4 (d := d p ; ?D impl (r, h, ḣ0 , d); advisory := (w, ḣf ) ∪ 5 d := d p + d ; ?D impl (r, h, ḣ0 , d); advisory := COC) ;6 a := * ; ?(wa ≥ -a d ); t := 0;

Fig. 6 Fig. 6 .

 66 Fig. 6. Top view of the two reference frames

Fig. 7 .

 7 Fig. 7. Original ownship path (cyan) and intruder path (red) vs. ownship responding to a do-notclimb (DNC) advisory issued by the ACAS X tables in starting state: r = 4,000 ft, rv = 200 ft/s, θv = 180 • , h = 600 ft, ḣ0 = 1,980 ft/min, ḣ1 = -1,500 ft/min.

Table 2 .

 2 Summary of the points of the state space at which we examined ACAS X

		Range Relative speed	Angle	Relative Vertical rates Previous
		r (ft)	rv (ft/s)	θv (degrees) altitude h (ft) ḣ0, ḣ1 (ft/s) advisory
	Min value	1,500	100	180 •	-4,000	-41.67	None
	Max value	200,000	2,200	180 •	4,000	41.67	None
	Number of values 80	10	1	33	13 2	1

We use units most common in the aerospace community, even though they are not part of the international system, including nautical miles nmi (1,852 metres), knots kts (nautical miles per hour), feet ft (0.3048 meter) and minutes min (60 seconds).

Jeannin, Ghorbal, Kouskoulas, Gardner, Schmidt, Zawadzki and Platzer

Acknowledgments. The authors would like to warmly thank Stefan Mitsch and Jan-David Quesel for their support of the KeYmaera tool. The authors would also like to thank Jeff Brush, Jessica Holland, Robert Klaus, Barbara Kobzik-Juul, Mykel Kochenderfer, Ted Londner, Sarah Loos, Ed Morehouse, Wes Olson, Michael Owen, Joshua Silbermann, Neal Suchy, and the ACAS X development team for interesting remarks.

This research was conducted under the sponsorship of the Federal Aviation Administration Traffic Alert & Collision Avoidance System (TCAS) Program Office (PO) AJM-233 under contract number DTFAWA-11-C-00074. Additionally, support for the basic verification technology used as a foundation for this research was provided by the National Science Foundation under NSF CAREER Award CNS-1054246.