Formálne overovanie UAV softvéru

Formálne overovanie bezpečnosti riadiaceho softvéru

Formálne overovanie bezpečnosti riadiaceho softvéru pre bezpilotné lietadlá (UAV) predstavuje systematický a matematicky podložený prístup k dokazovaniu, že implementácia spĺňa špecifikované bezpečnostné vlastnosti za všetkých relevantných prevádzkových podmienok. V prostredí zvyšujúcej sa autonómie, integrácie do kontrolovaného vzdušného priestoru a heterogénnych senzorických reťazcov je formálne overenie jedným z mála nástrojov, ktoré dokážu preukázateľne znížiť reziduálne riziko a podporiť certifikáciu podľa leteckých noriem.

Regulačný kontext a normy

• DO-178C/ED-12C: rámec pre vývoj leteckého softvéru. Pre najkritickejšie úrovne (A/B) vyžaduje formálne preukázanie úplnosti a konzistencie požiadaviek, trasovateľnosť a dôkaz o absencii tried chýb.
• DO-333 (Formal Methods Supplement): definuje, ako možno použiť formálne metódy na splnenie cieľov DO-178C (náhrada/posilnenie testovania, dokazovanie vlastností, znižovanie dôkazného dlhu).
• ARP4754A/ARP4761A: systémové a bezpečnostné procesy (FHA, FTA, FMEA, SSA), ktoré generujú bezpečnostné požiadavky pre softvér a vstupy do formálnych špecifikácií.
• ISO 26262/IEC 61508: hoci nie letecké, poskytujú pre UAV doplnkovú metodiku na zvládanie funkčnej bezpečnosti a systematických chýb.

Pojmy a typy bezpečnostných vlastností

• Invarianta (safety): „nič zlé sa nikdy nestane“ (napr. nikdy neprekročiť maximálny náklon, nikdy nezamknúť riadiacu slučku v stave bez zásahu).
• Živosť (liveness): „niečo dobré sa skôr či neskôr stane“ (napr. návrat do bezpečného režimu do T sekúnd po strate GPS).
• Časované a hybridné vlastnosti: viažu sa na čas a spojité dynamiky (napr. do 200 ms sa musí aktualizovať momentový príkaz; nediagnostikovaná saturácia nesmie trvať > 3 periódy).
• Pravdepodobnostné vlastnosti: „pravdepodobnosť porušenia výškového koridoru < 10⁻⁹/letovú hodinu“.

Metódy formálneho overovania

1. Model checking (MC)
   • Diskrétny MC (napr. SPIN/Promela, nuXmv): verifikácia temporálnych logík LTL/CTL nad stavovým priestorom konečného modelu.
   • Časovaný MC (UPPAAL): modely časovaných automatov pre plánovanie, watchdog-y, deadlines v RTOS.
   • Pravdepodobnostný MC (PRISM, STORM): DTMC/MDP pre vlastnosti s pravdepodobnostnými garanciami.
   • CEGAR (Counterexample-Guided Abstraction Refinement): iteratívne spresňovanie abstrakcií.
2. Dôkazové asistenty (theorem proving)
   • TLA+, Coq, Isabelle/HOL, HOL4 – konštrukcia formálnych špecifikácií a dôkazov korektnosti algoritmov (napr. konsenzus v distribuovaných uzloch, bezpečné prepínanie módov).
3. Abstraktná interpretácia a statická analýza
   • Frama-C, Astrée, Polyspace, Infer: dôkaz neprítomnosti pretečenia, delenia nulou, data races, porušenia MISRA C.
4. Korektnosť podľa kontraktov (Design by Contract)
   • ACSL/Frama-C, SPARK/Ada: dokazovanie pred-/post-podmienok a invariantov slučiek.
5. Formálne overený RTOS/mikrojadro
   • seL4: formálne dôkazy korektnosti jadra minimalizujú TCB a zjednodušujú argumentáciu bezpečnosti aplikácie.
6. Runtime verification (RV)
   • Monitorovanie logiky (LTLf/MTL) za behu, sentinelové automaty, kontrakty medzi komponentmi; vhodné pre detekciu odchýlok a núdzové stratégie.

Modelovanie riadiacich slučiek a hybridných systémov

UAV riadenie pozostáva z diskrétnych módov (ARMED, TAKEOFF, MISSION, RTL, FAILSAFE) a spojitých dynamík (stavová spätná väzba). Vhodnou formalizáciou je hybridný automat s:

• lokálnymi invariantmi pre módy (napr. rýchlosť stúpania ≤ v_max),
• prechodmi s guardami (napr. gps_loss ∧ t > 2 s ⇒ MISSION → RTL),
• flow definíciami (lineárne/afinné aproximácie spojitého modelu).

Pri časovo kritických slučkách (rate-monotonic scheduling, fixed-priority) je vhodná analýza schedulability (RTA) a model checking nad časovanými automatmi.

