NASA/TM–2010–216862

A Criteria Standard for Conflict

Resolution: A Vision for

Guaranteeing the Safety of

Self-Separation in NextGen

C ́esar Mu ̃noz, Ricky Butler, Anthony Narkawicz, Jeffrey Maddalon, and George Hagen

Langley Research Center, Hampton, Virginia

October 2010
NASA STI Program . . . in Profile

Since its founding, NASA has been dedicated

to the advancement of aeronautics and space

science. The NASA scientific and technical

information (STI) program plays a key part

in helping NASA maintain this important

role.

The NASA STI Program operates under the

auspices of the Agency Chief Information

Officer. It collects, organizes, provides for

archiving, and disseminates NASA’s STI.

The NASA STI Program provides access to

the NASA Aeronautics and Space Database

and its public interface, the NASA Technical

Report Server, thus providing one of the

largest collection of aeronautical and space

science STI in the world. Results are

published in both non-NASA channels and

by NASA in the NASA STI Report Series,

which includes the following report types:

• TECHNICAL PUBLICATION. Reports of

completed research or a major significant

phase of research that present the results

of NASA programs and include extensive

data or theoretical analysis. Includes

compilations of significant scientific and

technical data and information deemed to

be of continuing reference value. NASA

counterpart of peer-reviewed formal

professional papers, but having less

stringent limitations on manuscript length

and extent of graphic presentations.

• TECHNICAL MEMORANDUM.

Scientific and technical findings that are

preliminary or of specialized interest, e.g.,

quick release reports, working papers, and

bibliographies that contain minimal

annotation. Does not contain extensive

analysis.

• CONTRACTOR REPORT. Scientific and

technical findings by NASA-sponsored

contractors and grantees.

• CONFERENCE PUBLICATION.

Collected papers from scientific and

technical conferences, symposia, seminars,

or other meetings sponsored or

co-sponsored by NASA.

• SPECIAL PUBLICATION. Scientific,

technical, or historical information from

NASA programs, projects, and missions,

often concerned with subjects having

substantial public interest.

• TECHNICAL TRANSLATION. Englishlanguage translations of foreign scientific

and technical material pertinent to

NASA’s mission.

Specialized services also include creating

custom thesauri, building customized

databases, and organizing and publishing

research results.

For more information about the NASA STI

Program, see the following:

• Access the NASA STI program home page

at http://www.sti.nasa.gov

• E-mail your question via the Internet to

help@sti.nasa.gov

• Fax your question to the NASA STI

Help Desk at 443-757-5803

• Phone the NASA STI Help Desk at

443-757-5802

• Write to:

NASA STI Help Desk

NASA Center for AeroSpace

Information

7115 Standard Drive

Hanover, MD 21076–1320
NASA/TM–2010–216862

A Criteria Standard for Conflict

Resolution: A Vision for

Guaranteeing the Safety of

Self-Separation in NextGen

C ́esar Mu ̃noz, Ricky Butler, Anthony Narkawicz, Jeffrey Maddalon, and George Hagen

Langley Research Center, Hampton, Virginia

National Aeronautics and

Space Administration

Langley Research Center

Hampton, Virginia 23681-2199

October 2010
The use of trademarks or names of manufacturers in this report is for accurate reporting and does not

constitute an offical endorsement, either expressed or implied, of such products or manufacturers by the

National Aeronautics and Space Administration.

Available from:

NASA Center for AeroSpace Information

7115 Standard Drive

Hanover, MD 21076-1320

443-757-5802
Abstract

Distributed approaches for conflict resolution rely on analyzing the behavior of

each aircraft to ensure that system-wide safety properties are maintained. This

paper presents the criteria method, which increases the quality and efficiency

of a safety assurance analysis for distributed air traffic concepts. The criteria

standard is shown to provide two key safety properties: safe separation when

only one aircraft maneuvers and safe separation when both aircraft maneuver

at the same time. This approach is complemented with strong guarantees of

correct operation through formal verification. To show that an algorithm is

correct, i.e., that it always meets its specified safety property, one must only

show that the algorithm satisfies the criteria. Once this is done, then the algorithm inherits the safety properties of the criteria. An important consequence

of this approach is that there is no requirement that both aircraft execute

the same conflict resolution algorithm. Therefore, the criteria approach allows different avionics manufacturers or even different airlines to use different

algorithms, each optimized according to their own proprietary concerns.

1
Contents

1 Introduction 3

2 Notation 5

3 Criteria 6

3.1 Horizontal Criterion for Conflict Resolution . . . . . . . . . . 7

3.2 Horizontal Criterion for Loss of Separation . . . . . . . . . . . 8

3.3 Vertical Criterion for Conflict Resolution . . . . . . . . . . . . 9

3.3.1 Vertical Criterion For Vertical Speed Only . . . . . . . 11

3.3.2 The General Vertical Criterion Formula . . . . . . . . . 13

3.4 Vertical Criterion for Loss of Separation Recovery . . . . . . . 15

3.5 3-Dimensional Criteria . . . . . . . . . . . . . . . . . . . . . . 16

4 Correctness Theorems 17

4.1 Horizontal Correctness Theorems . . . . . . . . . . . . . . . . 17

4.1.1 Conflict Case . . . . . . . . . . . . . . . . . . . . . . . 17

4.1.2 Loss of Separation Case . . . . . . . . . . . . . . . . . 18

4.2 Vertical Correctness Theorems . . . . . . . . . . . . . . . . . . 20

4.2.1 Conflict Case . . . . . . . . . . . . . . . . . . . . . . . 20

4.2.2 Loss of Separation Case . . . . . . . . . . . . . . . . . 20

4.3 3-D Correctness Theorems . . . . . . . . . . . . . . . . . . . . 21

5 Choice of Direction Parameter,  22

5.1 Horizontal Direction Parameter . . . . . . . . . . . . . . . . . 23

5.2 Vertical Direction . . . . . . . . . . . . . . . . . . . . . . . . . 24

6 International Standard for State-Based Coordination 26

7 Implications for Strategic Algorithms 27

8 Conclusions 28

A Summary of Notation 31

B Summary of Criteria 32

2
1 Introduction

Two basic approaches for conflict detection and resolution are being considered

for the NextGen Airspace: (1) a centralized concept, where a single authority

detects conflicts and makes resolution decisions for several aircraft, and (2) a

distributed concept, where the elements of the system make individual decisions about maintaining conflict-free trajectories. There are advantages and

disadvantages to each approach, and any future air traffic system will likely

have both centralized and decentralized features. If the system is primarily

centralized and highly automated, then the safety of the system hinges on

assuring the correctness of the software performing the separation function

and on many other factors. Alternatively, in a distributed approach the safety

of the system cannot just rely on examining the software that is running on

