Formální ověřování bezpečnosti kritického řídicího softwaru UAV

Formální ověřování bezpečnosti řídicího softwaru

Formální ověřování bezpečnosti řídicího softwaru pro bezpilotní letouny (UAV) představuje systematický a matematicky podložený přístup k dokazování, že implementace splňuje specifikované bezpečnostní vlastnosti za všech relevantních provozních podmínek. V prostředí rostoucí autonomie, integrace do řízeného vzdušného prostoru a heterogenních senzorických řetězců je formální ověření jedním z mála nástrojů, které dokážou prokazatelně snížit reziduální riziko a podpořit certifikaci podle leteckých norem.

Regulační kontext a normy

DO-178C/ED-12C: rámec pro vývoj leteckého softwaru. Pro nejkritičtější úrovně (A/B) vyžaduje formální prokázání úplnosti a konzistence požadavků, trasovatelnost a důkaz o absenci tříd chyb.
DO-333 (Formal Methods Supplement): definuje, jak lze použít formální metody k naplnění cílů DO-178C (náhrada/posílení testování, dokazování vlastností, snižování důkazního dluhu).
ARP4754A/ARP4761A: systémové a bezpečnostní procesy (FHA, FTA, FMEA, SSA), které generují bezpečnostní požadavky pro software a vstupy do formálních specifikací.
ISO 26262/IEC 61508: i když nejsou letecké, poskytují pro UAV doplňkovou metodiku k zvládání funkční bezpečnosti a systematických chyb.

Pojmy a typy bezpečnostních vlastností

Invarianta (safety): „nic špatného se nikdy nestane“ (např. nikdy nepřekročit maximální náklon, nikdy nezablokovat řídicí smyčku ve stavu bez zásahu).
Životaschopnost (liveness): „něco dobrého se dříve či později stane“ (např. návrat do bezpečného režimu do T sekund po ztrátě GPS).
Časované a hybridní vlastnosti: vztahují se na čas a spojité dynamiky (např. do 200 ms musí být aktualizován momentový příkaz; nediagnostikovaná saturace nesmí trvat > 3 periody).
Pravděpodobnostní vlastnosti: „pravděpodobnost porušení výškového koridoru < 10⁻⁹/letovou hodinu“.

Metody formálního ověřování

Model checking (MC)
- Diskrétní MC (např. SPIN/Promela, nuXmv): verifikace temporálních logik LTL/CTL nad stavovým prostorem konečného modelu.
- Časovaný MC (UPPAAL): modely časovaných automatů pro plánování, watchdogy, deadline v RTOS.
- Pravděpodobnostní MC (PRISM, STORM): DTMC/MDP pro vlastnosti s pravděpodobnostními garancemi.
- CEGAR (Counterexample-Guided Abstraction Refinement): iterativní zpřesňování abstrakcí.
Důkazové asistenty (theorem proving)
- TLA+, Coq, Isabelle/HOL, HOL4 – konstrukce formálních specifikací a důkazů korektnosti algoritmů (např. konsenzus v distribuovaných uzlech, bezpečné přepínání módů).
Abstraktní interpretace a statická analýza
- Frama-C, Astrée, Polyspace, Infer: důkaz nepřítomnosti přetečení, dělení nulou, data races, porušení MISRA C.
Korektnost podle kontraktů (Design by Contract)
- ACSL/Frama-C, SPARK/Ada: dokazování pre-/post-podmínek a invariantů smyček.
Formálně ověřený RTOS/mikrojádro
- seL4: formální důkazy korektnosti jádra minimalizují TCB a zjednodušují argumentaci bezpečnosti aplikace.
Runtime verification (RV)
- Monitorování logiky (LTLf/MTL) za běhu, sentinelové automaty, kontrakty mezi komponentami; vhodné pro detekci odchylek a nouzové strategie.

Modelování řídicích smyček a hybridních systémů

UAV řízení sestává z diskrétních módů (ARMED, TAKEOFF, MISSION, RTL, FAILSAFE) a spojitých dynamik (stavová zpětná vazba). Vhodnou formalizací je hybridní automat s:

lokálními invarianty pro módy (např. rychlost stoupání ≤ v_max),
přechody s guardy (např. gps_loss ∧ t > 2 s ⇒ MISSION → RTL),
flow definicemi (lineární/afinní aproximace spojitého modelu).

Při časově kritických smyčkách (rate-monotonic scheduling, fixed-priority) je vhodná analýza schedulability (RTA) a model checking nad časovanými automaty.

Formální specifikování požadavků

Temporální šablony: běžné vzory bezpečnostních vlastností (Response, Precedence, Invariance, Absence) přeložitelné do LTL/MTL.
Kontrakty: komponentové Assume-Guarantee specifikace pro autopilota, navigaci, komunikaci a payload.
Časová rozšíření: MTL, TCTL a Signal Temporal Logic (STL) pro vlastnosti nad kontinuálními signály (např. |roll| < 35° vždy, nebo eventually altitude within ±1 m během 3 s).

Proces a životní cyklus s formálními důkazy

Bezpečnostní analýza systému: FHA → odvození Top-Level Aircraft Safety Requirements (TLSR); STPA identifikuje nebezpečné řídicí akce.
Formální specifikace: transformace TLSR → SW bezpečnostní požadavky (SWSR) v kontraktech/logikách.
Architektura a alokace: mapování SWSR na komponenty (FCU, Navigator, Estimator, Actuation, Health-Mgr).
Modelování: stavové diagramy, hybridní automaty, kontrakty; tvorba abstrakcí pro MC/TP.
Ověření: model checking/důkazy; CEGAR; validace předpokladů prostředí (senzorické chyby, zpoždění, ztráty linky).
Generování důkazních artefaktů: důkazové skripty, certifikáty, souhrnné reporty a trasovatelnost k požadavkům.
Integrace s testováním: formální metody nahrazují nebo snižují rozsah některých testů (podle DO-333), ale MC/DC a HIL/SITL zůstávají klíčové.
Provozní monitorování: RV a health-monitoring pro detekci odchylek mimo modelované předpoklady.