Formálne špecifikovanie požiadaviek

• Temporálne šablóny: bežné vzory bezpečnostných vlastností (Response, Precedence, Invariance, Absence) prekladateľné do LTL/MTL.
• Kontrakty: komponentové Assume-Guarantee špecifikácie pre autopilot, navigáciu, komunikáciu a payload.
• Časové rozšírenia: MTL, TCTL a Signal Temporal Logic (STL) pre vlastnosti nad kontinuálnymi signálmi (napr. |roll| < 35° vždy, alebo eventually altitude within ±1 m počas 3 s).

Proces a životný cyklus s formálnymi dôkazmi

1. Bezpečnostná analýza systému: FHA → odvodenie Top-Level Aircraft Safety Requirements (TLSR); STPA identifikuje nebezpečné riadiace akcie.
2. Formálna špecifikácia: transformácia TLSR → SW bezpečnostné požiadavky (SWSR) v kontraktoch/logikách.
3. Architektúra a alokácia: mapovanie SWSR na komponenty (FCU, Navigator, Estimator, Actuation, Health-Mgr).
4. Modelovanie: stavové diagramy, hybridné automaty, kontrakty; tvorba abstrakcií pre MC/TP.
5. Overenie: model checking/dôkazy; CEGAR; validácia predpokladov prostredia (senzorické chyby, oneskorenia, straty linky).
6. Generovanie dôkazných artefaktov: dôkazové skripty, certifikáty, summary reporty a trasovateľnosť do požiadaviek.
7. Integrácia s testovaním: formálne metódy nahrádzajú alebo znižujú rozsah niektorých testov (per DO-333), no MC/DC a HIL/SITL ostávajú kľúčové.
8. Prevádzkové monitorovanie: RV a health-monitoring na detekciu odchýlok mimo modelovaných predpokladov.

Overovanie bezpečnostných módov (failsafe) a návratových stratégií

• Loss of GPS → RTL/ALT HOLD: dokázať, že prechod nastane do T a že výškový profil neporuší minimá/maximum.
• Battery low: dôkaz, že spotreba energie pri aktuálnom profile letu umožní bezpečné dosadnutie alebo návrat s pravdepodobnosťou ≥ p.
• Link loss: vlastnosti „no-flyaway“ (max. horizontálny drift < D) a aktivácia geofencing obmedzení.

Overenie percepcie a fúzie senzorov

Aj keď formálne dôkazy nad neurónovými sieťami sú stále limitované, možno:

• získať robustness margins (lokálna Lipschitzovská robustnosť) pre malé perturbácie vstupov,
• obaliť ML komponent kontraktom (confidence bounds, fallback),
• formálne overiť nadväzujúce rozhodovanie tak, aby porucha percepcie viedla najneskôr k bezpečnému módu.

Integrácia s modelovo-orientovaným návrhom (MBD)

• Modely v Simulink/Stateflow: generovanie kódu s obmedzeným subsetom a následné verifikovanie kontraktov (napr. s Frama-C/ACSL).
• Sémantické obmedzenia: zákaz dynamickej alokácie, rekurzie, nedefinovaného správania; MISRA C/C++.
• Ko-simulácia HIL/SIL: validácia predpokladov prostredia, ktoré vstupovali do formálnych dôkazov.

Výkonnostné a plánovacie garancie

Bezpečnosť úzko súvisí s načasovaním. Potrebné je:

• preukázať schedulability (RTA) pre pevne prioritné úlohy (PID/MPPI slučky, estimator, navigator),
• overiť vlastnosti typu „deadline meet“ v UPPAAL,
• doložiť najhorší čas vykonania (WCET) kľúčových rutin (napr. s aiT),
• zahrnúť jitter a prenosové oneskorenia do kontraktov medzi vláknami.

Architektúrne vzory znižujúce dôkazové bremeno

• Separačná architektúra: mikro-jadro, izolácia domén (safety vs. mission).
• Command governor: saturácie a obmedzenia garantované projekciou príkazov na bezpečnú množinu.
• Simplex/Runtime Assurance: dvojica advanced vs. safe controller s formálne overeným prepínaním.
• Redundancia a monitorovanie: N-modulárna redundancia, diversita algoritmov (EKF vs. UKF).

Škálovanie a zvládanie stavovej explózie

• kompozičné dôkazy (Assume-Guarantee),
• abstrakcie (predikátové, časové, kvantizačné),
• symbolické metódy (BDDs, SMT-solvery ako Z3/CVC5),
• redukcie čiastočného poradia pre súbežnosť,
• oddelenie bezpečnostného jadra s malým TCB.

Dátové typy, numerika a prenos do implementácie

• výber reprezentácie (fix-point vs. float) a dôkaz neprítomnosti pretečenia/NaN,
• konzervatívne zaokrúhľovacie chyby v riadení (intervalová aritmetika),
• kontrakty pre konverzie medzi rámcami (NED/ENU/Body) a jednotkami (SI, knots, ft),
• kontrola nedefinovaného správania C (aliasing, UB podľa C11).