the aircraft but must involve analyzing a distributed property between the aircraft. For this reason, the safety analysis of a distributed system is probably

more complex than a similar analysis for a centralized approach. This paper presents a criteria method, which simplifies the analysis of self separation

while expanding the possibility of diverse applications.

This criteria method may be used for distributed airspace systems where

aircraft execute different resolution algorithms, and it can also be used where

each aircraft execute the same algorithm. The second approach was taken

in the design of the Traffic Collision Avoidance System (TCAS). A diverse

international committee met for many years and came to agreement on the

TCAS II algorithm [8]. The first approach is attractive because a large number of resolution algorithms have been proposed in recent years (see [4] for a

collection of examples) and it is difficult to imagine that everyone will agree on

mandating a single algorithm. The criteria standard allows different avionics

manufactures and perhaps different airlines to implement different algorithms,

which are optimized for different proprietary goals. All of these algorithms will

interact safely, provided that each algorithm is shown to meet the criteria. In

this concept the international community agrees on the criteria rather than on

a single algorithm. This paper presents proven results that if two algorithms

both meet the criteria presented in this paper, then their combined behavior

is safe with respect to separation, i.e., the combined effect of their maneuvers

resolves the conflict.

This paper introduces criteria that provide strong guarantees of safe separation as long as the aircraft use state-based conflict resolution algorithms that

satisfy the common criteria, even when the algorithms are different. Safe separation is guaranteed for all encounter geometries if only one aircraft maneuvers

or if both aircraft maneuver to avoid the conflict. When both aircraft maneuver to avoid a conflict, we must ensure that the combination of the maneuvers

is safe. One way to achieve this coordinated behavior is for the aircraft to

3
explicitly communicate their intentions: “I will climb, so you should descend.”

However, we focus on the concept of implicit coordination, which means that

when two aircraft maneuver, the combined effect resolves the conflict without

any additional communication between them. Only ADS-B surveillance data

that is periodically broadcast by all appropriately equipped aircraft is used

in implicit coordination. The concept presented here will guarantee implicit

coordination for arbitrary combinations of tactical guidance maneuvers (e.g.,

track only, ground speed only, vertical speed only). For example, one aircraft may select a ground-speed solution and the other aircraft a track-only

solution, and the combined effect will still maintain separation. There are

several other advantages that accrue from the implicit coordination approach,

including: (1) less demand on the radio frequency spectrum, (2) the concept

is procedurally simpler and hence less error prone, and (3) less workload on

the pilot and controllers.

This paper presents a framework for facilitating the verification of many

different algorithms in a mathematically rigorous way, i.e., via formal methods.

The concept is built on the idea of having an intermediate verification layer,

called the criteria layer. This is illustrated in Figure 1: The top layer (yellow)

Figure 1. Criteria Concept

defines mathematical correctness for both horizontal maneuvers and vertical

maneuvers. The middle layer (light blue) contains the equations that define

the criteria, and the bottom layer contains the conflict resolution algorithms.

The middle layer is the key to achieving our goals. The correctness statements

at the top level are state-based, that is, they are specified in terms of the

4
current position and velocity vectors of the two aircraft. There is no attempt

to incorporate intent information in this formulation.

The criteria layer consists of mathematical formulas that are shown to be

sufficient to guarantee correctness via formal mathematical proofs. The formulas are analytically defined so that many different algorithms can be checked

against the criteria in a straight-forward way. Also, the criteria only use information available to the local aircraft. Each algorithm is then separately

shown to satisfy the criteria and thereby inherits the system-wide safety properties. The criteria can also be used as a filter on any resolution algorithm

that computes multiple solutions. Only solutions that meet the criteria are

allowed to be executed and hence this revised, filtered algorithm will inherit

all of the coordination properties.

This paper proceeds first with a description of notation in Section 2. Section 3 presents individual criteria for different kinds of situations: horizontal

conflict resolution, horizontal loss of separation recovery, vertical conflict resolution, and vertical loss of separation recovery. Criteria are also presented

that combine the horizontal and vertical criteria in the case of 3-dimensional

conflict and loss of separation. Section 4 provides theorems stating that the

criteria guarantee independence and coordination. Most resolution maneuvers

have two complementary solutions: turn left or right, go up or down, etc.

Section 5 describes how an algorithm should choose between these complementary resolutions. In Section 6 there is a discussion about the issues that

might arise within an international committee that seeks to adopt the criteria

concept. Finally, Section 7 discusses how the criteria standard would work in

conjunction with strategic resolution methods that rely on intent information.

The contributions of this paper include: (1) a vision for guaranteeing the

safety of the next generation air-traffic management system, based on the

criteria approach, (2) the proposal of a specific set of criteria for meeting this

vision, and (3) a summary of the mathematical theory used in the criteria.

2 Notation

We consider two aircraft, the ownship and the traffic aircraft, that are potentially in conflict in a 3-dimensional airspace. The conflict resolution algorithms

discussed here only use state-based information, e.g,. initial position and velocity and straight line trajectories, i.e., constant velocity vectors in a Euclidean

coordinate system.

We use the following notations:

5
so 3D vector Initial position of the ownship aircraft

vo 3D vector Initial velocity of the ownship aircraft

si 3D vector Initial position of the traffic aircraft

vi 3D vector Initial velocity of the traffic aircraft

The components of each vector are scalar values, so they are represented without the bold-face font, for example so = (sox, soy, soz). As a simplifying assumption, we regard the position and velocity vectors as accurate and without

error. Recent work shows how measurement errors in the state information

can be correctly handled by state-based conflict detection and resolution algorithms through the use of appropriate safety buffers [3]. Also, the assumption

that the resolutions are executed instantaneously can be mitigated through

the use of algorithms that filter infeasible solutions, e.g., algorithms that use

models of turn dynamics to determine whether there is sufficient time for a

turn to complete.

For notational convenience, all the dot products in this paper are twodimensional, kwk denotes the norm of the 2-dimensional projection of w, i.e.,

kwk =

p

w2

x + w2y

, and w2 denotes w

2

x + w

2

y

.

It is mathematically convenient to use a translated coordinate system. The

relative position s of the ownship with respect to the traffic aircraft is defined

to be s = so − si, and the relative velocity is denoted by v = vo − vi. Within

this translated coordinate system, the traffic aircraft is at the origin of the

coordinate system and does not move. The separation requirements in the

airspace systems are specified as a minimum horizontal separation D and a

minimum vertical separation H (typically, D is 5 nautical miles and H is

1000 feet). Horizontal and vertical perspectives of this coordinate system are

illustrated in Figure 2.

An aircraft trajectory is modeled as a particle with an initial position s,

a constant velocity vector v, and a time parameter t. As usually done in

state-based conflict detection and resolution, we ignore the effects of wind and

only use ground speed in the paper. The location of the aircraft at time t is

