A TCAS-II Resolution Advisory Detection Algorithm∗

César Muñoz† Anthony Narkawicz

James Chamberlain
NASA, Langley Research Center, Hampton, VA, 23681, USA

The Traffic Alert and Collision Avoidance System (TCAS) is a family of airborne systems
designed to reduce the risk of mid-air collisions between aircraft. TCAS II, the current
generation of TCAS devices, provides resolution advisories that direct pilots to maintain
or increase vertical separation when aircraft distance and time parameters are beyond
designed system thresholds. This paper presents a mathematical model of the TCAS II
Resolution Advisory (RA) logic that assumes accurate aircraft state information. Based on
this model, an algorithm for RA detection is also presented. This algorithm is analogous
to a conflict detection algorithm, but instead of predicting loss of separation, it predicts
resolution advisories. It has been formally verified that for a kinematic model of aircraft
trajectories, this algorithm completely and correctly characterizes all encounter geometries
between two aircraft that lead to a resolution advisory within a given lookahead time
interval. The RA detection algorithm proposed in this paper is a fundamental component
of a NASA sense and avoid concept for the integration of Unmanned Aircraft Systems in
civil airspace.

Nomenclature
so Current horizontal component of ownship’s position
soz Current ownship’s altitude
vo Current horizontal component of ownship’s velocity
voz Current ownship’s vertical speed
si Current horizontal component of intruder’s position
siz Current intruder’s altitude
vi Current horizontal component of intruder’s velocity
viz Current intruder’s vertical speed
tcpa Time to closest horizontal point of approach
tcoa Time to co-altitude
τ Current ownship’s tau
τmod ` Current ownship’s modified tau for sensitivity level `
TAU` RA tau threshold for sensitivity level `
DMOD` RA DMOD for sensitivity level `
ZTHR` RA vertical threshold for sensitivity level `
HMD` RA Horizontal Miss Distance for sensitivity level `
ALIM` RA altitude limit for sensitivity level `
Subscript
o Ownship information
i Intruder information
` Current ownship’s sensitivity level
x Northern component of a position or velocity vector
y Eastern component of a position or velocity vector
∗ Note: Formulas (16), (23), (26), and (31) have typographical errors in the published version of this paper. Those errors

have been corrected in this document.

† Research Computer Scientist, AIAA Member.

1 of 12

American Institute of Aeronautics and Astronautics

 I. Introduction
The Unmanned Aircraft Systems (UAS) Integration in the National Airspace System (NAS) is a NASA
research project that addresses the integration of civil UAS into non-segregated airspace operations. One of
the major challenges of this integration is the lack of an on-board pilot to comply with the legal requirement
identified in the US Code of Federal Regulations (CFR) that pilots see and avoid other aircraft in their
vicinity. As a means of compliance with this legal requirement, the final report of the FAA-sponsored Sense
and Avoid (SAA) Workshop1 defines the concept of sense and avoid for remote pilots as “the capability of
a UAS to remain well clear from and avoid collisions with other airborne traffic.” Hence, collision avoidance
is a critical element of any sense and avoid concept for the integration of UAS in the NAS.
The Traffic Alert and Collision Avoidance System (TCAS) is a family of airborne devices that are designed
to reduce the risk of mid-air collisions between aircraft equipped with operating transponders.2 TCAS has
evolved through extensive development and a number of versions since its initial operational evaluation in
1982. TCAS II, the current generation of TCAS devices, is mandated in the US for aircraft with greater than
30 seats or a maximum takeoff weight greater than 33,000 pounds. Although it is not required, TCAS II is
also installed on many turbine-powered general aviation aircraft. Version 7.0 is the current operationally-
mandated version of TCAS II, and Version 7.1 has been standardized.3
In contrast to TCAS I, the first generation of TCAS devices, TCAS II provides resolution advisories
(RAs). RAs are visual and vocalized alerts that direct pilots to maintain or increase vertical separation
with intruders that are considered collision threats. TCAS II resolution advisories can be corrective or
preventive depending on whether the pilot is expected to change or maintain the aircraft’s current vertical
speed. Corrective RAs are particularly disruptive to the air traffic system since they may cause drastic
evasive maneuvers. For this reason, they are intended as a last resort maneuver when all other means of
separation have failed.
The Sense and Avoid (SAA) concept for Unmanned Aircraft Systems (UAS) described in4 rests on
interoperability principles that take into account both the Air Traffic Control (ATC) environment as well
as existing systems such as TCAS. Specifically, the concept addresses the determination of well clear values
that are large enough to avoid issuance of TCAS II resolution advisories. It relies on airborne and ground
capabilities that predict encounter geometries that will cause an RA. These capabilities allow UAS pilots
to take non-disruptive preventive actions early enough to avoid issuance of corrective RAs. The main
contribution of this paper is an algorithm for TCAS II RA detection that can be used to implement those
SSA airborne and ground capabilities.
The RA detection algorithm presented in this paper is based on a mathematical model of the TCAS II
resolution advisory logic that assumes accurate vector state information for two aircraft. It is analogous
to a conflict detection algorithm but instead of predicting loss of separation, it predicts RAs. It has been
formally verified in the Program Verification System (PVS)5 that assuming aircraft linear trajectories, the
algorithm completely and correctly characterizes all encounter geometries that will cause an RA within
a given lookahead time interval. The formal development presented in this paper is part of the NASA’s
Airborne Coordinated Resolution and Detection (ACCoRD) mathematical framework, which is electronically
available from http://shemesh.larc.nasa.gov/people/cam/ACCoRD.
The rest of this paper is organized as follows. Section II provides a high level description of the TCAS II
resolution advisory logic. A mathematical model of this logic is presented in Section III. Section IV proposes
an algorithm for resolution advisory detection and states its main correctness property. Section V presents
an algorithm that checks whether a given RA is corrective or preventive. Section VI discusses related work.
The last section concludes the paper.

II. TCAS II Resolution Advisory Logic

TCAS consists of several hardware and software sub-systems. These sub-systems provides means for lim-
ited surveillance and communication, and perform tasks such as traffic identification, tracking, and collision
avoidance. This paper focuses on the collision detection sub-system that deals with resolution advisories.
TCAS collision detection logic uses the concept of tau (τ ) to estimate the time to closest point of approach
(CPA) between the ownship and one given traffic aircraft known as intruder. The time tau is defined as

2 of 12

American Institute of Aeronautics and Astronautics

range (r) over closure rate, where closure rate is the negative of the range rate (ṙ), i.e.,
r
τ ≡− , (1)
ṙ
Both range and range rate are derived from TCAS interrogations of the intruder’s transponder, nominally
at one-second intervals. The time tau and the actual time to CPA coincide only when the aircraft are on a
perfect collision course and not accelerating. If the aircraft will merely pass near each other, then tau is only
an approximation of time to CPA. In this case, tau will decrease to a minimum value shortly before actual
CPA and then sharply increase until CPA, at which time the value of tau is undefined.
In the vertical dimension, time to co-altitude and vertical separation are used instead of tau and range.
Time to co-altitude is sometimes called vertical tau and is computed as vertical separation divided by vertical
closure rate. In the general case, a resolution advisory is issued when range and vertical separation are below
horizontal and vertical distance thresholds called DMOD and ZTHR, respectively, and tau and time to co-
altitude are below a time threshold called TAU. Since the ratio of range and range rate tends to be lower
at closer distances, the minimum value that tau will attain in the near future is a time that varies directly
with the nearness of the encounter. This property of tau means that the selection of a time threshold value,
i.e., TAU, at which to alert for a collision threat determines not only the time to react to the threat, but
also the size of protected airspace within which a given threat encounter will cause an alert.
An effective TCAS logic requires a tradeoff between necessary protection and unnecessary advisories.
This tradeoff is partly managed by controlling the sensitivity level (SL), which varies with the altitude of the
ownship. Higher SLs are selected for higher altitudes, where generally speeds are higher and separations are
larger. Among other things the SL controls the tau thresholds for RA issuance, and therefore the dimensions
of protected airspace around each TCAS-equipped aircraft.
Two problems may arise with use of the simple definition of tau given by Formula (1). The first problem
involves threat encounters with low range closure rates, and the second problem involves high closure rates
with large miss distances. TCAS II addresses the low-closure rate problem by using a modified definition of
tau:3
r2 − DMOD2
τmod ≡ − . (2)
rṙ
DMOD was designed to provide approximately an RA-threshold amount of reaction time for an intruder
that accelerated toward the ownship at a sustained 1/3 g.6 Modified tau values are nearly identical to the
true value of tau at large ranges and range rates but are smaller, i.e., more conservative, for smaller ranges
and rates. Formula (2) assumes that the closure rate is not zero and that the current range is greater or
equal than DMOD.
TCAS Versions 7.0 and higher address the high-closure-rate, nuisance-RA problem by employing a hori-
zontal miss distance (HMD) filter.7 The HMD filter employs a parabolic range tracker to provide projected
range acceleration as well as projected range and range rate, and uses the range acceleration to detect hor-
izontal miss distances that are sufficiently large so as not to be a collision threat (range acceleration will
be zero for non-accelerating aircraft on a collision course, but will be positive if the encounter has a miss
distance). The HMD filter employs numerous noise filters and maneuver checks whose explanations are
beyond the scope of this paper, but the end result is that the filter will suppress RA issuances for horizontal
miss distances at CPA that are approximately equal to or greater than the DMOD values.
Table 1. TCAS Sensitivity Level Definition and Alarm Thresholds for RAs

Ownship Altitude SL TAU DMOD ZTHR ALIM HMD

(feet) (sec) (nmi) (feet) (feet) (feet)
1000 - 2350 3 15 0.20 600 300 1215
2350 - 5000 4 20 0.35 600 300 2126
5000 -10000 5 25 0.55 600 350 3342
10000 - 20000 6 30 0.80 600 400 4861
20000 - 42000 7 35 1.10 700 600 6683
> 42000 7 35 1.10 800 700 6683

3 of 12

American Institute of Aeronautics and Astronautics

 Table 1 shows the altitude bands for each SL and the associated thresholds for RA issuance.2, 3 Although
expressed in different units, the values of HMD and DMOD are the same fo every sensitivity level. The
distance threshold value ALIM is used to determine if a particular RA is corrective or preventive. For
example, when a TCAS-equipped aircraft is between 20000 and 42000 feet (SL 7), the tau threshold for RA
issuance is 35 seconds, and generally an RA will be issued if both horizontal and vertical tau fall below this
value. An RA will also be issued for low vertical rate encounters if the current altitude difference is less than
the vertical threshold (ZTHR) value of 700 feet. Once TCAS determines that an RA is required, it must
determine the type of RA needed. In order to do this, TCAS estimates the altitude difference at CPA for
various RA types; if the altitude difference will be less than the altitude limit (ALIM) value (600 feet in this
example), then the RA will be corrective (e.g., “Climb” if level), requiring a trajectory change to regain at
least ALIM feet of vertical separation; otherwise the RA will be preventive (e.g., “Dont Descend” if level),
requiring no trajectory change.
The next section presents a mathematical model of the TCAS II RA logic that formalizes the description
provided above.

III. Vectorized Model of the TCAS II Resolution Advisory Logic

While TCAS II uses different mechanisms to track aircraft as accurately as possible, the mathematical
model presented in this section assumes that accurate aircraft surveillance information is available as hor-
izontal and vertical components in a 3-dimensional airspace. Through out this paper, letters in bold-face
denote 2-D vectors. Vector operations such as addition, subtraction,
√ scalar multiplication, dot product, i.e.,
s · v ≡ sx vx + sy vy , and the norm of a vector, i.e., ksk ≡ s · s, are defined in a 2-D Euclidean geometry.
The expression v⊥ denotes the 2-D right perpendicular of v, i.e., (vy , −vx ). Furthermore, the function root,
defined by Formula (3), computes the roots of the quadratic equation ax2 + bx + c = 0. For completeness, it
is defined such that it returns the value 0 when the roots are undefined. In this paper, the values returned
by root are only used in a context where a 6= 0 and b2 − 4ac ≥ 0.
√

 −b+ b2 −4ac if a 6= 0 and b2 − 4ac ≥ 0,
root(a, b, c, ) ≡ 2a (3)
0 otherwise.

Assuming constant velocities, the horizontal positions of the ownship and intruder aircraft at a time
t ≥ 0, are given by
so (t) ≡ so + tvo , (4)
si (t) ≡ si + tvi , (5)
respectively. As it simplifies the mathematical development, some definitions in this paper use a relative
coordinate system where the intruder is static at the center of the system. In this relative system, the ownship
is located at s = so −si and moves at relative velocity v = vo −vi . Therefore, the relative horizontal position
of the ownship with respect to the traffic aircraft at any time t can be defined as follows.
s(t) ≡ s + tv. (6)
The range between the aircraft at any time t is given bya
p
r(t) ≡ ks(t)k = ksk2 + 2ts · v + t2 kvk2 . (7)
Closure rate is the derivative of r(t) with respect to t, i.e.,
s · v + tkvk2
ṙ(t) ≡ . (8)
ks(t)k
Given a relative position s and velocity v, the time of horizontal closest point of approach, denoted tcpa , is
the time t that satisfies ṙ(t) = 0. Hence,
s·v
tcpa (s, v) ≡ − . (9)
kvk2
a Inthis paper, we assume that a 2-dimensional range is used in the calculation of τ and τmod . This assumption is consistent
with the use of these values in horizontal threshold checks done by the TCAS II resolution advisory logic.

4 of 12

American Institute of Aeronautics and Astronautics

By convention, tcpa is defined as 0 when the velocities of the ownship and intruder aircraft are identical, i.e.,
tcpa (s, v) = 0, if kvk2 = 0.
Given a relative position s and velocity v, Formula (1) and Formula (2) can be written in a vector form
as follows.
r r(0) ksk ksk2
τ (s, v) ≡ − = − = − s·v = − , (10)
ṙ ˙
r(0) ksk s · v
DMOD2` − ksk2
τmod ` (s, v) ≡ . (11)
s · v
Formula (1) and Formula (2) are undefined when the closure rate is 0. This happens when both aircraft
have the same velocity vector, i.e., same direction and same speed, and it also happens when at current time
the aircraft are at the closest point of approach. In the vector form of these formulas, i.e., Formula (10) and
Formula (11), the singularity is equivalently expressed as s · v = 0. The dot product s · v also characterizes
whether the aircraft are horizontally diverging, i.e., s · v > 0, or horizontally converging, i.e., s · v < 0. It can
be seen from Formula (10) that when the aircraft are converging, τ is positive. In the TCAS II RA logic,
Formula (11) is used in a context where the aircraft are horizontally converging. In that case, modified tau,
i.e., τmod ` , is positive when the current range is greater than DMOD` .
As explained in Section II, the TCAS II RA logic checks the value of τmod against horizontal and vertical
thresholds to determine if a resolution advisory will be issued. These checks can be mathematically modeled
using the functions Horizontal RA` and Vertical RA` below.
The function Horizontal RA` takes as parameters the relative horizontal position s and velocity v of the
aircraft. It returns true if, for the given input and sensitivity level `, the horizontal thresholds are satisfied.

Horizontal RA` (s, v) ≡ ksk ≤ DMOD` or (s · v < 0 and τmod ` (s, v) ≤ TAU` ). (12)

In order to model the vertical check performed by the TCAS II RA logic, it is necessary to define the
time to co-altitude tcoa . This time satisfies sz + tcoa vz = 0, where sz ≡ soz − siz and vz ≡ voz − viz . Therefore,
for a given vertical separation sz and relative non-zero vertical speed vz ,
sz
tcoa (sz , vz ) ≡ − . (13)
vz
Similar to the horizontal case, the product sz vz characterizes whether the aircraft are vertically diverging,
i.e., sz vz > 0, or vertically converging, i.e., ss vz < 0. In the TCAS II RA logic, Formula (13) is used
in a context where the aircraft are vertically converging. In this case, tcoa is always positive. The function
Vertical RA` , which returns true when the vertical thresholds are satisfied for a sensitivity level `, is defined
as follows.
Vertical RA` (sz , vz ) ≡ |sz | ≤ ZTHR` or (sz vz < 0 and tcoa (sz , vz ) ≤ TAU` ). (14)
where sz and vz are, respectively, the vertical separation and the relative vertical velocity of the aircraft.
In addition to the horizontal and vertical checks, TCAS Version 7.0 introduces a filter that inhibits
resolution advisories when the projected point of closest approach is larger than a given horizontal miss
distance. In the formal model presented in this paper, this functionality is accomplished by a state-based
2-D conflict detection algorithm called CD2D∞ .
The function CD2D∞ takes as parameters the relative state of the aircraft, i.e., relative position s and
relative velocity v, a minimum separation distance D > 0 and a time B ≥ 0. It returns a Boolean value that
indicates whether or not the aircraft will be within horizontal distance D of one another at any time after
B along trajectories which are linear projections of their current states.