Praktický postup (roadmapa) pre tím UAV

1. Definujte bezpečnostné ciele z FHA/STPA a priraďte kritickosť (A–E).
2. Vyberte metódu: MC pre diskrétne protokoly a módy, UPPAAL pre čas, Frama-C/ACSL pre kódové kontrakty, TLA+/Isabelle pre algoritmy.
3. Nastavte štandardy kódu (MISRA, banned patterns) a nástroje statickej analýzy v CI.
4. Modelujte kontrakty komponentov a ich rozhrania (assume–guarantee) vrátane časovania.
5. Automatizujte verifikáciu (CI pipeline): spúšťajte MC, dôkazy, statickú analýzu a generujte reporty s trasovateľnosťou.
6. Validujte predpoklady experimentom (SIL/HIL/flight-test) a spätnoväzbovo upravujte modely.
7. Vytvorte Safety Case (Goal Structuring Notation): prepojte ciele – dôkazy – artefakty – testy.

Merateľné ukazovatele (kvalita a pokrytie)

• pokrytie kontraktov (počet splnených vs. otvorených dôkazov),
• úplnosť vlastností voči rizikám (mapovanie STPA → formálne vlastnosti),
• zníženie nákladov na testovanie (nahradené testy podľa DO-333),
• defektová hustota v kóde po nasadení FM,
• čas uzatvorenia CEGAR slučiek (počet iterácií na dôkaz).

Limity, riziká a antipatery

• Nesprávne špecifikované prostredie: dôkaz je irelevantný, ak predpoklady (napr. rozsah vetra, latencie GNSS) nezodpovedajú realite.
• Over-abstrakcia: strata kritických interakcií (napr. saturácia aktuátorov) → falošné „dôkazy“ bezpečnosti.
• Nezvládnuteľná zložitosť: monolitické modely; riešením je modularita a kontrakty.
• Nesúlad model-kód: generovaný vs. ručne písaný kód bez formálnych väzieb.

Príkladové scenáre vlastností

• Invarianta geofencingu: „Vždy platí, že (lat, lon) ∈ povolený polygón ∨ mód = RTL ∨ mód = LAND.“
• Časovaná odozva: „Ak imu_fault, potom do 100 ms prepnúť na redundantné IMU alebo prejsť do ALT HOLD.“
• Absencia deadlocku v plánovači: „V každom stave existuje povolený prechod.“
• Pravdepodobnostná bezpečnosť: „P<10⁻⁹ [porušenie výšky > 20 m nad max] počas 1 h letu.“

Nástrojový ekosystém (ilustratívny)

Integrácia do CI/CD a evidenčné artefakty

• Automatizované spúšťanie MC/TP/SA pri každom merge.
• Export trasovateľnosti: požiadavka → vlastnosť → dôkaz → test → commit.
• Archivácia dôkazných skriptov a verzií modelov (reproducibilita).
• Generovanie Safety Case v GSN s odkazmi na konkrétne artefakty.

Case study (schematicky)

Autopilot pre multikoptéru: Kontrakty pre Attitude Controller zahŕňajú obmedzenia momentov a saturácie. UPPAAL modeluje úlohy 1 kHz (IMU/attitude) a 100 Hz (position). Overená vlastnosť: „Žiadna úloha neprekročí deadline pri najhorších interferenciách“ a „prepnutie do SAFE do 150 ms po estimator fault“. Frama-C dokazuje absenciu pretečenia pri pevnej bodovej aritmetike. RV monitor v letovom kontroléri sleduje STL vlastnosti signálov počas letu a pri porušení aktivuje Simplex prepnutie.

Odporúčané praktiky

• Píšte požiadavky „verifikovateľne“ (jednoznačné, merateľné, s toleranciami a hysteréziou).
• Uprednostňujte jednoduchosť riadiacej architektúry, ktorá sa dá dokázať.
• Udržujte malé, stabilné TCB (bezpečnostné jadro, fail-safe logika).
• Dokumentujte predpoklady prostredia a neustále ich konfrontujte s letovými dátami.
• Investujte do knižníc overených komponentov (časovače, FIFO, filtre) s opakovane použiteľnými dôkazmi.

Formálne overovanie neznamená len „prejsť nástrojom“, ale vytvoriť disciplinovaný vývojový ekosystém, v ktorom sú bezpečnostné vlastnosti explicitne špecifikované, modulárne dokázané a kontinuálne monitorované v prevádzke. Správnou kombináciou model checking-u, dôkazových asistentov, statickej analýzy, kontraktov a runtime verifikácie možno dosiahnuť výrazné zníženie rizika a urýchliť cestu k certifikácii bezpečného riadiaceho softvéru UAV.