therefore s + tv. We will use prime notation to indicate a new velocity vector

that is computed by a conflict resolution algorithm, e.g., v

0

.

3 Criteria

Criteria represent the key safety requirements on the resulting velocity vectors

from an airspace separation algorithm. Formally, a criterion is a predicate on

the set of relative resolution maneuvers. These resolution maneuvers, denoted

v

0

, solve a safety issue related to separation. Two kinds of separation issues

are considered in this paper: (1) when the two aircraft are in conflict, i.e., a

predicted loss of separation, and (2) when the two aircraft are currently in loss

6
−H

s

s

v

v

D

H

Figure 2. Relative Horizontal and Vertical Perspectives

of separation. If an algorithm ensures that its vectors satisfy a given criterion,

then the algorithm correctly solves the separation issue, e.g., in the case of a

conflict, the impending conflict is avoided, or in the case of loss of separation,

separation is eventually recovered. The criteria are summarized in appendix B.

3.1 Horizontal Criterion for Conflict Resolution

The horizontal criterion for conflict resolution is defined as follows.

Definition 3.1 (horizontal criterion).

horizontal criterion(s, )(v

0

) ≡ s · v

0 ≥ R  det(s, v0

),

where R =

√

s

2−D2

D

and  is a unit value ±1, which we will call a direction

parameter. Any vector v

0

that satisfies this formula will resolve the conflict

if the traffic aircraft does not maneuver. If both aircraft maneuver, then

both aircraft must select resolutions using the same . This is illustrated in

Figure 3. The current ownship velocity vector is shown in blue and the current

traffic velocity vector is shown in magenta. If the conflict resolution systems

on both aircraft produce resolution vectors anywhere in their green regions,

the combined result will be implicitly coordinated. Similarly, if the conflict

resolution systems on both aircraft produce resolution vectors anywhere in

their blue regions, the combined result will be implicitly coordinated. If only

one aircraft maneuvers, then a vector in either the green or blue region will

7
Figure 3. Visualization of Horizontal Criterion for Conflict

suffice. The criterion can also be applied to ground speed solutions. This is

illustrated in Figure 4.

A few observations can be made about this criterion. First, it depends on

v

0

, where v

0 = v0

o − vi

, which only uses data that is available locally to an

aircraft. In particular, it does not depend upon v

0

i

, the resolution that will

be computed on the traffic aircraft. This is fundamental to achieving implicit

coordination, because otherwise an explicit exchange of these computed values

would be necessary. Also, although figures 3 and 4 illustrate situations where

only one of the ownship’s track angle or ground speed changes, the criterion is

more general. It applies to velocity vectors v

0 where both the ownship’s track

angle and ground speed change.

3.2 Horizontal Criterion for Loss of Separation

The horizontal criterion for loss of separation is defined as follows.

Definition 3.2 (horizontal los criterion).

horizontal los criterion(s, v, Th)(v

0

) ≡

s · v

0 ≥ s · v ∧

s · v

0 > exit dot min(s, Th),

where

exit dot min(s, Th) ≡

ksk

Th

(D − ksk).

8
Figure 4. Horizontal Criterion for Ground Speed

If the relative velocity v

0

satisfies these two equations, then the criterion is

met. Note that the second term implies that the new dot product is positive,

which is sufficient to ensure divergence. The second term also ensures that the

recovery from the loss of separation is achieved within time Th. The correctness

theorems then ensure that if either aircraft or both aircraft execute a resolution

that meets this criterion, then the combined result will be divergence. This is

illustrated in Figure 5. The horizontal criterion for loss of separation gives only

one region for each aircraft to choose from, namely the green region. In this

example the ownship has more options because of its greater ground speed. In

Figure 6, we illustrate the impact of the second conjunction of the criterion.

The purple region shows the reduced set of vectors that are needed to escape

the protection zone within a bounded time.

Once again it should be noted that the criterion only uses data that is

available locally on an aircraft. It does not depend upon v

0

i

the resolution

that will be computed on the traffic aircraft. Thus, an explicit exchange of

information is not necessary to achieve safe self-separation.

3.3 Vertical Criterion for Conflict Resolution

The vertical criterion is more complex than the horizontal criterion because

it is 3-dimensional. It is certainly possible to create a one-dimensional crite9
Figure 5. Horizontal Criterion For Loss of Separation Recovery

Figure 6. Impact of Second Conjunction of the Criterion

10
rion that is suitable for vertical-speed-only solutions. However, such a onedimensional criteria would leave out resolution maneuvers that solve conflicts

vertically using ground-speed or track solutions. These kinds of resolutions

are possible when the aircraft are already in a climb or descent. In the relative

coordinate frame, these solutions fall within a 3-dimensional region of space.

The basic idea is to define a half plane (Figure 7) such that any vector

that intersects this plane satisfies the criterion. We will present the formulas

p

v’

Figure 7. Vertical Criterion

that define this 3-dimensional criteron subsequently, but it is helpful to first

examine the criterion for the special cases where only the vertical speed is

changed. This special case is one-dimensional.

3.3.1 Vertical Criterion For Vertical Speed Only

There are three basic cases that must be considered:

• Both horizontal and vertical separation exist originally (see Figure 8).

• Only horizontal separation exists originally (see Figure 9).

• Only vertical separation exists originally (see Figure 10).

These regions are determined by the initial position s and one of the corners

of the protection zone. The horizontal position of a corner is specified using

the horizontal entrance/exit times:

• Θ−1 = horizontal entrance time.

• Θ+1 = horizontal exit time.

11
s

s

+H

−H −H

+H

x

Altitude

Figure 8. Vertical Criterion Vertical Speed Only Case 1

s

+H

−H

s

Altitude

x

Figure 9. Vertical Criterion Vertical Speed Only Case 2

+H

−H −H

+H

s

s

Figure 10. Vertical Criterion Vertical Speed Only Case 3

12
and the vertical position of a corner is specified with a flag  which indicates

top and bottom:

•  = -1 indicates the bottom of protection zone.

•  = +1 indicates the top of protection zone.

Note also that the direction dir, whether an entry (dir = −1) into the protection zone, or an exit (dir = +1) from the protection zone, can be calculated

as follows:

dir = IF |sz| ≥ H THEN  · sign(sz) ELSE − 1 ENDIF.

Note that the following two formulas

|sz| ≥ H AND dir =  · sign(sz)

and

|sz| < H AND dir = −1

define the allowed corner points. That is, the border of the criterion region is

defined by a line going through these points. The function sign returns −1 if

its argument is negative and +1 otherwise.

3.3.2 The General Vertical Criterion Formula

We will illustrate the concept with the case where there is horizontal separation

and sz > H, which is shown in Figure 11. The point p can be calculated as

p

s

p

Figure 11. Vertical Criterion Vertical Speed Only Case 3

follows:

