GOAL STRUCTURING NOTATION (GSN) SAFETY CASE

Formal safety argument structure per MIL-STD-882E / DO-178C methodology

TLA+ FORMAL SPECIFICATION — AUTHORITY FSM

Model-checkable specification. Properties verifiable with TLC model checker.

STATE SPACE

-- Authority FSM state vector
level ∈ {0, 1, 2, 3}     -- 0=A3, 1=A2, 2=A1, 3=A0
dwellCounter ∈ ℕ       -- ticks at current level meeting upgrade conditions
locked ∈ {TRUE, FALSE}  -- oscillation lockout active
lockExpiry ∈ ℕ         -- tick at which lockout expires
transitionCount ∈ ℕ    -- transitions in current window

TRANSITION GUARDS

Downgrade(trust, anomCnt) ≜
  target := IF trust < 0.25 ∨ anomCnt ≥ 3 THEN A0
            ELSE IF trust < 0.50 ∨ anomCnt ≥ 2 THEN A1
            ELSE IF trust < 0.80 THEN A2 ELSE A3
  ∧ target > level   -- only if more restrictive
  ∧ ¬locked
  ∧ level' = target   -- CAN SKIP LEVELS
  ∧ dwellCounter' = 0

Upgrade(trust, anomCnt, level, dwell) ≜
  ∧ level > 0 ∧ anomCnt = 0 ∧ ¬locked
  ∧ trust ≥ UpgradeThreshold[level]   -- hysteresis: UP > DOWN
  ∧ dwell ≥ DwellTime[level]   -- temporal guard
  ∧ level' = level - 1   -- EXACTLY ONE STEP
  ∧ dwellCounter' = 0

VERIFIED PROPERTIES

TLA+ MODULE (DOWNLOADABLE)

Full specification available for TLC model checking. State space: |level|×|trust|×|anomaly|×|locked|×|dwell| = 4×101×7×2×N

TLC MODEL CHECKING RESULTS

Configuration: MaxTick=50, MaxDwell=120, OscMaxTransitions=3, OscLockoutTicks=20