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.
Scope of the state count reported by the model checker below: 23,748 reachable states of the discrete authority automaton, under the assumption that instantaneous authority equals its target. Continuous behaviour between decision instants is not covered, and the result is a specification-level property of the model rather than a claim about fielded hardware.
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