p = (s + Θ+1v) WITH [z ← H],

which is (s+Θ+1v) with the z component replaced with H. We now construct

a line perpendicular to p (and hence tangent to the circle) as illustrated in

13
s

p

Figure 12. Construction of Tangent Plane

Figure 12. Next, we construct the half-plane that passes through this line and

is directly above pz as illustrated in Figure 7. The vertical criterion states that

if a velocity vector v

0

from s intersects this plane, then it is accepted. The

plane is completely determined by the point p and logic specifying which half

of the plane is to be used. The point p defines the vector that is the minimal

vertical speed only solution from s. More formally, we can define the vertical

criterion as follows.

Definition 3.3 (vertical criterion).

vertical criterion?(s, v, )(v

0

) =

(kvk = 0 AND  v

0

z ≥ 0 AND  sz ≥ H

OR

dir = IF |sz| ≥ H THEN  · sign(sz) ELSE − 1 ENDIF AND

∆(s, v) > 0 AND Θdir > 0 AND

p = (s + Θdirv) WITH [z :=  H] AND

intersects half plane?(s, v

0

, p, )).

The first term deals with the special case where the relative ground speed

between the aircraft is zero, i.e., they are flying parallel to each other. The

auxiliary function intersects_half_plane? is defined as follows:

intersects half plane?(s, v, p, ) =

v · p 6= 0 AND

t =

D2 − s · p

v · p

AND

t ≥ 0 AND

(sz + tvz) ≥  pz,

14
where the dot products are two-dimensional and ∆(s, v) = D2v

2 − (s⊥ · v)2

.

This vertical criterion not only includes the vertical-speed only solutions

shown in figures 8, 9, and 10, but also vertical resolutions that are achieved by

modifying horizontal parameters of the aircraft, i.e., ground speed and track

angle. This criterion is illustrated in Figure 13.

Figure 13. Vertical Criterion: Perspective View

3.4 Vertical Criterion for Loss of Separation Recovery

The vertical loss of separation criterion is only concerned with the vertical

component (sz or vz) of the position and velocity vectors. A more general 3-

dimensional version can be envisioned that would allow horizontal maneuvers

that achieve vertical separation when the ownship is currently climbing or

descending. Whether such a generalization is desirable operationally is not

obvious. This criterion has two components: one to ensure that the aircraft

diverge and one to provide a maximum time to recover vertically from the

loss of separation. The predicate vertical_los_criterion? captures this

criterion.

Definition 3.4 (vertical los criterion).

vertical los criterion?(s, v, Tv)(v

0

) =

|sz| < H AND

z criterion?(s, vz)(v

0

z

) AND

Tv ≥ ttez(sz, v0

z

).

15
The function ttez computes the time to exit vertically as follows:

ttez(sz, vz) =  sign(vz)H − sz

vz

,

for non-zero vz.

The predicate z_criterion? provides one way to guarantees that the two

aircraft will diverge.

z criterion?(s, vz)(v

0

z

) =

v

0

z 6= 0 AND

z prop?(sz, v0

z

) AND

(z prop?(sz, vz) =⇒

IF vz 6= 0 THEN

sign(vz) v

0

z ≥ 0

ELSE

break symmetry(s) (v

0

z

) > 0,

ENDIF).

where z_prop? is defined as

z_prop?(sz, vz) = szvz ≥ 0,

and sign returns −1 if its argument is negative and +1 otherwise.

The divergence criterion is conceptually simple even though the formal

specification is somewhat lengthy. The key idea is contained in z_prop?,

which sends an aircraft upward if it is higher and downward if it is lower than

the other aircraft. The break_symmetry function returns a unit value, i.e.,

±1, and is used in the situation where the original vertical speeds are equal

(i.e., vz = 0) to overcome the symmetry. It can be any function which satisfies

the following two properties:

s 6= 0 =⇒ break symmetry(−s) = −break symmetry(s),

sz 6= 0 =⇒ break symmetry(s) = sign(sz).

3.5 3-Dimensional Criteria

The 3-dimensional criteria that combine the horizontal and vertical criteria for

conflict and loss of separation are defined as follows.

16
Definition 3.5 (criterion 3D).

criterion 3D(s, v, h, v)(v

0

) ≡ (s

2 ≥ D2

AND

horizontal criterion(s, h)(v

0

)) OR

(vertical criterion(s, v, v)(v

0

) AND

(s

2 < D2

OR

horizontal criterion(s, h)(v

0 − v))).

Definition 3.6 (los criterion 3D).

los criterion 3D(s, v, T)(v

0

) ≡ horizontal los criterion(s, v, T)(v

0

) OR

vertical los criterion(s, v, T)(v

0

).

4 Correctness Theorems

The correctness theorems for the conflict case ensure that the resolutions result

in conflict free trajectories. The correctness theorems for the loss of separation

case establish two key properties:

• Divergence of the two aircraft.

• Timeliness of the recovery, that is separation will be achieved within a

specified amount of time.

The theorems in this section are presented without proof. For a presentation of the proofs, see [6].

4.1 Horizontal Correctness Theorems

4.1.1 Conflict Case

The horizontal distance between two aircraft at time t has a simple representation in the relative frame:

q

[(sox + voxt) − (six + vixt)]2 + [(soy + voyt) − (siy + viyt)]2

=

q

(sx + vxt)

2 + (sy + vyt)2

= ks + v tk.

where s and v are 2-dimensional relative vectors in the horizontal plane. A

conflict is a predicted loss of separation. Thus, horizontal_conflict can be

defined as a loss of separation in the horizontal plane:

17
Definition 4.1 (horizontal conflict).

horizontal_conflict?(s, v) ≡ ∃t : ks + v tk < D.

This predicate is true whenever the two aircraft are in conflict. In other

words there exists a future time t where a loss of separation will occur.

We can now present the key correctness theorems, when one aircraft maneuvers (independence) and when both aircraft maneuver (coordination).

Theorem 4.1 (horizontal criterion independence). If the aircraft are

horizontally separated at s, then

horizontal criterion(s, )(v) =⇒

NOT horizontal conflict?(s, v).

The theorem above establishes that the horizontal criterion (Definition 3.1)

is sufficient when only one of the aircraft maneuvers. The next theorem states

that the horizontal criterion is also adequate when both aircraft maneuver.

This is implicit in the fact that the argument to horizontal_conflict? is

v

0

o − v

0

i

, which contains both of the new velocity vectors for the ownship and

intruder aircraft.

Theorem 4.2 (horizontal criterion coordination). If the aircraft are

horizontally separated at s, then

horizontal conflict?(s, vo − vi) AND

horizontal criterion?(s, )(v

0

o − vi) AND

horizontal criterion?(−s, )(v

0

i − vo)

=⇒

NOT horizontal conflict?(s, v

0

o − v

0

i

).

