> ## Documentation Index > Fetch the complete documentation index at: https://docs.alchemicalchef.io/llms.txt > Use this file to discover all available pages before exploring further. # TCAS II Formal Specification > A TLA+ specification of TCAS collision avoidance system per RTCA DO-185B The Traffic Collision Avoidance System (TCAS) II is one of the most safety-critical systems in commercial aviation. Mandated on all aircraft with more than 30 seats, TCAS provides the last line of defense against mid-air collisions. When two aircraft are on a collision course, TCAS coordinates vertical maneuvers to ensure they diverge one climbs, one descends. This specification models TCAS II Version 7.1, the current standard defined in RTCA DO-185B. Version 7.1 introduced critical improvements over 7.0, particularly in handling cases where the intruder aircraft doesn't follow their Resolution Advisory (RA). The 2002 Überlingen mid-air collision, where conflicting instructions from TCAS and ATC led to tragedy, drove many of these enhancements. ## Why Formally Specify TCAS? TCAS is a distributed system with real-time constraints, coordination requirements, and safety-critical invariants. Plus I was asked if I could figure it out, this is my attempt at doing so. The specification captures: * **Sensitivity levels (SL2-SL7)** with altitude-dependent thresholds * **Modified tau formula** for threat detection that handles low closure rates * **DMOD, ZTHR, and ALIM parameters** per altitude band * **Altitude inhibitions** preventing dangerous advisories near the ground * **Preventive vs Corrective RA selection** based on predicted miss distance * **RA timing constraints** preventing oscillation between advisories * **Multi-threat logic** when multiple intruders exist simultaneously * **Version 7.1 enhancements** for detecting intruder non-compliance The formal model allows verification of properties like "coordinated RAs always have complementary senses" and "no descent RA is issued below 1100 feet AGL." ## Specification Overview The specification defines several key components: ### Sensitivity Levels TCAS adjusts its alerting thresholds based on altitude above ground level (AGL). Lower altitudes use more aggressive thresholds because there's less time and space to maneuver: | Sensitivity Level | Altitude AGL | TAU for RA | DMOD | ALIM | | ----------------- | -------------- | ---------- | ------- | ------ | | SL2 | \< 1000 ft | No RA | - | - | | SL3 | 1000-2350 ft | 15 sec | 0.20 nm | 300 ft | | SL4 | 2350-5000 ft | 20 sec | 0.35 nm | 300 ft | | SL5 | 5000-10000 ft | 25 sec | 0.55 nm | 350 ft | | SL6 | 10000-20000 ft | 30 sec | 0.80 nm | 400 ft | | SL7 | > 20000 ft | 35 sec | 1.10 nm | 600 ft | ### Advisory Types The specification models the full RA vocabulary: * **Corrective RAs**: Require immediate pilot action (Climb, Descend, Increase Climb/Descend, Crossing maneuvers, Reversals) * **Preventive RAs**: Limit vertical rate without requiring action (Don't Climb, Don't Descend, Limit Climb/Descend to specific rates) * **Weakening RAs**: Reduce RA strength as threat diminishes (Level Off, Maintain VS) ### Coordination Protocol When two TCAS II-equipped aircraft encounter each other, they coordinate via Mode S datalink to ensure complementary maneuvers. The specification models: * Sense selection based on geometry and received coordination * Reversal when same-sense conflict detected * Version 7.1 enhancement: reversal when intruder non-compliance detected ## Full TLA+ Specification ```tla theme={null} ------------------------------- MODULE TCAS_v71 ------------------------------- (***************************************************************************) (* TCAS II Version 7.1 Specification (Per RTCA DO-185B) *) (* *) (* This specification models TCAS II with accurate: *) (* - Sensitivity levels (SL2-SL7) with correct thresholds *) (* - Modified tau formula for threat detection *) (* - DMOD, ZTHR, and ALIM parameters per altitude band *) (* - Altitude inhibitions (no RA below 1000 ft AGL) *) (* - Preventive vs Corrective RA selection *) (* - RA timing constraints *) (* - Full RA type enumeration *) (***************************************************************************) EXTENDS Integers, Sequences, FiniteSets, TLC CONSTANTS Aircraft, \* Set of aircraft identifiers MaxAltitudeMSL, \* Maximum altitude MSL (feet / 100) MinAltitudeMSL, \* Minimum altitude MSL (feet / 100) GroundElevation \* Ground elevation for AGL calculation (feet / 100) ASSUME /\ Aircraft # {} /\ MaxAltitudeMSL > MinAltitudeMSL /\ GroundElevation >= 0 (***************************************************************************) (* TCAS II Version 7.1 Threshold Tables (Per DO-185B) *) (* *) (* All altitudes in feet/100, times in seconds, distances in nm*100 *) (***************************************************************************) \* Sensitivity Level based on own altitude AGL \* Returns SL 2-7 SensitivityLevel(altAGL) == IF altAGL < 10 THEN 2 \* < 1000 ft AGL → SL2 (TA only!) ELSE IF altAGL < 24 THEN 3 \* 1000-2350 ft → SL3 ELSE IF altAGL < 50 THEN 4 \* 2350-5000 ft → SL4 ELSE IF altAGL < 100 THEN 5 \* 5000-10000 ft → SL5 ELSE IF altAGL < 200 THEN 6 \* 10000-20000 ft → SL6 ELSE 7 \* > 20000 ft → SL7 \* TAU thresholds for Traffic Advisory (seconds) TAU_TA(sl) == CASE sl = 2 -> 20 [] sl = 3 -> 25 [] sl = 4 -> 30 [] sl = 5 -> 40 [] sl = 6 -> 45 [] sl = 7 -> 48 [] OTHER -> 48 \* TAU thresholds for Resolution Advisory (seconds) \* Note: SL2 returns 9999 (effectively infinite) - NO RA at SL2! TAU_RA(sl) == CASE sl = 2 -> 9999 \* No RA below 1000 ft AGL! [] sl = 3 -> 15 [] sl = 4 -> 20 [] sl = 5 -> 25 [] sl = 6 -> 30 [] sl = 7 -> 35 [] OTHER -> 35 \* DMOD for Traffic Advisory (nm * 100) DMOD_TA(sl) == CASE sl = 2 -> 30 \* 0.30 nm [] sl = 3 -> 33 \* 0.33 nm [] sl = 4 -> 48 \* 0.48 nm [] sl = 5 -> 75 \* 0.75 nm [] sl = 6 -> 100 \* 1.00 nm [] sl = 7 -> 130 \* 1.30 nm [] OTHER -> 130 \* DMOD for Resolution Advisory (nm * 100) DMOD_RA(sl) == CASE sl = 2 -> 9999 \* No RA at SL2 [] sl = 3 -> 20 \* 0.20 nm [] sl = 4 -> 35 \* 0.35 nm [] sl = 5 -> 55 \* 0.55 nm [] sl = 6 -> 80 \* 0.80 nm [] sl = 7 -> 110 \* 1.10 nm [] OTHER -> 110 \* ZTHR (Vertical threshold) for TA (feet) \* Note: All sensitivity levels use 850 ft for TA threshold ZTHR_TA(sl) == 850 \* ZTHR (Vertical threshold) for RA (feet) ZTHR_RA(sl) == CASE sl = 2 -> 9999 \* No RA at SL2 [] sl = 3 -> 600 [] sl = 4 -> 600 [] sl = 5 -> 600 [] sl = 6 -> 600 [] sl = 7 -> 700 [] OTHER -> 700 \* ALIM - Altitude Limit for RA (target separation in feet) ALIM(sl) == CASE sl = 2 -> 9999 \* No RA at SL2 [] sl = 3 -> 300 [] sl = 4 -> 300 [] sl = 5 -> 350 [] sl = 6 -> 400 [] sl = 7 -> 600 [] OTHER -> 600 (***************************************************************************) (* Above FL420 Special Thresholds (Per DO-185B) *) (* *) (* Above FL420 (42,000 ft), TCAS uses expanded thresholds due to higher *) (* aircraft performance and thinner air affecting climb/descent rates. *) (***************************************************************************) \* Check if aircraft is above FL420 (42,000 ft = 420 in our units) IsAboveFL420(altMSL) == altMSL >= 420 \* ZTHR for TA above FL420 (expanded from 850 to 1200 ft) ZTHR_TA_FL420 == 1200 \* ZTHR for RA above FL420 (expanded from 700 to 800 ft) ZTHR_RA_FL420 == 800 \* ALIM above FL420 (expanded from 600 to 700 ft) ALIM_FL420 == 700 \* Get effective ZTHR_TA considering FL420 EffectiveZTHR_TA(sl, altMSL) == IF IsAboveFL420(altMSL) THEN ZTHR_TA_FL420 ELSE ZTHR_TA(sl) \* Get effective ZTHR_RA considering FL420 EffectiveZTHR_RA(sl, altMSL) == IF IsAboveFL420(altMSL) THEN ZTHR_RA_FL420 ELSE ZTHR_RA(sl) \* Get effective ALIM considering FL420 EffectiveALIM(sl, altMSL) == IF IsAboveFL420(altMSL) THEN ALIM_FL420 ELSE ALIM(sl) (***************************************************************************) (* HMD Filter (Horizontal Miss Distance) Per DO-185B *) (* *) (* The HMD filter prevents false alerts when aircraft will pass with *) (* adequate horizontal separation even if tau criteria are met. *) (* HMD = predicted horizontal distance at closest point of approach (CPA) *) (***************************************************************************) \* HMD threshold for TA (nm * 100) - same as DMOD_TA HMD_TA(sl) == DMOD_TA(sl) \* HMD threshold for RA (nm * 100) - same as DMOD_RA HMD_RA(sl) == DMOD_RA(sl) \* Calculate predicted HMD (Horizontal Miss Distance) at CPA \* Per DO-185B: HMD is the predicted horizontal distance at closest point of approach \* \* For a more accurate model (but still simplified without bearing): \* - If aircraft are closing (rDot < 0), HMD depends on crossing geometry \* - Head-on collision course: HMD ≈ 0 \* - Crossing/passing: HMD depends on lateral offset \* \* Improved approximation: Use range rate magnitude relative to closure \* If closure is fast relative to range, likely head-on (HMD small) \* If closure is slow, likely crossing (HMD larger, proportional to range) PredictedHMD(a, b) == LET r == horizontalRange[a][b] rDot == rangeRate[a][b] \* tau computation: if not closing (rDot >= 0), no CPA approaching tau == IF rDot >= 0 THEN 9999 ELSE r \div (-rDot) \* Time to CPA in seconds IN IF rDot >= 0 THEN r \* Diverging or parallel - HMD is at least current range ELSE IF tau > 120 THEN r \* Far away (> 2 min), use current range ELSE IF tau < 5 THEN 0 \* Very close to CPA, minimal HMD \* For intermediate cases: estimate based on closure geometry \* Faster closure relative to range suggests more direct approach (lower HMD) \* Closure rate of 1 nm/min at 1 nm range = direct approach \* Use: HMD ≈ r * (1 - closure_factor) where closure_factor = min(1, |rDot|*60/r) ELSE LET closureFactor == Min(100, ((-rDot) * 60 * 100) \div Max(1, r)) IN (r * (100 - closureFactor)) \div 100 \* HMD filter passes (threat not filtered out) HMDFilterPasses_TA(a, b) == PredictedHMD(a, b) < HMD_TA(sensitivityLvl[a]) HMDFilterPasses_RA(a, b) == PredictedHMD(a, b) < HMD_RA(sensitivityLvl[a]) (***************************************************************************) (* TCAS Operating Modes *) (* *) (* TCAS II can operate in three modes: *) (* - Standby: TCAS surveillance only, no advisories *) (* - TAOnly: Traffic Advisories only, no Resolution Advisories *) (* - TARA: Full TA/RA capability (normal operation) *) (***************************************************************************) TCASMode == {"Standby", "TAOnly", "TARA"} (***************************************************************************) (* Aural Annunciations (Per TCAS II v7.1) *) (* *) (* TCAS provides aural alerts to pilots for each advisory type. *) (***************************************************************************) AuralType == { "None", \* Traffic Advisory "TrafficTraffic", \* "Traffic, Traffic" \* Corrective RAs "ClimbClimb", \* "Climb, Climb" "DescendDescend", \* "Descend, Descend" "IncreaseClimb", \* "Increase Climb, Increase Climb" "IncreaseDescend", \* "Increase Descent, Increase Descent" "ClimbClimbNow", \* "Climb, Climb NOW" (reversal) "DescendDescendNow", \* "Descend, Descend NOW" (reversal) "ClimbCrossingClimb", \* "Climb, Crossing Climb" "DescendCrossingDescend", \* "Descend, Crossing Descend" \* Preventive RAs "MonitorVerticalSpeed", \* "Monitor Vertical Speed" \* Weakening/Clear (v7.1: "Adjust VS" replaced by "Level Off") "MaintainVerticalSpeed", \* "Maintain Vertical Speed, Maintain" "LevelOffLevelOff", \* "Level Off, Level Off" (v7.1 replacement for "Adjust VS") "ClearOfConflict" \* "Clear of Conflict" } \* Map RA type to aural annunciation \* Note: v7.1 replaced "Adjust Vertical Speed" with "Level Off, Level Off" AuralForRA(ra) == CASE ra = "Climb" -> "ClimbClimb" [] ra = "Descend" -> "DescendDescend" [] ra = "IncreaseClimb" -> "IncreaseClimb" [] ra = "IncreaseDescend" -> "IncreaseDescend" [] ra = "ReversalToClimb" -> "ClimbClimbNow" [] ra = "ReversalToDescend" -> "DescendDescendNow" [] ra = "CrossingClimb" -> "ClimbCrossingClimb" [] ra = "CrossingDescend" -> "DescendCrossingDescend" [] ra = "DontClimb" -> "MonitorVerticalSpeed" [] ra = "DontDescend" -> "MonitorVerticalSpeed" [] ra \in {"LimitClimb500", "LimitClimb1000", "LimitClimb2000", "LimitDescend500", "LimitDescend1000", "LimitDescend2000"} -> "MonitorVerticalSpeed" [] ra = "LevelOff" -> "LevelOffLevelOff" [] ra = "MaintainVS" -> "MaintainVerticalSpeed" [] ra = "MonitorVS" -> "MonitorVerticalSpeed" [] ra = "TA" -> "TrafficTraffic" [] OTHER -> "None" (***************************************************************************) (* Transponder and TCAS Equipment *) (***************************************************************************) TransponderMode == {"Off", "ModeA", "ModeC", "ModeS", "Failed"} TCASLevel == {"None", "TCAS_I", "TCAS_II"} (***************************************************************************) (* RA Types (Per TCAS II Version 7.1) *) (***************************************************************************) \* Corrective RAs - require immediate pilot action CorrectiveRA == { "Climb", \* Climb at 1500-2000 fpm "Descend", \* Descend at 1500-2000 fpm "IncreaseClimb", \* Increase climb to 2500 fpm "IncreaseDescend", \* Increase descent to 2500 fpm "CrossingClimb", \* Climb, crossing through intruder altitude "CrossingDescend", \* Descend, crossing through intruder altitude "ReversalToClimb", \* Reverse from descend to climb "ReversalToDescend" \* Reverse from climb to descend } \* Preventive RAs - limit vertical rate (don't go there) PreventiveRA == { "DontClimb", \* Don't climb (maintain or descend) "DontDescend", \* Don't descend (maintain or climb) "LimitClimb500", \* Limit climb to 500 fpm "LimitClimb1000", \* Limit climb to 1000 fpm "LimitClimb2000", \* Limit climb to 2000 fpm "LimitDescend500", \* Limit descent to 500 fpm "LimitDescend1000", \* Limit descent to 1000 fpm "LimitDescend2000" \* Limit descent to 2000 fpm } \* Weakening RAs - reduce the RA strength \* Note: "Adjust Vertical Speed" was REPLACED by "Level Off" in v7.1 WeakeningRA == { "LevelOff", \* Reduce vertical rate to 0 (v7.1 replaces "Adjust VS") "MaintainVS", \* Maintain current VS "MonitorVS" \* Monitor VS (becoming advisory) } AllRATypes == CorrectiveRA \cup PreventiveRA \cup WeakeningRA AdvisoryType == AllRATypes \cup {"None", "TA"} RASense == {"None", "Up", "Down"} ComplianceState == {"Complying", "NotComplying", "NoAdvisory"} (***************************************************************************) (* State Variables *) (***************************************************************************) VARIABLES \* Aircraft physical state altitudeMSL, \* Altitude MSL (feet / 100) altitudeAGL, \* Altitude AGL (feet / 100) - for inhibitions verticalRate, \* Vertical rate (feet/min / 100) horizontalRange, \* Range to other aircraft (nm * 100) rangeRate, \* Range rate / closure rate (nm/sec * 100, negative = closing) verticalSep, \* Vertical separation (feet / 100) \* Equipment state transponder, \* Transponder mode tcasEquipped, \* TCAS equipment level tcasMode, \* TCAS operating mode (Standby/TAOnly/TARA) \* TCAS computed state sensitivityLvl, \* Current sensitivity level (2-7) \* Advisory state advisory, \* Current advisory raSense, \* RA sense (Up/Down/None) raIssuedTime, \* When RA was issued (for timing constraints) intruders, \* Set of threatening aircraft auralAlert, \* Current aural annunciation \* Coordination state coordinatedSense, \* Sense being coordinated via Mode S receivedCoord, \* Coordination received from intruder \* Pilot state pilotCompliance, \* System time time vars == <> (***************************************************************************) (* Type Invariant *) (***************************************************************************) TypeOK == /\ altitudeMSL \in [Aircraft -> MinAltitudeMSL..MaxAltitudeMSL] /\ altitudeAGL \in [Aircraft -> 0..(MaxAltitudeMSL - GroundElevation)] /\ verticalRate \in [Aircraft -> -60..60] \* ±6000 fpm /\ horizontalRange \in [Aircraft -> [Aircraft -> 0..500]] \* 0-5 nm /\ rangeRate \in [Aircraft -> [Aircraft -> -100..100]] /\ verticalSep \in [Aircraft -> [Aircraft -> -500..500]] /\ transponder \in [Aircraft -> TransponderMode] /\ tcasEquipped \in [Aircraft -> TCASLevel] /\ tcasMode \in [Aircraft -> TCASMode] /\ sensitivityLvl \in [Aircraft -> 2..7] /\ advisory \in [Aircraft -> AdvisoryType] /\ raSense \in [Aircraft -> RASense] /\ raIssuedTime \in [Aircraft -> Nat] /\ intruders \in [Aircraft -> SUBSET Aircraft] /\ auralAlert \in [Aircraft -> AuralType] /\ coordinatedSense \in [Aircraft -> RASense] /\ receivedCoord \in [Aircraft -> RASense] /\ pilotCompliance \in [Aircraft -> ComplianceState] /\ time \in Nat (***************************************************************************) (* Helper Functions *) (***************************************************************************) Abs(x) == IF x < 0 THEN -x ELSE x Max(x, y) == IF x > y THEN x ELSE y Min(x, y) == IF x < y THEN x ELSE y \* Can aircraft 'a' see aircraft 'b' via TCAS? CanSee(a, b) == /\ a # b /\ tcasEquipped[a] \in {"TCAS_I", "TCAS_II"} /\ transponder[b] \in {"ModeC", "ModeS"} \* Can coordination occur between a and b? CanCoordinate(a, b) == /\ a # b /\ tcasEquipped[a] = "TCAS_II" /\ tcasEquipped[b] = "TCAS_II" /\ transponder[a] = "ModeS" /\ transponder[b] = "ModeS" (***************************************************************************) (* Intruder Compliance Detection (TCAS II v7.1 Enhancement) *) (* *) (* Version 7.1 monitors the intruder's vertical rate to detect when they *) (* are NOT following their coordinated RA. If non-compliance is detected, *) (* TCAS can issue a reversal to the compliant aircraft. *) (***************************************************************************) \* Detect if intruder b is not complying with their RA \* This looks at intruder's actual vertical rate vs expected behavior \* based on the coordination sense they sent (which indicates their RA sense) IntruderNotComplying(a, b) == /\ CanCoordinate(a, b) /\ receivedCoord[a] # "None" \* We received coordination from them /\ LET intruderSense == receivedCoord[a] \* Their coordinated sense intruderVR == verticalRate[b] \* Their actual vertical rate \* Compliance threshold: should show significant response \* Positive VR means climbing, negative means descending IN \/ (intruderSense = "Up" /\ intruderVR < 5) \* Should climb but isn't \/ (intruderSense = "Down" /\ intruderVR > -5) \* Should descend but isn't \* Check if enough time has passed to expect pilot response PilotResponseOverdue(a) == time - raIssuedTime[a] >= EXPECTED_PILOT_RESPONSE \* Detect if intruder is definitively not complying (after response time) \* This is used to trigger v7.1 enhanced reversal logic IntruderDefinitelyNotComplying(a, b) == /\ IntruderNotComplying(a, b) /\ b \in intruders[a] /\ raIssuedTime[b] > 0 \* Intruder has an active RA /\ time - raIssuedTime[b] >= EXPECTED_PILOT_RESPONSE \* Response time elapsed (***************************************************************************) (* Modified Tau Calculation (Per DO-185B) *) (* *) (* τ_mod = -(r² - DMOD²) / (r × ṙ) *) (* *) (* This handles low closure rate scenarios better than simple tau. *) (***************************************************************************) \* Modified horizontal tau for TA \* Protected against division by zero when r = 0 ModifiedTauTA(a, b) == LET r == horizontalRange[a][b] rDot == rangeRate[a][b] dmod == DMOD_TA(sensitivityLvl[a]) IN IF rDot >= 0 THEN 9999 \* Not closing ELSE IF r = 0 THEN 0 \* At collision point ELSE IF r <= dmod THEN 0 \* Already inside DMOD ELSE ((r * r) - (dmod * dmod)) \div ((-rDot) * r) \* Modified horizontal tau for RA \* Protected against division by zero when r = 0 ModifiedTauRA(a, b) == LET r == horizontalRange[a][b] rDot == rangeRate[a][b] dmod == DMOD_RA(sensitivityLvl[a]) IN IF rDot >= 0 THEN 9999 ELSE IF r = 0 THEN 0 \* At collision point ELSE IF r <= dmod THEN 0 ELSE ((r * r) - (dmod * dmod)) \div ((-rDot) * r) \* Vertical tau (time to co-altitude in SECONDS) \* Note: verticalRate is in feet/min/100, so we need to convert properly \* Result must be in seconds to match horizontal tau calculations VerticalTau(a, b) == LET altDiff == verticalSep[a][b] * 100 \* Convert to feet vrDiff == (verticalRate[b] - verticalRate[a]) * 100 \* feet/min IN IF vrDiff = 0 THEN 9999 ELSE IF (altDiff * vrDiff) < 0 THEN 9999 \* Diverging vertically \* Result is (feet / feet/min) = minutes, multiply by 60 to get seconds ELSE (Abs(altDiff) * 60) \div Abs(vrDiff) (***************************************************************************) (* Threat Detection (Per DO-185B) *) (* *) (* TA Condition: τ_mod < TAU_TA AND vertical_sep < ZTHR_TA *) (* RA Condition: τ_mod < TAU_RA AND vertical_sep < ZTHR_RA AND SL >= 3 *) (***************************************************************************) \* Traffic Advisory condition (with HMD filter and FL420 support) TACondition(a, b) == /\ CanSee(a, b) /\ tcasMode[a] \in {"TAOnly", "TARA"} \* Not in Standby /\ ModifiedTauTA(a, b) < TAU_TA(sensitivityLvl[a]) /\ Abs(verticalSep[a][b]) * 100 < EffectiveZTHR_TA(sensitivityLvl[a], altitudeMSL[a]) /\ HMDFilterPasses_TA(a, b) \* HMD filter \* Resolution Advisory condition (with HMD filter and FL420 support) RACondition(a, b) == /\ CanSee(a, b) /\ tcasEquipped[a] = "TCAS_II" /\ tcasMode[a] = "TARA" \* Full TA/RA mode only /\ sensitivityLvl[a] >= 3 \* No RA at SL2! /\ ModifiedTauRA(a, b) < TAU_RA(sensitivityLvl[a]) /\ Abs(verticalSep[a][b]) * 100 < EffectiveZTHR_RA(sensitivityLvl[a], altitudeMSL[a]) /\ HMDFilterPasses_RA(a, b) \* HMD filter (***************************************************************************) (* Altitude Inhibitions (Per DO-185B) *) (* *) (* Below 1000 ft AGL: No RAs (SL2) *) (* Below 1100 ft AGL: No Descend RAs *) (* Below 1550 ft AGL: No Increase Descend RAs *) (***************************************************************************) \* Can any RA be issued? RANotInhibited(a) == altitudeAGL[a] >= 10 \* >= 1000 ft AGL \* Can Descend RA be issued? DescendRANotInhibited(a) == altitudeAGL[a] >= 11 \* >= 1100 ft AGL \* Can Increase Descend RA be issued? IncreaseDescendNotInhibited(a) == altitudeAGL[a] >= 16 \* >= 1550 ft AGL \* Can Crossing Descend RA be issued? \* Same inhibition as regular Descend RA CrossingDescendNotInhibited(a) == altitudeAGL[a] >= 11 \* >= 1100 ft AGL (***************************************************************************) (* RA Selection Logic *) (* *) (* 1. Calculate predicted VMD (Vertical Miss Distance) at CPA *) (* 2. If VMD >= ALIM: Issue preventive RA *) (* 3. If VMD < ALIM: Issue corrective RA *) (* 4. Select sense based on geometry and coordination *) (***************************************************************************) \* Predict vertical miss distance at CPA PredictedVMD(a, b) == LET tau == Min(ModifiedTauRA(a, b), VerticalTau(a, b)) \* Project altitudes forward by tau seconds altA_atCPA == altitudeMSL[a] + (verticalRate[a] * tau \div 60) altB_atCPA == altitudeMSL[b] + (verticalRate[b] * tau \div 60) IN Abs(altA_atCPA - altB_atCPA) * 100 \* In feet \* Determine if preventive RA is sufficient IsPreventiveSufficient(a, b) == PredictedVMD(a, b) >= ALIM(sensitivityLvl[a]) \* Select RA sense considering coordination, inhibitions, and own aircraft trajectory \* Per DO-185B: Prefer sense that requires less deviation from current trajectory SelectSense(a, b) == LET theirCoord == receivedCoord[a] myAlt == altitudeMSL[a] theirAlt == altitudeMSL[b] myVR == verticalRate[a] \* Own vertical rate (positive = climbing) \* Threshold for "significant" vertical rate (500 fpm = 5 in our units) significantVR == 5 IN \* Priority 1: If coordination received, comply with complementary sense IF theirCoord = "Up" THEN "Down" ELSE IF theirCoord = "Down" THEN "Up" \* Priority 2: Check altitude inhibitions ELSE IF ~DescendRANotInhibited(a) THEN "Up" \* Can't descend near ground \* Priority 3: If already in significant climb/descent, prefer that direction \* This minimizes required maneuver deviation (DO-185B optimization) ELSE IF myVR >= significantVR THEN "Up" \* Already climbing, continue up ELSE IF myVR <= -significantVR THEN "Down" \* Already descending, continue down \* Priority 4: Select based on geometry - maneuver away from intruder ELSE IF myAlt > theirAlt THEN "Up" \* Above intruder: climb away ELSE IF myAlt < theirAlt THEN "Down" \* Below intruder: descend away ELSE "Up" \* Same altitude, default to climb \* Determine if crossing RA is needed \* Crossing RA is issued when own aircraft must pass through intruder's altitude \* to achieve safe separation (intruder is between own and target altitude) NeedsCrossingRA(a, b) == LET myAlt == altitudeMSL[a] theirAlt == altitudeMSL[b] sense == SelectSense(a, b) alim == EffectiveALIM(sensitivityLvl[a], altitudeMSL[a]) targetAlt == IF sense = "Up" THEN theirAlt + (alim \div 100) + 1 ELSE theirAlt - (alim \div 100) - 1 IN \* Crossing needed if intruder is between current and target altitude \/ (sense = "Up" /\ theirAlt > myAlt /\ theirAlt < targetAlt) \/ (sense = "Down" /\ theirAlt < myAlt /\ theirAlt > targetAlt) \* Select specific RA type (with crossing RA support and altitude inhibitions) SelectRA(a, b) == LET sense == SelectSense(a, b) preventive == IsPreventiveSufficient(a, b) crossing == NeedsCrossingRA(a, b) IN IF preventive THEN IF sense = "Up" THEN "DontDescend" ELSE "DontClimb" ELSE IF crossing THEN IF sense = "Up" THEN "CrossingClimb" \* CrossingDescend has same inhibition as regular Descend ELSE IF CrossingDescendNotInhibited(a) THEN "CrossingDescend" ELSE "Descend" \* Fall back to regular Descend if crossing inhibited ELSE IF sense = "Up" THEN "Climb" ELSE "Descend" (***************************************************************************) (* Multi-Threat RA Selection (Per DO-185B) *) (* *) (* When multiple intruders exist, TCAS must select a single RA that *) (* provides safe separation from ALL threats. If no single sense works, *) (* TCAS may issue a composite RA (level off, or pass through). *) (***************************************************************************) \* Count threats above own aircraft ThreatsAbove(a) == {b \in intruders[a] : altitudeMSL[b] > altitudeMSL[a]} \* Count threats below own aircraft ThreatsBelow(a) == {b \in intruders[a] : altitudeMSL[b] < altitudeMSL[a]} \* Count co-altitude threats ThreatsCoAlt(a) == {b \in intruders[a] : altitudeMSL[b] = altitudeMSL[a]} \* Determine if a single sense can provide separation from all threats SingleSensePossible(a) == \/ Cardinality(ThreatsAbove(a)) = 0 \* Can climb \/ Cardinality(ThreatsBelow(a)) = 0 \* Can descend \* Select sense considering ALL threats (multi-threat logic) SelectMultiThreatSense(a) == LET above == Cardinality(ThreatsAbove(a)) below == Cardinality(ThreatsBelow(a)) coordReceived == receivedCoord[a] IN \* If coordination received, comply with complementary sense IF coordReceived = "Up" THEN "Down" ELSE IF coordReceived = "Down" THEN "Up" \* Check altitude inhibitions ELSE IF ~DescendRANotInhibited(a) THEN "Up" \* Select based on threat geometry ELSE IF above = 0 THEN "Up" \* No threats above, climb ELSE IF below = 0 THEN "Down" \* No threats below, descend \* Both above and below threats - select based on minimum separation needed ELSE IF above <= below THEN "Up" \* Fewer threats above, try to climb ELSE "Down" \* Check if any intruder requires a crossing maneuver AnyIntruderNeedsCrossing(a) == \E b \in intruders[a] : NeedsCrossingRA(a, b) \* Select RA for multi-threat scenario \* Enhanced to consider crossing RAs when needed SelectMultiThreatRA(a) == LET sense == SelectMultiThreatSense(a) \* Check if preventive is sufficient for ALL threats allPreventiveSufficient == \A b \in intruders[a] : IsPreventiveSufficient(a, b) \* Check if any intruder requires crossing maneuver needsCrossing == AnyIntruderNeedsCrossing(a) IN IF ~SingleSensePossible(a) THEN "LevelOff" \* Cannot escape up or down - level off ELSE IF allPreventiveSufficient THEN IF sense = "Up" THEN "DontDescend" ELSE "DontClimb" ELSE IF needsCrossing THEN \* Crossing RA needed - check altitude inhibitions IF sense = "Up" THEN "CrossingClimb" ELSE IF CrossingDescendNotInhibited(a) THEN "CrossingDescend" ELSE "Descend" \* Fall back if crossing inhibited ELSE IF sense = "Up" THEN "Climb" ELSE "Descend" \* Issue RA considering multiple threats IssueMultiThreatRA(a) == /\ advisory[a] \in {"None", "TA"} /\ RANotInhibited(a) /\ Cardinality(intruders[a]) > 1 \* Multiple threats /\ \E b \in intruders[a] : RACondition(a, b) /\ LET selectedRA == SelectMultiThreatRA(a) sense == SelectMultiThreatSense(a) IN /\ advisory' = [advisory EXCEPT ![a] = selectedRA] /\ raSense' = [raSense EXCEPT ![a] = sense] /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time] /\ coordinatedSense' = [coordinatedSense EXCEPT ![a] = IF \E b \in intruders[a] : CanCoordinate(a, b) THEN sense ELSE "None"] /\ auralAlert' = [auralAlert EXCEPT ![a] = AuralForRA(selectedRA)] /\ pilotCompliance' = [pilotCompliance EXCEPT ![a] = "NotComplying"] /\ UNCHANGED <> (***************************************************************************) (* RA Timing Constraints (Per DO-185B) *) (***************************************************************************) MIN_RA_DURATION == 5 \* Minimum 5 seconds before changing RA MIN_REVERSAL_DELAY == 5 \* Minimum 5 seconds before reversal MIN_WEAKENING_DELAY == 10 \* Minimum 10 seconds before weakening EXPECTED_PILOT_RESPONSE == 5 \* Expected pilot response time (5 seconds per DO-185B) CLEAR_OF_CONFLICT_DELAY == 5 \* Delay before announcing "Clear of Conflict" (DO-185B) CanModifyRA(a) == time - raIssuedTime[a] >= MIN_RA_DURATION CanReverseRA(a) == time - raIssuedTime[a] >= MIN_REVERSAL_DELAY CanWeakenRA(a) == time - raIssuedTime[a] >= MIN_WEAKENING_DELAY (***************************************************************************) (* Initial State *) (***************************************************************************) Init == /\ altitudeMSL \in [Aircraft -> MinAltitudeMSL..MaxAltitudeMSL] /\ altitudeAGL = [a \in Aircraft |-> altitudeMSL[a] - GroundElevation] /\ verticalRate = [a \in Aircraft |-> 0] /\ horizontalRange = [a \in Aircraft |-> [b \in Aircraft |-> IF a = b THEN 0 ELSE 200]] /\ rangeRate = [a \in Aircraft |-> [b \in Aircraft |-> IF a = b THEN 0 ELSE 0]] /\ verticalSep = [a \in Aircraft |-> [b \in Aircraft |-> altitudeMSL[a] - altitudeMSL[b]]] /\ transponder \in [Aircraft -> TransponderMode] /\ tcasEquipped \in [Aircraft -> TCASLevel] \* TCAS mode: TARA for TCAS II, TAOnly for TCAS I, Standby for None /\ tcasMode = [a \in Aircraft |-> IF tcasEquipped[a] = "TCAS_II" THEN "TARA" ELSE IF tcasEquipped[a] = "TCAS_I" THEN "TAOnly" ELSE "Standby"] /\ sensitivityLvl = [a \in Aircraft |-> SensitivityLevel(altitudeAGL[a])] /\ advisory = [a \in Aircraft |-> "None"] /\ raSense = [a \in Aircraft |-> "None"] /\ raIssuedTime = [a \in Aircraft |-> 0] /\ intruders = [a \in Aircraft |-> {}] /\ auralAlert = [a \in Aircraft |-> "None"] /\ coordinatedSense = [a \in Aircraft |-> "None"] /\ receivedCoord = [a \in Aircraft |-> "None"] /\ pilotCompliance = [a \in Aircraft |-> "NoAdvisory"] /\ time = 0 (***************************************************************************) (* Actions *) (***************************************************************************) \* Update sensitivity level based on current AGL altitude UpdateSensitivityLevel(a) == /\ sensitivityLvl' = [sensitivityLvl EXCEPT ![a] = SensitivityLevel(altitudeAGL[a])] /\ UNCHANGED <> \* Detect and track intruders DetectIntruders(a) == /\ tcasEquipped[a] \in {"TCAS_I", "TCAS_II"} /\ tcasMode[a] # "Standby" /\ intruders' = [intruders EXCEPT ![a] = {b \in Aircraft : TACondition(a, b)}] /\ UNCHANGED <> \* Issue Traffic Advisory IssueTA(a) == /\ advisory[a] = "None" /\ \E b \in Aircraft : TACondition(a, b) /\ ~RACondition(a, b) /\ advisory' = [advisory EXCEPT ![a] = "TA"] /\ auralAlert' = [auralAlert EXCEPT ![a] = "TrafficTraffic"] /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time] \* Track TA issue time for clear delay /\ UNCHANGED <> \* Issue Resolution Advisory IssueRA(a) == /\ advisory[a] \in {"None", "TA"} /\ RANotInhibited(a) /\ \E b \in Aircraft : /\ RACondition(a, b) /\ LET selectedRA == SelectRA(a, b) sense == SelectSense(a, b) IN /\ advisory' = [advisory EXCEPT ![a] = selectedRA] /\ raSense' = [raSense EXCEPT ![a] = sense] /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time] /\ coordinatedSense' = [coordinatedSense EXCEPT ![a] = IF CanCoordinate(a, b) THEN sense ELSE "None"] /\ auralAlert' = [auralAlert EXCEPT ![a] = AuralForRA(selectedRA)] /\ pilotCompliance' = [pilotCompliance EXCEPT ![a] = "NotComplying"] /\ UNCHANGED <> \* Receive coordination from intruder (Mode S) ReceiveCoordination(a, b) == /\ a # b /\ CanCoordinate(a, b) /\ coordinatedSense[b] # "None" /\ receivedCoord[a] = "None" /\ receivedCoord' = [receivedCoord EXCEPT ![a] = coordinatedSense[b]] /\ UNCHANGED <> \* Strengthen RA (increase vertical rate requirement) \* Note: IncreaseClimb has no altitude inhibition, but IncreaseDescend is inhibited below 1550 ft AGL \* Strengthening can occur when: \* 1. Threat has escalated (tau is less than half the threshold), OR \* 2. Pilot hasn't responded after expected response time (v7.1 enhancement) StrengthenRA(a) == /\ advisory[a] \in {"Climb", "Descend"} /\ CanModifyRA(a) /\ \E b \in Aircraft : /\ RACondition(a, b) /\ \/ ModifiedTauRA(a, b) < TAU_RA(sensitivityLvl[a]) \div 2 \* Escalating threat \/ /\ PilotResponseOverdue(a) \* No response yet (v7.1) /\ pilotCompliance[a] = "NotComplying" /\ LET newRA == IF advisory[a] = "Climb" THEN "IncreaseClimb" \* No altitude inhibition for Increase Climb ELSE IF IncreaseDescendNotInhibited(a) THEN "IncreaseDescend" ELSE advisory[a] IN /\ advisory' = [advisory EXCEPT ![a] = newRA] /\ auralAlert' = [auralAlert EXCEPT ![a] = AuralForRA(newRA)] /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time] /\ UNCHANGED <> \* Reverse RA (change sense due to coordination) ReverseRA(a) == /\ advisory[a] \in CorrectiveRA /\ CanReverseRA(a) /\ \E b \in Aircraft : /\ RACondition(a, b) /\ CanCoordinate(a, b) /\ raSense[a] = raSense[b] \* Same sense conflict /\ LET newSense == IF raSense[a] = "Up" THEN "Down" ELSE "Up" newRA == IF newSense = "Up" THEN "ReversalToClimb" ELSE "ReversalToDescend" canReverse == DescendRANotInhibited(a) \/ newSense = "Up" IN IF ~canReverse THEN UNCHANGED <> ELSE /\ advisory' = [advisory EXCEPT ![a] = newRA] /\ raSense' = [raSense EXCEPT ![a] = newSense] /\ auralAlert' = [auralAlert EXCEPT ![a] = AuralForRA(newRA)] /\ coordinatedSense' = [coordinatedSense EXCEPT ![a] = newSense] /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time] /\ UNCHANGED <> \* Reverse RA due to intruder non-compliance (TCAS II v7.1 enhancement) \* This is the key v7.1 improvement: if we detect that the intruder is NOT \* following their RA (e.g., descending when they should climb), we reverse \* our own RA to maintain separation. ReverseRADueToIntruderNonCompliance(a) == /\ advisory[a] \in CorrectiveRA /\ CanReverseRA(a) /\ pilotCompliance[a] = "Complying" \* Own aircraft IS complying /\ \E b \in Aircraft : /\ RACondition(a, b) /\ IntruderDefinitelyNotComplying(a, b) \* Intruder is not responding correctly, so we need to reverse /\ LET newSense == IF raSense[a] = "Up" THEN "Down" ELSE "Up" newRA == IF newSense = "Up" THEN "ReversalToClimb" ELSE "ReversalToDescend" IN IF ~DescendRANotInhibited(a) /\ newSense = "Down" THEN UNCHANGED <> \* Can't reverse to descend near ground ELSE /\ advisory' = [advisory EXCEPT ![a] = newRA] /\ raSense' = [raSense EXCEPT ![a] = newSense] /\ auralAlert' = [auralAlert EXCEPT ![a] = AuralForRA(newRA)] /\ coordinatedSense' = [coordinatedSense EXCEPT ![a] = newSense] /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time] /\ UNCHANGED <> \* Weaken RA (reduce strength as threat diminishes) WeakenRA(a) == /\ advisory[a] \in CorrectiveRA /\ CanWeakenRA(a) /\ \A b \in intruders[a] : PredictedVMD(a, b) >= EffectiveALIM(sensitivityLvl[a], altitudeMSL[a]) * 2 /\ advisory' = [advisory EXCEPT ![a] = "LevelOff"] /\ auralAlert' = [auralAlert EXCEPT ![a] = "LevelOffLevelOff"] /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time] /\ UNCHANGED <> \* Clear advisory when threat resolved \* Per DO-185B: Delay clearing to prevent rapid cycling of advisories ClearAdvisory(a) == /\ advisory[a] # "None" /\ \A b \in Aircraft : ~TACondition(a, b) \* Delay before clearing - must have been active for at least CLEAR_OF_CONFLICT_DELAY /\ time - raIssuedTime[a] >= CLEAR_OF_CONFLICT_DELAY /\ advisory' = [advisory EXCEPT ![a] = "None"] /\ raSense' = [raSense EXCEPT ![a] = "None"] /\ auralAlert' = [auralAlert EXCEPT ![a] = "ClearOfConflict"] /\ coordinatedSense' = [coordinatedSense EXCEPT ![a] = "None"] /\ receivedCoord' = [receivedCoord EXCEPT ![a] = "None"] /\ intruders' = [intruders EXCEPT ![a] = {}] /\ pilotCompliance' = [pilotCompliance EXCEPT ![a] = "NoAdvisory"] /\ UNCHANGED <> \* Environment: Aircraft approach (closing) AircraftApproach(a, b) == /\ a # b /\ horizontalRange[a][b] > 0 /\ horizontalRange' = [horizontalRange EXCEPT ![a][b] = @ - 1, ![b][a] = @ - 1] /\ rangeRate' = [rangeRate EXCEPT ![a][b] = -1, ![b][a] = -1] \* Closing /\ UNCHANGED <> \* Environment: Aircraft diverge (separating) AircraftDiverge(a, b) == /\ a # b /\ horizontalRange[a][b] < 500 \* Don't diverge beyond max range /\ horizontalRange' = [horizontalRange EXCEPT ![a][b] = @ + 1, ![b][a] = @ + 1] /\ rangeRate' = [rangeRate EXCEPT ![a][b] = 1, ![b][a] = 1] \* Opening /\ UNCHANGED <> \* Environment: Aircraft maintain range (parallel flight) AircraftParallel(a, b) == /\ a # b /\ rangeRate[a][b] # 0 \* Currently closing or opening /\ rangeRate' = [rangeRate EXCEPT ![a][b] = 0, ![b][a] = 0] \* Parallel /\ UNCHANGED <> \* Transponder fails TransponderFail(a) == /\ transponder[a] \in {"ModeA", "ModeC", "ModeS"} /\ transponder' = [transponder EXCEPT ![a] = "Failed"] /\ UNCHANGED <> \* Transponder turned off by pilot TransponderOff(a) == /\ transponder[a] \in {"ModeA", "ModeC", "ModeS"} /\ transponder' = [transponder EXCEPT ![a] = "Off"] /\ UNCHANGED <> \* Transponder turned on or reset after failure TransponderOn(a) == /\ transponder[a] \in {"Off", "Failed"} /\ transponder' = [transponder EXCEPT ![a] = "ModeS"] \* Default to Mode S /\ UNCHANGED <> \* Transponder mode degrades (Mode S → Mode C, Mode C → Mode A) TransponderDegrade(a) == /\ \/ /\ transponder[a] = "ModeS" /\ transponder' = [transponder EXCEPT ![a] = "ModeC"] \/ /\ transponder[a] = "ModeC" /\ transponder' = [transponder EXCEPT ![a] = "ModeA"] /\ UNCHANGED <> (***************************************************************************) (* TCAS Mode Switching Actions *) (***************************************************************************) \* Switch TCAS to Standby mode (surveillance only, no advisories) SetTCASStandby(a) == /\ tcasEquipped[a] \in {"TCAS_I", "TCAS_II"} /\ tcasMode[a] # "Standby" /\ tcasMode' = [tcasMode EXCEPT ![a] = "Standby"] \* Clear any active advisories when switching to standby /\ advisory' = [advisory EXCEPT ![a] = "None"] /\ raSense' = [raSense EXCEPT ![a] = "None"] /\ auralAlert' = [auralAlert EXCEPT ![a] = "None"] /\ intruders' = [intruders EXCEPT ![a] = {}] /\ UNCHANGED <> \* Switch TCAS to TA Only mode (traffic advisories only) \* Note: This is the maximum capability for TCAS I equipment SetTCASTAOnly(a) == /\ tcasEquipped[a] \in {"TCAS_I", "TCAS_II"} /\ tcasMode[a] # "TAOnly" /\ tcasMode' = [tcasMode EXCEPT ![a] = "TAOnly"] \* Downgrade any active RA to TA /\ IF advisory[a] \in CorrectiveRA \cup PreventiveRA \cup WeakeningRA THEN /\ advisory' = [advisory EXCEPT ![a] = "TA"] /\ raSense' = [raSense EXCEPT ![a] = "None"] /\ auralAlert' = [auralAlert EXCEPT ![a] = "TrafficTraffic"] ELSE UNCHANGED <> /\ UNCHANGED <> \* Switch TCAS to full TA/RA mode (normal operation) SetTCASTARA(a) == /\ tcasEquipped[a] = "TCAS_II" \* Only TCAS II supports RA /\ tcasMode[a] # "TARA" /\ tcasMode' = [tcasMode EXCEPT ![a] = "TARA"] /\ UNCHANGED <> (***************************************************************************) (* Pilot Actions *) (***************************************************************************) \* Pilot complies with RA by adjusting vertical rate PilotComply(a) == /\ advisory[a] \in CorrectiveRA /\ pilotCompliance[a] = "NotComplying" /\ LET targetRate == CASE advisory[a] \in {"Climb", "CrossingClimb", "ReversalToClimb"} -> 20 [] advisory[a] \in {"Descend", "CrossingDescend", "ReversalToDescend"} -> -20 [] advisory[a] = "IncreaseClimb" -> 25 [] advisory[a] = "IncreaseDescend" -> -25 [] OTHER -> 0 IN verticalRate' = [verticalRate EXCEPT ![a] = targetRate] /\ pilotCompliance' = [pilotCompliance EXCEPT ![a] = "Complying"] /\ UNCHANGED <> \* Pilot ignores RA (models non-compliance for verification) PilotIgnoreRA(a) == /\ advisory[a] \in CorrectiveRA \cup PreventiveRA /\ pilotCompliance[a] = "NotComplying" \* Pilot continues current action (no vertical rate change) /\ UNCHANGED vars \* Pilot complies with preventive RA by limiting vertical rate PilotComplyPreventive(a) == /\ advisory[a] \in PreventiveRA /\ pilotCompliance[a] = "NotComplying" /\ LET limitedRate == CASE advisory[a] = "DontClimb" -> IF verticalRate[a] > 0 THEN 0 ELSE verticalRate[a] [] advisory[a] = "DontDescend" -> IF verticalRate[a] < 0 THEN 0 ELSE verticalRate[a] [] advisory[a] = "LimitClimb500" -> IF verticalRate[a] > 5 THEN 5 ELSE verticalRate[a] [] advisory[a] = "LimitClimb1000" -> IF verticalRate[a] > 10 THEN 10 ELSE verticalRate[a] [] advisory[a] = "LimitClimb2000" -> IF verticalRate[a] > 20 THEN 20 ELSE verticalRate[a] [] advisory[a] = "LimitDescend500" -> IF verticalRate[a] < -5 THEN -5 ELSE verticalRate[a] [] advisory[a] = "LimitDescend1000" -> IF verticalRate[a] < -10 THEN -10 ELSE verticalRate[a] [] advisory[a] = "LimitDescend2000" -> IF verticalRate[a] < -20 THEN -20 ELSE verticalRate[a] [] OTHER -> verticalRate[a] IN verticalRate' = [verticalRate EXCEPT ![a] = limitedRate] /\ pilotCompliance' = [pilotCompliance EXCEPT ![a] = "Complying"] /\ UNCHANGED <> (***************************************************************************) (* Aircraft Movement Actions *) (***************************************************************************) \* Aircraft changes altitude based on vertical rate AircraftMove(a) == /\ LET newAltMSL == altitudeMSL[a] + verticalRate[a] clampedMSL == IF newAltMSL > MaxAltitudeMSL THEN MaxAltitudeMSL ELSE IF newAltMSL < MinAltitudeMSL THEN MinAltitudeMSL ELSE newAltMSL newAltAGL == clampedMSL - GroundElevation IN /\ altitudeMSL' = [altitudeMSL EXCEPT ![a] = clampedMSL] /\ altitudeAGL' = [altitudeAGL EXCEPT ![a] = IF newAltAGL < 0 THEN 0 ELSE newAltAGL] \* Update vertical separation with all other aircraft \* Note: Self-separation (a,a) must always be 0 /\ verticalSep' = [x \in Aircraft |-> [y \in Aircraft |-> IF x = y THEN 0 \* Self-separation is always 0 ELSE IF x = a THEN altitudeMSL'[a] - altitudeMSL[y] ELSE IF y = a THEN altitudeMSL[x] - altitudeMSL'[a] ELSE verticalSep[x][y]]] /\ UNCHANGED <> \* Aircraft changes vertical rate ChangeVerticalRate(a) == /\ \E newRate \in {-30, -20, -10, 0, 10, 20, 30} : /\ newRate # verticalRate[a] /\ verticalRate' = [verticalRate EXCEPT ![a] = newRate] /\ UNCHANGED <> \* Clear aural alert after it has been announced ClearAuralAlert(a) == /\ auralAlert[a] # "None" /\ auralAlert' = [auralAlert EXCEPT ![a] = "None"] /\ UNCHANGED <> \* Time tick Tick == /\ time' = time + 1 /\ UNCHANGED <> (***************************************************************************) (* Next State *) (***************************************************************************) Next == \* TCAS system actions \/ \E a \in Aircraft : UpdateSensitivityLevel(a) \/ \E a \in Aircraft : DetectIntruders(a) \/ \E a \in Aircraft : IssueTA(a) \/ \E a \in Aircraft : IssueRA(a) \/ \E a \in Aircraft : IssueMultiThreatRA(a) \/ \E a, b \in Aircraft : ReceiveCoordination(a, b) \/ \E a \in Aircraft : StrengthenRA(a) \/ \E a \in Aircraft : ReverseRA(a) \/ \E a \in Aircraft : ReverseRADueToIntruderNonCompliance(a) \/ \E a \in Aircraft : WeakenRA(a) \/ \E a \in Aircraft : ClearAdvisory(a) \/ \E a \in Aircraft : ClearAuralAlert(a) \* TCAS mode switching \/ \E a \in Aircraft : SetTCASStandby(a) \/ \E a \in Aircraft : SetTCASTAOnly(a) \/ \E a \in Aircraft : SetTCASTARA(a) \* Pilot actions \/ \E a \in Aircraft : PilotComply(a) \/ \E a \in Aircraft : PilotComplyPreventive(a) \/ \E a \in Aircraft : PilotIgnoreRA(a) \* Aircraft movement \/ \E a \in Aircraft : AircraftMove(a) \/ \E a \in Aircraft : ChangeVerticalRate(a) \/ \E a, b \in Aircraft : AircraftApproach(a, b) \/ \E a, b \in Aircraft : AircraftDiverge(a, b) \/ \E a, b \in Aircraft : AircraftParallel(a, b) \* Transponder actions \/ \E a \in Aircraft : TransponderFail(a) \/ \E a \in Aircraft : TransponderOff(a) \/ \E a \in Aircraft : TransponderOn(a) \/ \E a \in Aircraft : TransponderDegrade(a) \* Time \/ Tick Spec == Init /\ [][Next]_vars (***************************************************************************) (* Fairness Conditions *) (***************************************************************************) \* TCAS must eventually process threats Fairness == /\ \A a \in Aircraft : WF_vars(DetectIntruders(a)) /\ \A a \in Aircraft : WF_vars(IssueTA(a)) /\ \A a \in Aircraft : WF_vars(IssueRA(a)) /\ \A a \in Aircraft : WF_vars(IssueMultiThreatRA(a)) /\ \A a \in Aircraft : WF_vars(ClearAdvisory(a)) /\ \A a \in Aircraft : WF_vars(UpdateSensitivityLevel(a)) FairSpec == Spec /\ Fairness (***************************************************************************) (* Safety Properties *) (***************************************************************************) \* No RA issued below 1000 ft AGL (SL2) NoRABelowSL2 == \A a \in Aircraft : sensitivityLvl[a] = 2 => advisory[a] \in {"None", "TA"} \* No Descend RA below 1100 ft AGL NoDescendRABelowThreshold == \A a \in Aircraft : altitudeAGL[a] < 11 => advisory[a] \notin {"Descend", "IncreaseDescend", "ReversalToDescend"} \* Coordinated RAs have complementary senses CoordinatedRAsComplementary == \A a, b \in Aircraft : /\ a # b /\ advisory[a] \in CorrectiveRA /\ advisory[b] \in CorrectiveRA /\ CanCoordinate(a, b) /\ b \in intruders[a] => raSense[a] # raSense[b] \* RA timing constraints respected RATimingRespected == \A a \in Aircraft : advisory[a] \in {"ReversalToClimb", "ReversalToDescend"} => time - raIssuedTime[a] >= MIN_REVERSAL_DELAY \* No advisory possible without TCAS equipment NoAdvisoryWithoutTCAS == \A a \in Aircraft : tcasEquipped[a] = "None" => advisory[a] = "None" \* No RA possible with only TCAS I NoRAWithTCAS_I == \A a \in Aircraft : tcasEquipped[a] = "TCAS_I" => advisory[a] \in {"None", "TA"} \* TCAS I cannot be in TA/RA mode (only Standby or TAOnly) TCAS_I_ModeConstraint == \A a \in Aircraft : tcasEquipped[a] = "TCAS_I" => tcasMode[a] \in {"Standby", "TAOnly"} \* Multi-threat RAs still maintain complementary senses when possible MultiThreatCoordination == \A a, b \in Aircraft : /\ a # b /\ advisory[a] \in CorrectiveRA /\ advisory[b] \in CorrectiveRA /\ CanCoordinate(a, b) /\ b \in intruders[a] /\ a \in intruders[b] /\ SingleSensePossible(a) /\ SingleSensePossible(b) => raSense[a] # raSense[b] \* Collision avoidance when both aircraft visible (fundamental TCAS guarantee) NoCollisionWhenVisible == \A a, b \in Aircraft : /\ a # b /\ horizontalRange[a][b] = 0 /\ CanSee(a, b) /\ CanSee(b, a) => Abs(verticalSep[a][b]) >= 3 \* 300 ft minimum \* V7.1 Enhancement: System monitors for intruder non-compliance \* If intruder is not complying after expected response time, TCAS should \* be able to detect this (IntruderDefinitelyNotComplying will be true) IntruderNonComplianceDetectable == \A a, b \in Aircraft : /\ a # b /\ advisory[a] \in CorrectiveRA /\ advisory[b] \in CorrectiveRA /\ CanCoordinate(a, b) /\ receivedCoord[a] # "None" /\ pilotCompliance[a] = "Complying" /\ pilotCompliance[b] = "NotComplying" /\ time - raIssuedTime[b] >= EXPECTED_PILOT_RESPONSE => IntruderNotComplying(a, b) \* TCAS mode constraints NoRAInTAOnlyMode == \A a \in Aircraft : tcasMode[a] = "TAOnly" => advisory[a] \notin (CorrectiveRA \cup PreventiveRA \cup WeakeningRA) NoAdvisoryInStandbyMode == \A a \in Aircraft : tcasMode[a] = "Standby" => advisory[a] = "None" \* FL420 threshold constraints FL420ThresholdsUsed == \A a \in Aircraft : IsAboveFL420(altitudeMSL[a]) => EffectiveALIM(sensitivityLvl[a], altitudeMSL[a]) = ALIM_FL420 \* Crossing RA issued when needed CrossingRAWhenAppropriate == \A a \in Aircraft : advisory[a] \in {"CrossingClimb", "CrossingDescend"} => \E b \in intruders[a] : NeedsCrossingRA(a, b) \* Aural alert corresponds to advisory AuralMatchesAdvisory == \A a \in Aircraft : advisory[a] \in CorrectiveRA \cup PreventiveRA => auralAlert[a] \in AuralType \ {"None", "ClearOfConflict"} (***************************************************************************) (* Liveness Properties *) (***************************************************************************) \* If there's a threat, eventually an advisory is issued EventualAdvisory == \A a, b \in Aircraft : (TACondition(a, b)) ~> (advisory[a] # "None") \* If RA is issued, pilot eventually complies (or advisory is cleared) \* Note: Non-compliance is also modeled (PilotIgnoreRA), so we check for \* either compliance OR advisory resolution EventualResponse == \A a \in Aircraft : (advisory[a] \in CorrectiveRA) ~> (pilotCompliance[a] = "Complying" \/ advisory[a] = "None") \* Threats are eventually resolved EventualResolution == \A a \in Aircraft : (advisory[a] # "None") ~> (advisory[a] = "None") ============================================================================= ``` ## Key Safety Properties The specification verifies several critical invariants: ### NoRABelowSL2 No Resolution Advisory can be issued when an aircraft is below 1000 ft AGL (Sensitivity Level 2). At this altitude, pilots need to focus on landing/takeoff and shouldn't be distracted by TCAS maneuvers. ### NoDescendRABelowThreshold Descend RAs are inhibited below 1100 ft AGL to prevent TCAS from commanding descent into terrain. ### CoordinatedRAsComplementary When two TCAS II-equipped aircraft coordinate, their RAs must have complementary senses—if one climbs, the other descends. This prevents both aircraft from maneuvering in the same direction. ### IntruderNonComplianceDetectable The v7.1 enhancement: if the intruder isn't following their RA after the expected pilot response time (5 seconds), the system detects this and can trigger a reversal for the compliant aircraft. ## Model Checking Configuration To run this specification, create a configuration file: ```tla theme={null} CONSTANTS Aircraft = {a1, a2} MaxAltitudeMSL = 500 MinAltitudeMSL = 0 GroundElevation = 0 INIT Init NEXT Next INVARIANTS TypeOK NoRABelowSL2 NoDescendRABelowThreshold CoordinatedRAsComplementary NoAdvisoryWithoutTCAS PROPERTIES EventualAdvisory EventualResolution ``` The state space grows quickly with more aircraft. For practical model checking, 2-3 aircraft with bounded altitude ranges work well(ish)