Ověřování bezpečnostních módů (failsafe) a návratových strategií

Ztráta GPS → RTL/ALT HOLD: dokázat, že přechod nastane do T a že výškový profil neporuší minima/maxima.
Nízká baterie: důkaz, že spotřeba energie při aktuálním profilu letu umožní bezpečné dosednutí nebo návrat s pravděpodobností ≥ p.
Ztráta spojení: vlastnosti „no-flyaway“ (max. horizontální drift < D) a aktivace geofencingových omezení.

Ověření percepce a fúze senzorů

Ačkoliv formální důkazy nad neuronovými sítěmi jsou stále omezené, lze:

získat robustness margins (lokální Lipschitzovskou robustnost) pro malé perturbace vstupů,
obalit ML komponent kontraktem (confidence bounds, fallback),
formálně ověřit následné rozhodování tak, aby porucha percepce vedla nejpozději k bezpečnému módu.

Integrace s modelově orientovaným návrhem (MBD)

Modely v Simulink/Stateflow: generování kódu s omezeným podmnožinou a následné ověřování kontraktů (např. s Frama-C/ACSL).
Sémantická omezení: zákaz dynamické alokace, rekurze, nedefinovaného chování; MISRA C/C++.
Ko-simulace HIL/SIL: validace předpokladů prostředí, které vstupovaly do formálních důkazů.

Výkonnostní a plánovací garance

Bezpečnost úzce souvisí s načasováním. Je třeba:

prokázat schedulability (RTA) pro pevně prioritní úlohy (PID/MPPI smyčky, estimator, navigator),
ověřit vlastnosti typu „deadline meet“ v UPPAAL,
doložit nejhorší čas vykonání (WCET) klíčových rutin (např. s aiT),
zahrnout jitter a přenosová zpoždění do kontraktů mezi vlákny.

Architektonické vzory snižující důkazní zátěž

Separační architektura: mikrojádro, izolace domén (safety vs. mission).
Command governor: saturace a omezení garantované projekcí příkazů na bezpečnou množinu.
Simplex/Runtime Assurance: dvojice advanced vs. safe controller s formálně ověřeným přepínáním.
Redundance a monitorování: N-modulární redundance, diverzita algoritmů (EKF vs. UKF).

Škálování a zvládání stavové exploze

kompoziční důkazy (Assume-Guarantee),
abstrakce (predikátové, časové, kvantizační),
symbolické metody (BDDs, SMT-solvery jako Z3/CVC5),
redukce částečného pořadí pro souběžnost,
oddělení bezpečnostního jádra s malým TCB.

Datové typy, numerika a přenos do implementace

výběr reprezentace (fix-point vs. float) a důkaz nepřítomnosti přetečení/NaN,
konzervativní zaokrouhlovací chyby v řízení (intervalová aritmetika),
kontrakty pro konverze mezi rámci (NED/ENU/Body) a jednotkami (SI, uzly, ft),
kontrola nedefinovaného chování v C (aliasing, UB dle C11).

Praktický postup (roadmapa) pro tým UAV

Definujte bezpečnostní cíle z FHA/STPA a přiřaďte kritičnost (A–E).
Vyberte metodu: MC pro diskrétní protokoly a módy, UPPAAL pro čas, Frama-C/ACSL pro kódové kontrakty, TLA+/Isabelle pro algoritmy.
Nastavte standardy kódu (MISRA, banned patterns) a nástroje statické analýzy v CI.
Modelujte kontrakty komponent a jejich rozhraní (assume–guarantee) včetně časování.
Automatizujte verifikaci (CI pipeline): spouštějte MC, důkazy, statickou analýzu a generujte reporty s trasovatelností.
Validujte předpoklady experimentem (SIL/HIL/flight-test) a zpětnovazebně upravujte modely.
Vytvořte Safety Case (Goal Structuring Notation): propojte cíle – důkazy – artefakty – testy.

Měřitelné ukazatele (kvalita a pokrytí)

pokrytí kontraktů (počet splněných vs. otevřených důkazů),
úplnost vlastností vůči rizikům (mapování STPA → formální vlastnosti),
snížení nákladů na testování (nahrazené testy dle DO-333),
defektová hustota v kódu po nasazení FM,
čas uzavření CEGAR smyček (počet iterací na důkaz).

Limity, rizika a antipatterny

Nesprávně specifikované prostředí: důkaz je irelevantní, pokud předpoklady (např. rozsah větru, latence GNSS) neodpovídají realitě.
Přemíra abstrakce: ztráta kritických interakcí (např. saturace aktorů) → falešné „doklady“ bezpečnosti.
Nekontrolovatelná složitost: monolitické modely; řešením je modularita a kontrakty.
Neodpovídající model-kód: generovaný vs. ručně psaný kód bez formálních vazeb.

Příkladové scénáře vlastností

Invarianta geofencingu: „Vždy platí, že (lat, lon) ∈ povolený polygon ∨ mód = RTL ∨ mód = LAND.“
Časovaná odezva: „Pokud imu_fault, pak do 100 ms přepnout na redundantní IMU nebo přejít do ALT HOLD.“
Absence deadlocku v plánovači: „V každém stavu existuje povolený přechod.“
Pravděpodobnostní bezpečnost: „P<10⁻⁹ [porušení výšky > 20 m nad max] během 1 h letu.“