The theorem also reveals that it is essential that the unit value  = ±1

must be the same for both aircraft in order for there to be coordination. Note

that the criterion for the traffic aircraft has arguments that are the negative

of the ownship. The position of the traffic aircraft relative to the ownship is

si − so, which equals −s and vi − vo, which equals −v.

4.1.2 Loss of Separation Case

For the loss of separation recovery theorems we need to introduce two additional predicates, horizontal_sep_after? and horizontal_divergent?,

which are defined as follows:

18
Definition 4.2 (horizontal sep after?).

horizontal sep after?(s, v, t) ≡

∀t

0

: t

0 ≥ t =⇒ (s + t v)2 ≥ D2

.

This predicate is true if and only if the aircraft are adequately separated for

all times greater than t.

Definition 4.3 (horizontal divergent?).

horizontal divergent?(s, v) ≡ ∀t : t > 0 =⇒ ksk < ks + tvk.

This predicate is true if the distance between the aircraft is strictly increasing

for all times greater than t.

The key horizontal loss of separation theorems are:

Theorem 4.3 (horizontal los criterion independence).

horizontal los criterion?(s, v, Th)(v

0

)

=⇒

horizontal divergent?(s, v

0

) AND

horizontal sep after?(s, v

0

, Th).

Thus, if only one aircraft maneuvers and its algorithm satisfies the criterion,

then the two aircraft will be in a divergent state, and within time Th, they will

no longer be in loss of separation. The next theorem covers the case where

both aircraft maneuver.

Theorem 4.4 (horizontal los criterion coordination).

horizontal los criterion?(s, vo − vi, T1)(v

0

o − vi) AND

horizontal los criterion?(−s, vi − vo, T2)(v

0

i − vo)

=⇒

horizontal divergent?(s, v

0

o − v

0

i

) AND

horizontal sep after?(s, v

0

o − v

0

i

, min(T1, T2)).

The theorem shows us that if both aircraft’s algorithms satisfy the criterion,

then the combined result will be implicitly coordinated. This is reflected in

the fact that both horizontal_divergent? and horizontal_sep_after? (in

the conclusion) have v

0

o − v

0

i

as their parameters (i.e., both of the aircraft’s

resolutions). Note that the time to exit from the protection zone is the minimum of the two local times T1 and T2. Thus, each local aircraft will meet its

local timeliness goal.

For examples of formally verified practical algorithms for recovery from

loss of separation, the reader is referred to [2].

19
4.2 Vertical Correctness Theorems

4.2.1 Conflict Case

The vertical correctness theorems in the conflict case are 3-dimensional. They

include the case when the velocity vector v

0 achieves vertical separation by

only modifying the vertical speed, but also the cases when vertical separation

is achieved by modifying the horizontal components of v

0

.

We introduce a predicate conflict?, which is true whenever there is a

future time where both vertical and horizontal separation is lost:

Definition 4.4 (conflict?).

conflict?(s, v) = ∃t : t ≥ 0 AND |sz + tvz| < H AND (s + tv)

2 < D2

.

The key correctness theorems are:

Theorem 4.5 (vertical criterion independence).

vertical criterion?(s, v, )(v

0

) =⇒

NOT conflict?(s, v

0

).

Theorem 4.6 (vertical criterion coordination).

conflict?(s, vo − vi) AND

vertical criterion?(s, vo − vi

, )(v

0

o − vi) AND

vertical criterion?(−s, vi − vo, −)(v

0

i − vo)

=⇒

NOT conflict?(s, v

0

o − v

0

i

).

The first theorem establishes correctness when only one aircraft maneuvers,

and the second theorem establishes correctness when both aircraft maneuver.

It is important to note that as long as the ownship uses the unit value  = ±1

and the intruder uses the opposite value −, coordination is guaranteed. We

also note that this is different from the horizontal theorems where it is required

the unit value  to be the same for the ownship and intruder aircraft.

4.2.2 Loss of Separation Case

As noted in Section 3.4, the vertical loss of separation criterion is one-dimensional.

Therefore, we introduce predicates that define divergence and timeliness with

respect to the vertical dimension alone. Vertical divergence is defined by

vertical_divergent:

20
Definition 4.5 (vertical divergent).

vertical divergent?(s, v) ≡

∀t : t > 0 =⇒ |sz| < |sz + t vz|.

Definition 4.6 (vertical sep after).

vertical sep after(s, v, t) ≡

|sz + t vz| > H.

These predicates appear in the correctness theorem to ensure that there is

divergence in the vertical dimension and that recovery will be achieved within

a maximum time, say Tv. The vertical loss of separation theorems provide

results for both the independent and the coordinated cases:

Theorem 4.7 (vertical los criterion independence).

vertical los criterion?(s, v, Tv)(v

0

)

=⇒

vertical divergent?(s, v

0

) AND

vertical sep after?(s, v

0

, Tv).

Theorem 4.8 (vertical los criterion coordination).

ksk 6= 0 AND

vertical los criterion?(s, vo − vi, Tv)(v

0

o − vi) AND

vertical los criterion?(−s, vi − vo, Tv)(v

0

i − vo)

=⇒

vertical divergent?(s, v

0

o − v

0

i

) AND

vertical sep after?(s, v

0

o − v

0

i

, Tv).

The first predicate rules out the situation where the two aircraft are exactly

over each other (i.e., their horizontal distance apart is 0).

4.3 3-D Correctness Theorems

The correctness theorems for the 3-dimensional conflict and loss of separation

criteria are stated as follows.

Theorem 4.9 (criterion 3D independence).

criterion 3D?(s, v, h, v)(v

0

) =⇒

NOT conflict?(s, v

0

).

21
Theorem 4.10 (criterion 3D coordination).

conflict?(s, vo − vi) AND

criterion 3D?(s, vo − vi

, h, v)(v

0

o − vi) AND

criterion 3D?(−s, vi − vo, h, −v)(v

0

i − vo)

=⇒

NOT conflict?(s, v

0

o − v

0

i

).

Theorem 4.11 (los criterion 3D independence).

los criterion 3D?(s, v, T)(v

0

)

=⇒

divergent?(s, v

0

) AND

separation after?(s, v

0

, T),

where

divergent?(s, v

0

) ≡ horizontal divergent?(s, v

0

) OR

vertical divergent?(s, v

0

),

separation after?(s, v

0

, t) ≡ horizontal sep after?(s, v

0

, t) OR

vertical sep after?(s, v

0

, t).

Theorem 4.12 (los criterion 3D coordination).

los criterion 3D?(s, vo − vi, T1)(v

0

o − vi) AND

los criterion?(−s, vi − vo, T2)(v

0

i − vo)

=⇒

divergent?(s, v

0

o − v

0

i

) AND

separation after?(s, v

0

o − v

0

i

, min(T1, T2)).