CD2D∞ (s, v, D, B) ≡ (kvk = 0 and ksk ≤ D) or

(15)
(kvk > 0 and ∆(s, v, D) ≥ 0 and Θ(s, v, D, 1) ≥ B),

where

∆(s, v, D) ≡ D2 kvk2 − (s · v⊥ )2 , and (16)

2 2 2
Θ(s, v, D, ) ≡ root(kvk , 2(s · v), ksk − D , ). (17)

5 of 12

American Institute of Aeronautics and Astronautics

When ∆(s, v, D) ≥ 0, the function Θ computes the times when the aircraft will loss separation, if  = −1,
or regain separation, if  = 1.
It has been formally proved in the PVS theorem prover that the function CD2D∞ completely and correctly
predicts violations of a minimum distance D after time B, i.e., the following statement holds.
Proposition 1. For all vectors s = so − si , v = vo − vi , distance D > 0, and time B ≥ 0, CD2D∞ (s, v, D, B)
returns true if and only if there exists a time t ≥ B where ks + tvk < D.
Using Horizontal RA` , Vertical RA` , and CD2D∞ , the function that determines whether or not an RA
will be issued for the ownship can be defined as follows.

TCASII RA(so , soz , vo , voz , si , siz , vi , viz ) ≡

let s = so − si , v = vo − vi , sz = soz − siz , vz = voz − viz in
Horizontal RA` (s, v) and (18)
Vertical RA` (sz , vz ) and
CD2D∞ (s, v, HMD` , 0),

where ` is the sensitivity level corresponding to soz and HMD` is the horizontal miss distance for that sensitivity
level. Furthermore, the function that checks if an RA will be issued for the ownship at a given future time
t < tcpa (s, v) can be defined as follows.b

TCASII RA at(so , soz , vo , voz , si , siz , vi , viz , t) ≡

let s = so − si , v = vo − vi , sz = soz − siz , vz = voz − viz in
Horizontal RA` (s + tv, v) and (19)
Vertical RA` (sz + tvz , vz ) and
CD2D∞ (s, v, HMD` , t).