These theorems guarantee that all combinations of horizontal and vertical

manuevers are independently correct and that they are implicitly coordinated.

5 Choice of Direction Parameter, 

The criteria presented in Section 3 include a direction parameter , which is

a unit value ±1. This parameter captures the notion of whether the aircraft

should turn to the left or right in the horizontal dimension, or similarly up or

down in the vertical dimension. From the standpoint of the criteria, the choice

is arbitrary, and either choice is safe. Since either choice is safe, we can choose

an epsilon based on other factors, such as minimizing the size of the turn.

The key idea is that the choice of  is just as significant a policy decision

as the agreement on the criteria itself.

22
5.1 Horizontal Direction Parameter

There are many schemes that could be developed for choosing the horizontal unit value  used by both aircraft involved in a pairwise conflict, but it

is essential that if Horizontal_Direction is the function that chooses the

horizontal , the following property holds:

Horizontal Direction(s, v) = Horizontal Direction(−s, −v). (1)

This is sufficient to ensure that both aircraft will choose the same  for the

horizontal case.

One simple schema that satisfies Formula (1) is to mandate that  = 1, i.e.,

use the green solutions only. Alternatively, we could set  = −1 and only use

blue solutions. The use of a simple static method for choosing the horizontal

direction parameter, e.g.,  = −1, will inevitably leave out useful coordinated

solutions. This is illustrated in Figure 14. For this configuration of aircraft,

Figure 14. Static  = -1 Direction Problem

there are no blue ( = −1) ownship resolutions. Note that the traffic aircraft

has both green and blue resolutions. The brown region is where the green and

blue regions overlap. There are other configurations where there are no green

solutions.

We recommend the following method:

23
Definition 5.1 (Preferred Horizontal Direction Parameter).

 = sign(s

⊥ · v ≥ 0).

This non-static method will sometimes pick a green region and sometimes pick

a blue region, as illustrated in Figure 15. The top configuration in Figure 15

Figure 15. Our Recommended Direction Parameter

results in a green choice while the bottom configuration results in a blue choice.

Nevertheless, in all cases the combined result will be implicitly coordinated.

5.2 Vertical Direction

Any function Vertical_Direction that chooses a unit value  for the vertical

criterion must satisfy

Vertical Direction(s, v) = −Vertical Direction(−s, −v). (2)

24
This property guarantees that if the ownship chooses a unit value  = ±1, the

intruder aircraft will choose the opposite value −.

A simple schema that satisfies Formula (2) is to use  = 1 for the aircraft

that is higher,  = −1 for the lower aircraft, and to use a breaking symmetry

mechanism if the aircraft are at the same flight level. There are many possibilities for the symmetry breaking function and any can be used as long as the

following property holds:

s 6= 0 =⇒ break symmetry(s) = −break symmetry(−s).

For example, the following function satisfies the property above:

break symmetry(s) ≡ IF sz > 0 OR

(sz = 0 AND sx > 0) OR

(sz = 0 AND sx = 0 AND sy > 0)

THEN 1

ELSE − 1

ENDIF.

The simple schema is not ideal when the aircraft is currently climbing or

descending. Consider the following diagram (Figure 16), where the aircraft

is currently descending and is only slightly higher than the other aircraft. In

+H

−H

Figure 16. Vertical Criterion: Perspective View

this case it is better to increase the speed of the descent rather than abruptly

change directions and climb upward. Thus, we prefer the following method to

select the vertical unit value :

Definition 5.2 (Preferred Vertical Direction Parameter).

 = IF sz + Θ−1 vz > 0 THEN 1

ELSEIF sz + Θ−1 vz < 0 THEN − 1

ELSE break symmetry(s)

ENDIF.

This policy checks the z-component at the time of horizontal entry into the

protection zone.

25
6 International Standard for State-Based Coordination

Under the assumption that distributed self-separation is deemed to have sufficient benefit to the airspace community, an international standard would

have to be created and adopted that defines the specifics of the criteria and

their application. An important part of the work of this committee will be

to develop the requirements that the separation algorithms must meet. These

requirements must be evaluated for their safety properties in the manner of a

detailed analysis, similar to what was presented in Section 4. The advantage

of the criteria standard, which is advocated in this paper, is that it allows

efficient investigation of these requirements on algorithms. The efficiency is

a result of part of the safety analysis that is done once for all algorithms. If

a single algorithm is mandated by the standard then, undoubtedly, multiple

algorithm candidates will be evaluated first, so the efficiency of the criteria

standard is an important enabling technology. On the other hand, if multiple

algorithms are allowed, then the safety requirements are precisely the criteria,

along with the associated choice of  (see Section 5).

Understanding the criteria and proofs of correctness requires a certain level

of mathematical sophistication. We have attempted to aid the mathematical

analysis through the development of a mathematical framework for analyzing

criteria and algorithms. We call this framework the Airborne Coordinated

Conflict Resolution and Detection (ACCoRD) framework [9]. This framework

has been developed with generality in mind. We want to support a wide

class of algorithms and criteria. Achieving implicit coordination for both the

independent and coordinated cases is non-trivial, and our criteria are by no

means unique. Other criteria could be created, but eventually the world community must decide on a set of criteria that will be adopted. Conceivably,

the ACCoRD framework may be used for other criteria as well. We believe

that our criteria are very general and powerful, but future refinements and

improvements are possible. We have at least shown mathematically that such

an approach is viable.

All types of analysis rely on certain assumptions, and ACCoRD is no exception. Several idealistic assumptions were made in these proofs: (1) input

data contains no errors, (2) the computations were performed with infinite

precision, i.e., mathematical real numbers, (3) the resolution maneuvers can

be performed instantaneously, and (4) at least one aircraft must implement the

prescribed maneuver in a timely manner and the other aircraft must either not

change its velocity vector or do so in accordance with the critieria, and (6) only

two aircraft are involved in a conflict at the same time. An on-going research

effort is underway to enhance ACCoRD by relaxing all of these assumptions.

One great advantage of the formal mathematical approach is that the proofs

26
of correctness can not only be checked by domain experts, but they can also

be checked by specialized software called theorem provers. The mathematical

proofs in ACCoRD were verified using the PVS theorem prover [7].

7 Implications for Strategic Algorithms

The safety argument for a distributed implementation of self separation is typically built around the idea that there are layers of recovery. Typical layers

include (1) strategic conflict resolution, (2) state-based tactical conflict resolution, and finally (3) collision avoidance [1,10]. The strategic conflict resolution

system is designed to provide highly efficient solutions but, due to its complexity, it may fail to produce a timely solution. In this case, the system is designed

with a backup conflict detection and resolution algorithm that is state-based.

If this backup fails to resolve the conflict, then there is a collision avoidance

mechanism such as TCAS II to prevent catastrophe. Each system layer contributes to the safety of the system. The strategic layer solves many conflicts

and thus the tactical system is invoked infrequently. The tactical layer solves

the majority of the remaining conflicts and thus the collision avoidance system

is very infrequently invoked. The safety of the system fundamentally depends

upon certain correctness properties of these layers, but especially upon the

state-based backups. This is precisely where the criteria provide the needed

guarantees. The tactical conflict resolution algorithms need only satisfy the

conflict criteria to inherit the needed properties. The collision avoidance algorithms need only satisfy the loss of separation criteria.

Strategic algorithms incorporate both the current position and velocity

of the aircraft, but also include expected turns, accelerations, decelerations,

climbs, and descents. In strategic conflict detection resolution algorithms,

coordination is sometimes achieved using different pilot alerting times for the

two aircraft. Using this approach, only one aircraft maneuvers at a time. The

aircraft with the larger lookahead time is often referred to as the burdened

aircraft. It is essential that the mechanism for choosing the burdened aircraft

be unambiguous and well-defined for all possible configurations of aircraft.

We can envision an approach that blends this idea with the criteria approach

presented in this paper. While the time to loss of separation is large, only

the burdened aircraft maneuvers. However, if the time to loss of separation is

small, both aircraft are allowed to maneuver in accordance with the criteria.

We would also recommend that the strategic algorithms choose a maneuver

(for the burdened aircraft) that is consistent with the criteria. In this way a

seamless transition to the state-based algorithms would be achieved. In this

blended concept, the criteria serve as a filter on the allowed solutions from the

strategic algorithms. In fact, any resolution algorithm can be made consistent

with the criteria by using the criteria to filter resolutions.

27
There is another advantage to using the criteria to filter strategic resolution

algorithm solutions: it provides fault tolerance. Suppose that there is some

failure in the selection of the burdened aircraft due to data errors or some

system failure. If both aircraft erroneously conclude that they are the burdened

aircraft, the use of criteria will ensure that the combined result is coordinated.

8 Conclusions

The goal of this work was to develop a mechanism that would allow for the

efficient safety analysis of many different separation algorithms. As a consequence of this research, we discovered a way to ensure that aircraft using

different conflict resolution algorithms will still have a strong guarantee of

aircraft separation. We have shown that a correct algorithm will perform a

safe maneuver when both aircraft maneuver at the same time or when only

one aircraft executes a maneuver. The mechanism proposed in this paper is

the use of an intermediate layer called the criteria layer. For each criterion,

the basic idea is to decompose the safety argument into two steps: first, the

criterion implies correctness, and second an algorithm satisfies the criterion.

The first step establishes that the criterion is sufficient to meet the correctness

properties. This verification step has already been accomplished within the

ACCoRD framework [9]. We note that if alternate formulas are adopted, the

verification would need to be redone. However, some mathematical tools have

been developed that could simplify this new verification [6]. The second step

shows that a particular algorithm meets the criterion. This must be accomplished for each new algorithm that is developed. We believe that this step is

relatively easier than the first step.

For multiple algorithms to be used safely within the distributed concept for

self-separation, the international standard must agree on both specific formulas for criteria and a particular method for choosing the direction parameters

() that appear in the criteria. Some may argue that the proposed criteria

are too complex for an international standard to address. We counter that

argument with the observation that the criteria here are far simpler than the

specification of Traffic Collision Avoidance System (TCAS), whose state machine representation is over 700 pages long [8]. Furthermore, the estimated

cost of the TCAS II development over a period of fifteen years was $400 million in 2001 dollars. This estimate includes tests, analyses, and computer

simulations [5]. The criteria formulas presented in this paper are complex and

a certain level of mathematical sophistication is required to understand them.

However, separation systems are complex and safety critical by their nature.

We conclude that it will be easier to mandate a set of criteria than attempt

to gain international agreement for the development of a single algorithm.

We have sought to make the criteria as general as possible, though we

28
expect that improvements will continue to be made. An air transportation

system built around a criteria standard will be far more general and flexible

than a concept where a particular algorithm is mandated. Specifically, the

criteria standard supports the natural evolution of the air transportation system as better technologies are introduced that enable better algorithms. In

an approach where a single algorithm is mandated, changes in technologies

require new international committees. However, in the criteria approach, it is

only necessary to show that the new algorithm satisfies the criteria. It then

inherits the system-wide global guarantees of coordinated resolutions.

Additionally, the criteria may be used in other contexts. For instance, the

criteria can be displayed on the ground control station so that the controllers

have an indication of what the algorithms will do. In fact, this criterion

approach is not limited to only distributed separation assurance protocols.

It could be applied to ground-based concepts. In this way, as long as the

controllers choose resolutions within the criteria, hand-offs between sectors, or

even between nations, would be coordinated.

References

1. M.G. Ballin, V. Sharma, R.A. Vivona, E.J. Johnson, and E. Ramiscal. A

flight deck decision support tool for autonomous airborne operations. In

Proceedings of the AIAA Guidance, Navigation and Control Conference,

Monterey, CA, USA, AIAA. Citeseer, 2002.

2. Ricky W. Butler and C ́esar A. Mu ̃noz. Formally verified practical algorithms for recovery from loss of separation. Technical Report NASA TM2009-215726, NASA Langley Research Center, NASA LaRC,Hampton VA

23681-2199, USA, Jun 2009.

3. Heber Herencia-Zapana, Jean-Baptiste Jeannin, and C ́esar Mu ̃noz. Formal

verification of safety buffers for state-based conflict detection and resolution. In Proceedings of 27th International Congress of the Aeronautical

Sciences, ICAS 2010, Nice, France, 2010.

4. James Kuchar and Lee Yang. A review of conflict detection and resolution modeling methods. IEEE Transactions on Intelligent Transportation

Systems, 1(4):179–189, 2000.

5. MTSI. Airspace modeling for UAS sense and avoid, 2007. http://www.uvsinfo.com/Yearbook2007/147 MTSI Sense-&-Avoid.pdf (accessed Oct.

2000).

29
6. Anthony Narkawicz and C ́esar A. Mu ̃noz. State-based implicit coordination and applications. NASA TP, NASA Langley Research Center,

October 2010. Submitted.

7. Sam Owre, John Rushby, and Natarajan Shankar. PVS: A prototype

verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in

Artificial Intelligence, pages 748–752, Saratoga, NY, June 1992. Springer

Verlag.

8. RTCA. Minimum operational performance standards for traffic alert and

collision avoidance system II (TCAS II), 1997. DO-185A.

9. NASA Langley Formal Methods Team. Airborne coordinated conflict resolution and detection (ACCoRD), 2010.

http://shemesh.larc.nasa.gov/people/cam/ACCoRD/.

10. David J. Wing, Robert A. Vivona, and David A. Roscoe. Airborne tactical