IV. Resolution Advisory Detection

In a similar way that a conflict detection algorithm checks whether or not a loss of separation is predicted
to occur within a period of time, it is possible to design a resolution advisory detection algorithm that checks
whether or not an RA is predicted to be issued for the ownship within a period of time. This sections
presents an analytical formulation of such a resolution advisory detection algorithm, which is called RA3D.
RA3D is a function that takes as parameters the states of the ownship and intruder aircraft and a lookahead
time interval, and returns a Boolean value that indicates whether an RA is predicted to be issued for the
ownship within that time. It has been formally proved that, assuming accurate vector information and
kinematic aircraft trajectories, RA3D correctly and completely characterizes the aircraft states that lead to
an RA for the ownship within the lookahead time interval.
In order to define RA3D, it is necessary to first define a function that detects whether a horizontal RA
will occur between two current or future times. This is accomplished by a function called RA2D` . Then, the
function RAZTimeInterval` is defined that characterizes the time interval where the values of the functions
Vertical RA` and CD2D∞ are set to true. The function RA3D is defined by appropriately calling RA2D` on
the interval returned by RAZTimeInterval` .

IV.A. Characterization of Horizontal RAs

As illustrated by Formula (12) in Section III, the value of τmod ` (s, v) determines whether there is a horizontal
RA when the aircraft have horizontal relative position s and horizontal relative velocity v. Thus, the
minimum value of τmod ` (s+tv, v), where t ranges over the lookahead time interval [B, T ], determines whether
or not a horizontal RA will occur for some time t in this interval. The minimum value of τmod ` can be
computed with a concise formula, namely Formula (20), which defines the function Time Min TAUmod` . This
b Formula (19) assumes that the sensitivity level ` does not change in the time interval [0, t].

6 of 12

American Institute of Aeronautics and Astronautics

function computes exactly the time t in [B, T ] at which τmod ` (s + tv, v) attains its minimum value.



 B if (s + Bv) · v ≥ 0,

t∗ (τ ) if ∆(s, v, DMOD ) < 0,

min `
Time Min TAUmod` (s, v, B, T ) ≡ (20)


 T if (s + T v) · v < 0,

∗

t (0) otherwise,

where
p
−∆(s, v, DMOD` )
τmin ≡2 , (21)
kvk2
t
t∗ (t) ≡ max(B, min(T, tcpa (s, v) − )). (22)
2
It should be noted that Formula (21) and Formula (22) are used in Formula (20) only in cases where the
corresponding conditions imply that kvk2 6= 0 and ∆(s, v, DMOD` ) ≤ 0. Hence, the function Time Min TAUmod`
is well-defined and does not involve divisions by zero or square roots of negative numbers. The function RA2D`
is defined as follows.
RA2D` (s, v, B, T ) ≡ (∆(s, v, DMOD` ) ≥ 0 and (s + Bv) · v < 0 and (s + T v) · v ≥ 0) or
let t = Time Min TAUmod` (s, v, B, T ) in (23)
Horizontal RA` (s + tv, v).

The following proposition, which has been formally proved in the PVS theorem prover, asserts that, for
a given sensitivity level `, the function RA2D` characterizes the set of possible relative states that lead to a
horizontal RA within a lookahead time interval.
Proposition 2. For all vectors s = so −si , v = vo −vi , and lookahead time interval [B, T ], RA2D` (s, v, B, T )
returns true if and only if there exists a time t ∈ [B, T ] where Horizontal RA` (s + tv, v) holds.
For some applications, it may be necessary to determine not only the existence of an RA within a
lookahead time interval, but also the time interval when RAs are issued. The following function computes
such a time interval for horizontal RAs.

RA2DTimeInterval` (s, v, B, T ) ≡
let a = kvk2 ,
b = 2(s · v) + TAU` kvk2 ,
c = ksk2 + TAU` (s · v) − DMOD2` in
if a = 0 and ksk ≤ DMOD` then
[B, T ]
else
let θ = Θ(s, v, DMOD` , 1) in
if ksk ≤ DMOD` then (24)
[B, θ]
elsif (s · v ≥ 0 or b2 − 4ac < 0 then
[T + 1, 0]
elsif ∆(s, v, DMOD` ) ≥ 0 then
[root(a, b, c, −1), θ]
else
[root(a, b, c, −1), root(a, b, c, 1)]
endif.

7 of 12

American Institute of Aeronautics and Astronautics

 The following proposition, which has been formally proved in the PVS theorem prover, asserts that, for
a given sensitivity level `, the function RA2DTimeInterval` computes a time interval that characterizes the
times, within a lookahead time interval [B, T ], at which a horizontal RA will be issued.
Proposition 3. For all vectors s = so − si , v = vo − vi , and lookahead time interval [B, T ],
if RA2DTimeInterval` (s, v, B, T ) returns the time interval [tin , tout ], then for all times t ∈ [B, T ],
Horizontal RA` (s + tv, v) holds if and only if t ∈ [tin , tout ].

IV.B. Characterization of RAs

As noted above, the functions RA2D` and RA2DTimeInterval` can be used to, respectively, detect a horizontal
RA within a lookahead time interval and compute the times, within the lookahead time interval, when a
horizontal RA violation will occur. To completely formalize a TCAS II RA detection algorithm, functions
RA3D and RA3DTimeInterval` , which are analogous to RA2D` and RA2DTimeInterval` , are defined such
that they take into account both the horizontal and vertical components of the TCAS II RA logic. These
functions have as parameters the state information of the ownship, i.e., so , soz , vo , voz , the state information
of the intruder aircraft, i.e., si , siz , vi , viz , the lookahead time interval [B, T ], and a flag hmdf? that indicates
whether or not the horizontal miss distance filter should be used. For RA detection according to the TCAS II
RA logic, that flag should always be set to true.
The function RA2DTimeInterval` computes the times, within the lookahead time interval [B, T ], when
an RA violation will occur. It is formally defined as follows.

RA3DTimeInterval` (so , soz , vo , voz , si , siz , vi , viz , B, T, hmdf?) ≡

let s = so − si , v = vo − vi , sz = soz − siz , vz = voz − viz in
if hmdf? and not CD2D∞ (s, v, HMD` , B) then
[T, B]
elsif vz = 0 and |sz | > ZTHR` then
[T, B]
else
let [tin z , tout z ] = RAZTimeInterval` (sz , vz , B, T ) in
if tout z < B or T < tin z then
[T, B]
else
let [tin , tout ] = [max(B, tin z ), min(T, tout z )],
[tin xy , tout xy ] = RA2DTimeInterval` (s, v, B, T ),
[t1 , t2 ] = [max(tin , min(tout , tin xy )), max(tin , min(tout , tout xy ))] in (25)
if tin xy > tout xy or tout xy < tin or tin xy > tout then
[T, B]
if hmdf? and HMD` < DMOD` and
(s + tin z v) · v ≥ 0 and ks + tin z vk > HMD` then
[T, B]
elsif hmdf? and HMD` < DMOD` then
let θ = Θ(s, v, HMD` , 1),
t3 = if kvk = 0 then T else max(B, min(θ, T )) endif,
t4 = min(t2 , t3 ) in
[t1 , t4 ]
else
[t1 , t2 ]
endif.

8 of 12

American Institute of Aeronautics and Astronautics

 The function RAZTimeInterval` used in Formula (25) computes the time interval when vertical separation
with respect to ZTHR` will be lost within the time interval [B, T ]. It is defined by Formula (26).

[B, T ] if vz = 0,
RAZTimeInterval` (sz , vz , B, T ) ≡ (26)
[ −sign(v z )H−s z sign(v z )ZTHR` −sz
, vz vz ] otherwise,

where H ≡ max(ZTHR` , TAU` |vz |) and sign(vz ) denotes the sign of vz , i.e., -1 when vz < 0 and 1 when vz > 0.
The function RA3D detects RAs by checking the time interval that is returned by RA3DTimeInterval` ,
where ` is the sensitivity level corresponding to soz .

RA3D(so , soz , vo , voz , si , siz , vi , viz , B, T ) ≡

let [tin , tout ] = RA3DTimeInterval` (so , soz , vo , voz , si , siz , vi , viz , B, T, true) in (27)
tin ≤ tout .

Just as for the rest the mathematical development presented in this paper, the following proposition has
been formally proved in the PVS theorem prover. It states that the function RA3D characterizes the set of
aircraft states that will lead to an RA for the ownship within a lookahead time interval assuming that the
aircraft follow linear projections of their current states and the sensitivity level remains constant.

Proposition 4. For all ownship states so , soz , vo , voz , intruder states si , siz , vi , viz , and lookahead time
interval [B, T ], RA3D(so , soz , vo , voz , si , siz , vi , viz , B, T ) returns true if and only if there exists a t ∈ [B, T ]
where TCASII RA at(so , soz , vo , voz , si , siz , vi , viz , t) holds.

V. Corrective Resolution Advisories

As explained in Section II, there are two types of resolution advisories: corrective and preventive. Cor-
rective RAs require a trajectory change by the ownship to regain a minimum altitude limit (ALIM), whose
value depends on the sensitivity level. This section presents mathematical formulas that determine if a given
RA is either corrective or preventive.
The function sep at, defined by Formula (28), predicts the vertical separation between the aircraft at a
given time t assuming a target vertical speed v for the ownship. The ownship is assumed to fly at constant
ground speed and constant vertical acceleration a. Once the target vertical speed v is reached the ownship
continues to fly at constant vertical speed. The function own alt at, defined by Formula (29), computes the
vertical altitude of the ownship at time t given a target vertical speed v and acceleration a. The parameter 
specifies a possible direction for the vertical ownship maneuver, which is upward when  = 1 and downward
when  = −1. The intruder is assumed to continue its trajectory at its current vertical speed.

sep at(soz , voz ,siz , viz , v, a, , t) ≡

let o = own alt at(soz , voz , |v|, a,  sign(v), t),
(28)
i = siz + tviz in
 (o − i).

own alt at(soz , voz , v, a, , t) ≡

let s = stop accel(voz , v, a, , t),
q = min(t, s), (29)
l = max(0, t − s) in
a
 q 2 + qvoz + soz +  l v.
2
The function stop accel computes the time at which the ownship reaches the target vertical speed v. It is

9 of 12

American Institute of Aeronautics and Astronautics

defined as follows.
stop accel(voz , v, a, , t) ≡
if t ≤ 0 or  voz ≥ v then 0
 v − voz (30)
else
a
endif.
The sense of an RA is computed based on the direction for the ownship maneuver that provides a greater
vertical separation, with a bias towards the non-crossing direction. The function RA sense computes such a
direction, where ALIM` is the altitude limit for a given sensitivity level `.
RA sense(soz , voz , siz , viz , v, a, t) ≡
let o↑ = own alt at(soz , voz , v, a, 1, t),
o↓ = own alt at(soz , voz , v, a, −1, t),
i = siz + tviz ,
u = o↑ − i,
d = i − o↓ in (31)
if sign(soz − siz ) = 1 and u ≥ ALIM` then 1
elsif sign(soz − siz ) = −1 and d ≥ ALIM` then − 1
elsif u ≥ d then 1
else − 1
endif.
An RA is corrective if the altitude limit is not cleared when the ownship maneuvers in the direction of
the RA sense. The Boolean function corrective specifies an algorithm that returns true when a given RA
is corrective.
corrective(so , soz , vo , voz , si , siz , vi , viz , v, a) ≡
let s = so − si , v = vo − vi , sz = soz − siz , vz = voz − viz ,
t = τmod ` (s, v),
(32)
 = RA sense(soz , voz , siz , viz , v, a, t) in
ksk < DMOD` or
(s · v < 0 and  (sz + t vz ) < ALIM` ),
where ` is the sensitivity level corresponding to soz .

VI. Related Work

Formal models of TCAS have been proposed before. Leveson et al. provides a complete specification of
the TCAS II logic in a tabular notation called Requirements State Machine Language (RSML).8 Livadas et
al. presents a high level model of the core components of TCAS using the formalism of Hybrid Input/Output
Automata (HIOA).9 The model presented here is more modest than those models. This paper focuses on
the collision avoidance logic that deals with resolution advisories and assumes that accurate state vector
information will be available to sense and avoid systems. A key difference between this work and other
models, such as those listed above, is the introduction of this vector information, which enables the derivations
of the concise formulas presented in this paper for computing TCAS II RA information, especially those
formulas used to analytically detect future RAs. The assumption that accurate state vector information is
available reduces the complexity in the TCAS II logic concerning aircraft tracking and enables the analytical
presentation, which is based on vector arithmetic. It should be noted that the algorithm presented in
Section V projects aircraft vertical trajectories using constant acceleration and a target vertical speed as
specified in the TCAS II logic, rather than constant vertical speed as specified in.9
Safety properties related to issuance of resolution advisories have been verified by Coen-Porisini et al.10
using symbolic execution and, more recently, by Gotlieb11 using constraint programming. These works rely

10 of 12

American Institute of Aeronautics and Astronautics

on a C implementation of the core TCAS II RA logic that is available at the Software-artifact Infrastructure
Repository (SIR) maintained by the University of Nebraska–Lincoln. That code deals with high-level aspects
of the function that computes the sense of an RA, but does not implement the mathematical formulas that
determine whether or not an RA is issued.

VII. Conclusion
This paper presents a formal development that consists of a mathematical model of the TCAS II resolution
advisory logic and algorithms for detecting RAs within a given lookahead time interval and for checking
whether a given RA is corrective or not.
As far as the authors know, an algorithm for detecting resolution advisories has not been proposed before.
This algorithm is a key component of NASA’s Separation Assurance concept for the integration of UAS in
the NAS.4 In particular, it is used to implement airborne and ground capabilities that allow UAS pilots to
avoid encounter scenarios that are not well-clear vis-a-vis systems such as TCAS. It should be noted that
the algorithm presented here can be easily parameterized into an algorithm for detecting traffic advisories.
This is possible since the TCAS II logic for traffic advisories and the logic for resolution advisories mainly
differ in the values of the time and distance threshold parameters and the use of an horizontal miss distance
filter. Indeed, the function TA3D defined by Formula (33) detects Traffic Alerts (TAs) within a lookahead
time interval [B, T ], when the threshold values TAU` , DMOD` , and ZTHR` are taken from Table 2.2 In this case,
the function RA3DTimeInterval` is called with the parameter corresponding to the horizontal miss distance
filter hmdf? set to false.

TA3D(so , soz , vo , voz , si , siz , vi , viz , B, T ) ≡

let [tin , tout ] = RA3DTimeInterval` (so , soz , vo , voz , si , siz , vi , viz , B, T, false) in (33)
tin ≤ tout .

Table 2. TCAS Sensitivity Level Definition and Alarm Thresholds for TAs

Ownship Altitude SL TAU DMOD ZTHR

(feet) (sec) (nmi) (feet)
1000 - 2350 2 20 0.30 850
1000 - 2350 3 25 0.33 850
2350 - 5000 4 30 0.48 850
5000 -10000 5 40 0.75 850
10000 - 20000 6 45 1.0 850
20000 - 42000 7 48 1.3 850
> 42000 7 48 1.3 1200

Finally, it is emphasized that the mathematical development presented here has been formalized and
mechanically verified in PVS. This level of rigor is justified by the safety-critical role that sense-and-avoid
UAS systems may play in the future airspace system.

References
1 FAA Sponsored Sense and Avoid Workshop, “Sense and avoid (SAA) for unmanned aircraft systems (UAS),” October
2009.
2 U.S. Department of Transportation Federal Aviation Administration, “Introduction to TCAS II Version 7.1,” February
2011.
3 RTCA SC-147, “RTCA-DO-185B, Minimum operational performance standards for traffic alert and collision avoidance
system II (TCAS II),” July 2009.
4 Consiglio, M., Chamberlain, J., Muñoz, C., and Hoffler, K., “Concept of integration for UAS operations in the NAS,”

Proceedings of 28th International Congress of the Aeronautical Sciences, ICAS 2012 , Brisbane, Australia, 2012.
5 Owre, S., Rushby, J., and Shankar, N., “PVS: A Prototype Verification System,” Proc. 11th Int. Conf. on Automated

Deduction, edited by D. Kapur, Vol. 607 of Lecture Notes in Artificial Intelligence, Springer-Verlag, June 1992, pp. 748–752.

11 of 12

American Institute of Aeronautics and Astronautics

 6 Kuchar, J., “Update on the analysis of ACAS performance on Global Hawk,” May 2006, ASP/WG A/WP A10-04.
7 Hammer, J., “Horizontal miss distance filter system for suppressing false resolution alerts,” October 1996, U.S. Patent
5,566,074.
8 Leveson, N. G., Heimdahl, M., Hildreth, H., and Reese, J. D., “Requirements Specification for Process-Control Systems,”

IEEE Transactions on Software Engineering, Vol. 20, No. 9, 1994, pp. 684–707.
9 Livadas, C., Lygeros, J., and Lynch, N., “High-Level Modeling and Analysis of the Traffic Alert and Collision Avoidance

System (TCAS),” Proceedings of IEEE, Special Issue on Hybrid Systems: Theory & Applications, Vol. 88, No. 7, July 2000,
pp. 926–948.
10 Coen-Porisini, A., Denaro, G., Ghezzi, C., and Pezzè, M., “Using Symbolic Execution for Verifying Safety-Critical

Systems,” Proceedings of the European Software Engineering Conference (ESEC 2001/FSE 9), No. 142–151, ACM, Vienna,
Austria, 2001.
11 Gotlieb, A., “TCAS software verification using constraint programming,” The Knowledge Engineering Review , Vol. 27,

No. 3, September 2012, pp. 343–360.

12 of 12

American Institute of Aeronautics and Astronautics