intent-based conflict resolution capability. In 9th AIAA Aviation Technology, Integration, and Operations Conference (ATIO), Hilton Head, South

Carolina, USA, September 2009.

30
Appendix A

Summary of Notation

break_symmetry function used to break vertical symmetry

conflict?(s, v) true if aircraft are in conflict horizontally and vertically

criterion_3D the 3-dimensional criterion for conflict resolution

D diameter of protection zone around an aircraft

∆(s, v) discriminant of quadratic equation from ks+tvk

2 =

D2

det(s, v) sxvy − syvx

horizontal_divergent?(s, v) true if horizontal distance between two aircraft is

increasing

 ±1, the direction parameter

exit_dot_min(s, t)

|s|

t

(D − |s|)

H height of protection zone around an aircraft

horizontal_criterion the criterion for horizontal conflict resolution

horizontal_los_criterion the criterion for horizontal loss of separation recovery

horizontal_conflict?(s, v) true if aircraft are in conflict horizontally

horizontal_sep_after?(s, v, t) true if aircraft will be horizontally separated after

time t

los_criterion-3D the 3-dimensional criterion for loss of separation recovery

Θ−1 horizontal entrance time into protection zone

Θ+1 horizontal exit time from protection zone

sign(x) IF x ≥ 0 THEN 1 ELSE − 1 ENDIF

so initial position of the ownship aircraft

siinitial position of the traffic aircraft

vertical_criterion? the criterion for vertical conflict resolution

vertical_los_criterion? the criterion for vertical loss of separation recovery

vertical_sep_after(s, v

0

o

, v

0

i

, t) true iff there is vertical separation after t

vertical_divergent?(s, v) true if vertical distance between two aircraft is increasing

kwk two-dimensional norm of vector w

z_prop?(s, v) szvz ≥ 0

31
Appendix B

Summary of Criteria

The following table provides a quick reference summary of the criteria

presented in this paper.

Conflict Resolution Loss of Separation Recovery

horiz. s · v

0 ≥ R  det(s, v0

)

s · v

0 ≥ s · v ∧

s · v

0 > exit_dot_min(s,T)

vert.

∆(s, v) > 0 ∧ Θdir > 0 ∧

p = (s + Θdirv) WITH [z ←  H] ∧

intersects_half_plane?(s, v

0

, p, )

|sz| < H ∧

z_criterion?(s, vz)(v

0

z

) ∧

Tv ≥ ttez(sz, v0

z

)

3D

(s

2 ≥ D2 ∧

horizontal_criterion(s, h)(v

0

)) ∨

(vertical_criterion(s, v, v)(v

0

) ∧

(s

2 < D2 ∨

horizontal_criterion(s, h)(v

0 +

v)))

horizontal_los_criterion(s, v, T)(v

0

) ∨

vertical_los_criterion(s, v, T)(v

0

)

32

REPORT DOCUMENTATION PAGE Form Approved

OMB No. 0704–0188

The public reporting burden for this collection of information is estimated to average 1 hour per response, including the time for reviewing instructions, searching existing data sources,

gathering and maintaining the data needed, and completing and reviewing the collection of information. Send comments regarding this burden estimate or any other aspect of this collection

of information, including suggestions for reducing this burden, to Department of Defense, Washington Headquarters Services, Directorate for Information Operations and Reports

(0704-0188), 1215 Jefferson Davis Highway, Suite 1204, Arlington, VA 22202-4302. Respondents should be aware that notwithstanding any other provision of law, no person shall be

subject to any penalty for failing to comply with a collection of information if it does not display a currently valid OMB control number.

PLEASE DO NOT RETURN YOUR FORM TO THE ABOVE ADDRESS.

Standard Form 298 (Rev. 8/98)

Prescribed by ANSI Std. Z39.18

1. REPORT DATE (DD-MM-YYYY)

01-10-2010

2. REPORT TYPE

Technical Memorandum

3. DATES COVERED (From - To)

4. TITLE AND SUBTITLE

A Criteria Standard for Conflict Resolution: A Vision for

Guaranteeing the Safety of Self-Separation in NextGen

5a. CONTRACT NUMBER

5b. GRANT NUMBER

5c. PROGRAM ELEMENT NUMBER

5d. PROJECT NUMBER

5e. TASK NUMBER

5f. WORK UNIT NUMBER

411931-02-51-07-01

6. AUTHOR(S)

C ́esar Mu ̃noz, Ricky W. Butler, Anthony Narkawicz, Jeffrey M.

Maddalon, and George Hagen

7. PERFORMING ORGANIZATION NAME(S) AND ADDRESS(ES)

NASA Langley Research Center

Hampton, Virginia 23681-2199

8. PERFORMING ORGANIZATION

REPORT NUMBER

L–19932

9. SPONSORING/MONITORING AGENCY NAME(S) AND ADDRESS(ES)

National Aeronautics and Space Administration

Washington, DC 20546-0001

10. SPONSOR/MONITOR’S ACRONYM(S)

NASA

11. SPONSOR/MONITOR’S REPORT

NUMBER(S)

NASA/TM–2010–216862

12. DISTRIBUTION/AVAILABILITY STATEMENT

Unclassified-Unlimited

Subject Category 03

Availability: NASA CASI (443) 757-5802

13. SUPPLEMENTARY NOTES

An electronic version can be found at http://ntrs.nasa.gov.

14. ABSTRACT

Distributed approaches for conflict resolution rely on analyzing the behavior of each aircraft to ensure that system-wide safety properties are

maintained. This paper presents the criteria method, which increases the quality and efficiency of a safety assurance analysis for distributed air

traffic concepts. The criteria standard is shown to provide two key safety properties: safe separation when only one aircraft maneuvers and safe

separation when both aircraft maneuver at the same time. This approach is complemented with strong guarantees of correct operation through

formal verification. To show that an algorithm is correct, i.e., that it always meets its specified safety property, one must only show that the

algorithm satisfies the criteria. Once this is done, then the algorithm inherits the safety properties of the criteria. An important consequence of

this approach is that there is no requirement that both aircraft execute the same conflict resolution algorithm. Therefore, the criteria approach

allows different avionics manufacturers or even different airlines to use different algorithms, each optimized according to their own proprietary

concerns.

15. SUBJECT TERMS

air traffic, conflict, detection, resolution, avoidance, formal methods, formal verification, criteria, algorithm, safety

16. SECURITY CLASSIFICATION OF:

a. REPORT

U

b. ABSTRACT

U

c. THIS PAGE

U

17. LIMITATION OF

ABSTRACT

UU

18. NUMBER

OF

PAGES

40

19a. NAME OF RESPONSIBLE PERSON

STI Help Desk (email: help@sti.nasa.gov)

19b. TELEPHONE NUMBER (Include area code)

(443) 757-5802