Formele verificatie voor veiligheidskritische defensiesoftware

Door Corvus Intelligence Engineering Team · Over het team →

24 juni 2026 13 min lezen

Een softwaredefect in een commerciële applicatie kost het bedrijf geld en veroorzaakt ongemak voor gebruikers. Een softwaredefect in een wapensysteem voor vuurbeheersing, een vliegtuig-vliegbeheersysteem of een component van een nucleaire commandoautoriteit kan onomkeerbare fysieke schade veroorzaken. De asymmetrie van de gevolgen is zo extreem dat de standaardbenadering van softwarekwaliteit — code schrijven, testen uitvoeren, door tests gevonden fouten oplossen — ontoereikend is. Testen kan de aanwezigheid van defecten aantonen; het kan hun afwezigheid niet aantonen. Voor de meest veiligheidskritische defensiesoftware heeft de ingenieurswereld op deze beperking gereageerd met formele verificatie: wiskundig rigoureuze technieken die bewijzen dat het softwaregedrag correct is door constructie, niet slechts door steekproeven.

Dit artikel is een praktische technische referentie voor het toepassen van formele methoden op veiligheidskritische defensiesoftware. Het behandelt het regelgevingskader dat formele verificatie op de hoogste kritikaliteitsniveaus verplicht stelt, de voornaamste tools en technieken (TLA+, SPARK Ada, CBMC, Frama-C), de specifieke uitdaging van protocolverificatie via modelcontrole, en de integratie van formele artefacten in DO-178C-nalevingsbewijzen. Het sluit af met een kosten-batenanalyse die programmamanagers een kader biedt om te beslissen wanneer formele verificatie de overhead waard is — en wanneer het simpelweg vereist is.

Wanneer formele verificatie vereist is in defensiesoftware

Het mandaat voor formele verificatie in defensiesoftware ontstaat op het snijpunt van twee regelgevingskaders: de systeemveiligheidsnorm MIL-STD-882E, die gevaren classificeert op gevolgsernst en waarschijnlijkheid, en de softwareontwikkelingsnormen die deze classificaties vertalen naar softwaretechnische verplichtingen.

MIL-STD-882E kent elke softwarefunctie een Software Criticality Index (SCI) toe op basis van het product van gevolgsernst (Catastrofaal — verlies van leven of systeem; Kritisch — ernstig letsel of grote systeemschade; Marginaal — klein letsel of systeemschade; Verwaarloosbaar) en waarschijnlijkheid. Functies beoordeeld als Catastrofaal ontvangen SCI Categorie I ongeacht de waarschijnlijkheid, omdat geen enkele kans om een catastrofaal resultaat te veroorzaken door technische nalatigheid aanvaardbaar is. Categorie I-functies moeten worden onderworpen aan de meest rigoureuze beschikbare softwareveiligheidsanalysetechnieken — wat vandaag de dag formele analyse betekent.

Voor luchtvaart- en luchtvaartgerelateerde wapensystemen (raketten, geleide munitie met vluchtsoftware) is de certificeringsnorm DO-178C. DO-178C definieert vijf Design Assurance Levels (DAL A tot E), waarbij Level A is gereserveerd voor software waarvan het falen een catastrofale faaltoestand kan veroorzaken of bijdragen. Level A legt 66 softwareontwikkeling- en verificatiedoelstellingen op, waaronder:

100% Modified Condition/Decision Coverage (MC/DC) — elk onafhankelijk effect van een voorwaarde op een beslissing moet worden aangetoond
Onafhankelijkheid van verificatieactiviteiten ten opzichte van ontwikkelingsactiviteiten
Toolkwalificatie onder DO-330 voor elke tool die wordt gebruikt om vereiste verificatieactiviteiten te elimineren
Formele analyse (via DO-333-supplement) als alternatief nalevingsmiddel voor structurele dekkingsdoelstellingen

Het DO-333-supplement op DO-178C behandelt formele methoden expliciet als middel om verificatiedoelstellingen te voldoen. Wanneer een programma formele verificatie toepast met DO-333, moet het een Formal Methods Plan produceren dat de gekozen formalisme beschrijft, de geverifieerde eigenschappen, de gebruikte tools, en hoe formeel verificatiebewijs wordt gekoppeld aan DO-178C Tabellen A-3 tot A-7 doelstellingen.

Voor grondvoertuigen en maritieme wapensystemen die niet onder DO-178C vallen, loopt het analoge pad via MIL-STD-882E Categorie I-vereisten naar programmaspecifieke Softwareontwikkelingsplannen die steeds vaker formele analysetechnieken als bewijs van strengheid proportioneel aan gevolgsernst noemen. De missiekritische softwarearchitectuur-beslissingen die bepalen welke componenten Categorie I of DAL A bereiken, moeten vroeg in het systeemontwerp worden genomen — ze zijn de primaire aanjager van verificatiekosten.

Belangrijke regelgevingskoppeling: MIL-STD-882E SCI Categorie I → DO-178C Level A → DO-333 Formal Methods Supplement → TQL-1 toolkwalificatie onder DO-330. Elke schakel in deze keten heeft verplichte artefacten met gedefinieerde inhoud en traceerbaarheidsvereisten.

Specificatie vóór code: het formele model

TLA+ (Temporal Logic of Actions, ontwikkeld door Leslie Lamport) is de meest gebruikte formele specificatietaal voor gedistribueerde systemen en toestandsmachineprotocollen in defensiesoftware. Een TLA+-specificatie beschrijft een systeem als een set toestandsvariabelen en een set acties — overgangen die de toestand veranderen — uitgedrukt in een wiskundige notatie die ondubbelzinnig en machinaal controleerbaar is.

Het cruciale inzicht is dat TLA+-specificaties worden geschreven voordat de implementatie begint. Dit is niet slechts een goede praktijk; het is het mechanisme waarmee formele methoden de defecten vinden die tests missen. Tests oefenen gedragingen uit die de tester anticipeerde. Een formeel model, uitputtend gecontroleerd door de TLC-modelcontroleur, oefent alle gedragingen uit die de specificatie toestaat — inclusief gedragingen die de specificeerder niet bewust heeft overwogen.

Beschouw een vereenvoudigd voorbeeld van een protocol voor autorisatie van wapenafvuur. Het protocol vereist dat een afvuurcommando alleen wordt uitgevoerd wanneer beide bemanningsleden zich onafhankelijk hebben geverifieerd en beiden expliciet het afvuur hebben geautoriseerd binnen een gedefinieerd tijdvenster. Een natuurlijk-taalvereiste kan dit duidelijk stellen. Maar de formele specificatie moet elke toestandsovergang expliciet maken:

VARIABLES pilot_auth, copilot_auth, pilot_authorized,
          copilot_authorized, release_executed, time_window_open

TypeInvariant ==
    /\ pilot_auth       \in BOOLEAN
    /\ copilot_auth     \in BOOLEAN
    /\ pilot_authorized \in BOOLEAN
    /\ copilot_authorized \in BOOLEAN
    /\ release_executed \in BOOLEAN
    /\ time_window_open \in BOOLEAN

SafetyInvariant ==
    release_executed =>
        (pilot_auth /\ copilot_auth /\
         pilot_authorized /\ copilot_authorized /\
         time_window_open)

Init ==
    /\ pilot_auth       = FALSE
    /\ copilot_auth     = FALSE
    /\ pilot_authorized = FALSE
    /\ copilot_authorized = FALSE
    /\ release_executed = FALSE
    /\ time_window_open = FALSE

Wanneer TLC dit model controleert, verkent het alle bereikbare toestanden vanuit Init onder alle mogelijke Next-overgangen. Als een reeks geldige overgangen een toestand kan bereiken waarbij release_executed = TRUE terwijl de veiligheidsinvariant wordt geschonden, produceert TLC een tegenvoorbeeldspoor — een stapsgewijze reeks toestandsovergangen die leidt tot de onveilige toestand. Dit tegenvoorbeeld is geen testgeval dat toevallig faalde; het is een bewijs dat de specificatie een leemte heeft, en die leemte moet worden gedicht in de vereisten voordat de implementatie begint.

Wat TLA+ opvangt wat tests missen, valt in drie categorieën. Ten eerste, race-condities in gelijktijdige toestandsmachines — twee onafhankelijke gebeurtenissen die kunnen verstrengelen op een manier die geen sequentiële test kan uitoefenen. Ten tweede, levendigheidsovertredingen — scenario's waarbij het systeem vastloopt in een toestand die alle veiligheidsinvarianten voldoet maar nooit vooruitgang boekt naar een vereist doel. Ten derde, impliciete aannames — eigenschappen die het ontwerpteam impliciet hield en daarom nooit testte, die TLC schendt door overgangen te verkennen die het team niet bewust heeft overwogen.

SPARK Ada: subset van Ada voor aantoonbare correctheid

SPARK Ada is een formeel gedefinieerde subset van de programmeertaal Ada, ontworpen zodat programma's geschreven in SPARK statisch kunnen worden geverifieerd door de GNATprove-toolset. SPARK beperkt de volledige Ada-taal op manieren die de semantiek vatbaar maken voor geautomatiseerd bewijs: geen aliasing via access-types (pointers), geen dynamische dispatch in de bewijs-relevante subset, geen tasking in het bewijs-doel, en expliciete declaratie van alle globale toestand via aspect-specificaties.

De verificatiewaarde van SPARK komt van twee afzonderlijke analyseniveaus:

Stroomanalyse verifieert gegevensstrooméigenschappen zonder te proberen te bewijzen: het bevestigt dat elke gelezen variabele is geïnitialiseerd vóór de leesbewerking, dat subprogramma's alleen toegang hebben tot de globale toestand die zij declareren in hun Global-aspect, en dat informatiestromen consistent zijn met het Depends-aspect (dat stelt welke uitvoer afhankelijk is van welke invoer). Stroomanalyse verloopt snel — in seconden tot minuten voor grote codebases — en elimineert een gehele categorie runtime-fouten die conventioneel testen alleen zou vinden met adequate dekking.

Bewijsmodus probeert alle runtime-controlecondities te ontladen als wiskundige stellingen met behulp van de SMT-back-end solvers van GNATprove (Alt-Ergo, CVC5, Z3). Een runtime-controleconditie in SPARK wordt gegenereerd voor elke bewerking die een runtime-fout kan veroorzaken: arrayindex-toegangen, geheel getal-rekenkunde, type-conversies, preconditiecontroles. Wanneer GNATprove een controleconditie bewijst, heeft het vastgesteld dat geen uitvoering van het subprogramma die runtime-fout kan triggeren, voor alle mogelijke invoer die aan de preconditie voldoet. Dit is een fundamenteel sterkere garantie dan testen.

-- Example: verified bounded buffer for C2 message queue
package Message_Queue
  with SPARK_Mode => On
is
   Max_Messages : constant := 256;
   subtype Index_Type is Natural range 0 .. Max_Messages - 1;
   subtype Count_Type is Natural range 0 .. Max_Messages;

   type Queue_T is private;

   function Is_Full  (Q : Queue_T) return Boolean;
   function Is_Empty (Q : Queue_T) return Boolean;
   function Length   (Q : Queue_T) return Count_Type;

   procedure Enqueue (Q   : in out Queue_T;
                      Msg :        Message_T)
     with Pre  => not Is_Full (Q),
          Post => Length (Q) = Length (Q'Old) + 1;

   procedure Dequeue (Q   : in out Queue_T;
                      Msg :    out Message_T)
     with Pre  => not Is_Empty (Q),
          Post => Length (Q) = Length (Q'Old) - 1;

private
   type Queue_T is record
      Data  : Message_Array (Index_Type);
      Head  : Index_Type := 0;
      Tail  : Index_Type := 0;
      Count : Count_Type := 0;
   end record;
end Message_Queue;

GNATprove verifieert dat de implementatie van Enqueue en Dequeue hun postconditities naleeft voor alle invoer die aan hun preconditites voldoet, en dat geen array buiten-grenzen toegang, geen geheel getal-overflow en geen niet-geïnitialiseerde lezing kan optreden. Voor een berichtenwachtrij gebruikt in een gecertificeerde C2-applicatie vervangt dit tientallen grenswaarde-testgevallen door een enkel bewijs dat de volledige invoerruimte dekt.

Integratie met GNAT in de defensiesoftware CI/CD-pijplijn is eenvoudig: GNATprove wordt aangeroepen als een bouwstap met het projectbestand dat het bewijs-niveau specificeert (0 tot 4, waarbij 4 de hoogste inspanningsbewijzen probeert). Bewijsresultaten worden uitgestoten als machineleesbare JSON, waardoor integratie met defectregistratie en certificeringstraceerbaarheidstooling mogelijk is.

Formele analysetools voor C/C++

Het merendeel van de geïmplementeerde defensiesoftware is geschreven in C en C++, niet in Ada. Voor deze geïnstalleerde basis worden twee formele analysetools het meest gebruikt in gecertificeerde programma's: CBMC (C Bounded Model Checker) voor begrensde bereikbaarheidscontrole, en Frama-C met zijn WP (zwakste preconditie) plugin voor volledige deductieve verificatie.

CBMC vertaalt C-programma's naar SAT/SMT-problemen en lost deze op om te bepalen of een gegeven eigenschap kan worden geschonden binnen een begrensd aantal uitvoeringsstappen. CBMC controleert standaard op bufferoverflows, gebruik-na-vrijgave, geheel getal-overflow, null-pointer-dereferences en bewering-overtredingen — de categorieën defecten die de meerderheid van beveiligingskwetsbaarheden in C-code veroorzaken. Zijn primaire sterkte is een lage annotatie-inspanning: CBMC kan een C-functie controleren op runtime-fouten met minimale wijziging van de broncode. Zijn primaire beperking is dat het alleen garanties biedt tot de opgegeven lusafwikkelingsgrens — voor onbegrensde lussen is de afwezigheid van een CBMC-tegenvoorbeeld geen bewijs van correctheid.

Frama-C met WP is een modulair C-analyseframework dat volledige deductieve verificatie van C-code ondersteunt die is geannoteerd met ACSL (ANSI/ISO C Specification Language) contracten. ACSL-contracten specificeren functie-preconditites, postconditites, lusinvarianten en geheugenvoetafdrukken in een formele taal ingebed als C-commentaar. De WP-plugin genereert verificatiecondities (VC's) uit de geannoteerde C-code en ontlaadt deze met behulp van Why3's back-end bewijzers (Alt-Ergo, CVC5, Coq). Niet-bewezen VC's vertegenwoordigen echte defecten, ontbrekende lusinvarianten of eigenschappen die handmatige Coq-bewijzen vereisen.

De relatie tussen MISRA C en formele verificatie is complementair: MISRA C-regels elimineren de taalconstructies (impliciete geheel getal-conversies, pointer-aliasing via casts, dynamische geheugentoewijzing) die C-code semantisch dubbelzinnig maken en daarom moeilijk formeel te verifiëren. Het handhaven van MISRA C:2012-naleving — met name de Vereiste regels in de categorieën Pointer-typeconversies, Overlappende opslag en Essentieel typemodel — legt het goed gedefinieerde semantische fundament dat de WP-analyses van Frama-C nodig hebben om geluide resultaten te produceren. Een MISRA C-nalevingscontrole is dan ook de juiste eerste stap vóór het toepassen van Frama-C, niet een alternatief daarvoor.

Tool	Techniek	Annotatie-inspanning	Garantiesterkte	DO-330 TQL
CBMC	Begrensde modelcontrole (SAT)	Laag	Tot grens	TQL-3 (aanvullend)
Frama-C / WP	Deductieve verificatie (SMT)	Hoog (ACSL-contracten)	Volledig (voor bewezen doelen)	TQL-1 (met kwalificatiekit)
Polyspace Verifier	Abstracte interpretatie	Laag–gemiddeld	Geluid (kan over-benaderen)	TQL-1 (kwalificatiekit beschikbaar)
GNATprove (SPARK)	Deductief + stroomanalyse	Hoog (Ada+SPARK-contracten)	Volledig (voor bewezen doelen)	TQL-1 (kwalificatiekit beschikbaar)

Modelcontrole voor protocolverificatie

Modelcontrole verkent uitputtend de toestandsruimte van een eindig-toestandsmodel om te bepalen of een temporele logica-eigenschap geldt in alle bereikbare toestanden. Voor defensie-C2-protocollen — authenticatiehandshakes, berichtenvolgorde, link-state convergentie, cryptografische protocolcorrectheid — is modelcontrole de meest directe weg naar zekerheid omdat het protocolgedrag inherent gelijktijdig is en de faalmodi precies de verstrengeling-afhankelijke bugs zijn die testen niet betrouwbaar kan blootleggen.

De fundamentele uitdaging is toestandsexplosie: de grootte van de toestandsruimte groeit exponentieel met het aantal gelijktijdige componenten. Een C2-systeem met 8 knooppunten, elk met 16 toestandsbits, heeft een theoretische toestandsruimte van 2^128 — ongeveer 3,4 × 10^38 toestanden, die geen expliciete-toestand modelcontroleur in eindige tijd kan opsommen. Defensieprogramma's pakken toestandsexplosie aan via vier complementaire strategieën:

Abstractie. Vervang concrete gegevenswaarden door abstracte domeinen die de te controleren eigenschappen bewaren. In plaats van een 32-bits volgnummer te modelleren, modelleer het als een abstract element van een geordende verzameling {INITIAL, NEXT, WRAP} die de volgorderingssemantiek vastlegt zonder het volledige numerieke bereik. Counterexample-guided abstraction refinement (CEGAR) automatiseert dit: de modelcontroleur verfijnt de abstractie telkens wanneer hij een tegenvoorbeeld produceert dat niet uitvoerbaar is in het concrete model.

Symmetriereductie. Benut structurele equivalenties tussen componenten. Als 8 knooppunten in een C2-netwerk structureel identiek zijn, hoeft de modelcontroleur slechts één vertegenwoordiger van elke equivalentieklasse van systeemtoestanden onder de permutatiegroep van de 8 knooppunten te verkennen. Dit kan de effectieve toestandsruimte reduceren met een factor N! (8! = 40.320 voor 8 knooppunten).

Partiële-orde reductie. Veel gelijktijdige uitvoeringen die alleen verschillen in de volgorde van onafhankelijke gebeurtenissen (gebeurtenissen die geen toestand delen) leiden tot dezelfde toestand. Partiële-orde reductie vouwt deze equivalente volgordes samen in één vertegenwoordiger zonder verlies van eigenschap-controlerende volledigheid.

Begrensde modelcontrole. In plaats van alle paden van willekeurige lengte te verkennen, controleer alle paden tot lengte k met een SAT- of SMT-solver. De meeste protocoldefecten manifesteren zich in korte tegenvoorbeeldsporen (4–20 stappen); begrensde modelcontrole met k=30 is voldoende om de grote meerderheid van protocolfouten te vinden terwijl het rekenkundig haalbaar blijft.

Wanneer een modelcontroleur een eigenschap-overtreding vindt, produceert hij een tegenvoorbeeldspoor — een complete reeks systeemtoestanden van de begintoestand tot de schendende toestand. Dit spoor is direct bruikbaar: het specificeert precies welke reeks gebeurtenissen leidt tot de onveilige toestand, waardoor ontwikkelaars de fout deterministisch kunnen reproduceren en een protocoloplossing kunnen ontwerpen. In één gedocumenteerde defensie-C2-protocolverificatie onthulde een tegenvoorbeeldspoor van 12 stappen dat een authenticatie-omzeiling mogelijk was als een specifieke combinatie van berichtvertraging en hertransmissie optrad — een scenario dat in 18 maanden integratietesten niet was uitgeoefend.

Formele methoden integreren in DO-178C-naleving

Het DO-333-supplement op DO-178C legt het kader vast voor het gebruik van formele methoden als alternatieve nalevingsmiddelen voor specifieke DO-178C-verificatiedoelstellingen. Het gebruik van DO-333 vereist een Formal Methods Plan dat het volgende behandelt:

De gekozen formele methode(n) en de basis voor hun selectie
De formeel te verifiëren eigenschappen en hun koppeling aan DO-178C-softwarevereisten
De te gebruiken tool(s), hun DO-330-kwalificatiestatus en het kwalificatieplan indien niet vooraf gekwalificeerd
Hoe formeel verificatiebewijs wordt gepresenteerd in de Software Accomplishment Summary
Welke combinatie van formele verificatie en testen volledige doelstellingsdekking bereikt

Traceerbaarheid is het kritieke integratiemechanisme. De DO-178C-traceerbaarheidsketen loopt van Systeemvereisten via High-Level Requirements (HLR), Low-Level Requirements (LLR), Broncode en Verificatiegevallen. Formele artefacten moeten op gedefinieerde punten in deze keten worden ingevoegd:

System Req (SRD)
    └─► High-Level Req (HLR)    ◄── TLA+-specificatie-eigenschappen
            └─► Low-Level Req (LLR) ◄── SPARK-contracten / ACSL-annotaties
                    └─► Source Code  ◄── GNATprove / CBMC / Frama-C doel
                            └─► Verificatiegevallen (SVCP/SVR)
                                    └─► Bewijsrapporten, modelcontroleur-uitvoer,
                                        tegenvoorbeeld-vrije verificatielogboeken

Toolkwalificatie onder DO-330 is de tweede integratie-uitdaging. Een tool die een vereist DO-178C-verificatieproces elimineert — zoals een formele bewijzer die de noodzaak voor structurele dekkingstesten elimineert — moet worden gekwalificeerd op TQL-1. TQL-1-kwalificatie vereist een Tool Qualification Plan, Tool Accomplishment Summary, Tool Operational Requirements en testbewijs gegenereerd in de bouwomgeving van het programma. Vooraf gekwalificeerde toolpakketten van AdaCore (GNATprove), MathWorks (Polyspace) en LDRA verminderen deze inspanning aanzienlijk vergeleken met interne kwalificatie, maar het programma moet nog steeds verifiëren dat de kwalificatie van de leverancier van toepassing is op hun specifieke toolversie en gebruikscontext.

De discussie over AI-ethiek voor militaire systemen is hier steeds relevanter naarmate programma's AI-ondersteunde formele verificatie overwegen — tools die neurale netwerken gebruiken om lusinvarianten of bewijsstrategieën voor te stellen. De certificeringsstatus van dergelijke AI-ondersteuningscomponenten is onopgelost onder de huidige DO-178C-richtlijnen; programma's moeten AI-ondersteunde suggesties behandelen als dat ze onafhankelijke menselijke beoordeling vereisen voordat ze worden opgenomen in certificeringsbewijs.

Kosten-batenanalyse: wanneer is formele verificatie de moeite waard

De kosten van formele verificatie zijn reëel en aanzienlijk. Het annoteren van een SPARK Ada-module van 10.000 regels tot het punt van volledig runtime-foutbewijs duurt 3–6 maanden expertingenieurtijd. Het kwalificeren van een formele verificatietool onder DO-330 TQL-1 duurt 3–6 maanden extra inspanning de eerste keer. Het schrijven en controleren van een TLA+-specificatie van een complex protocol duurt weken. Geen van deze kosten verdwijnt.

De berekening van voordelen moet worden gemaakt ten opzichte van het juiste alternatief. Het alternatief voor formele verificatie bij DO-178C Level A is niet geen verificatie; het is uitputtend testen op MC/DC-dekking, wat voor een complexe toestandsmachine met N voorwaarden in een beslissing O(2N) testgevallen heeft, mogelijk met formele analyse vereist om toch MC/DC-toereikendheid aan te tonen. Voor niet-triviale veiligheidskritische functies zijn de testkosten voor het bereiken van Level A-doelstellingen zonder formele methoden vaak hoger dan de kosten van formele verificatie — en bieden een zwakkere vorm van zekerheid.

Industriegegevens ondersteunen consistent drie conclusies:

Kosten van defectontdekking. Defecten gevonden tijdens formele specificatie kosten ongeveer 1× om te repareren. Defecten gevonden tijdens codebeoordeling kosten 10× de basislijn. Defecten gevonden tijdens integratietesten kosten 100×. Defecten gevonden na certificering kosten 1.000× of meer, inclusief her-certificeringsoverhead. Formele specificatie, die defecten in de vroegst mogelijke fase blootlegt, heeft het beste defect-kostenprofiel van elke techniek — met name voor de architectuur-niveau defecten (onjuist toestandsmachine-ontwerp, protocol-race-condities) die formele methoden uniek effectief bij het vinden zijn.

Reductie van levenscyclus-verificatiekosten. Voor programma's die SPARK Ada toepassen op Level A-componenten is de stroomafwaartse verificatiekostreductie 50–70%. De formele bewijzer ontlaadt de structurele dekkingsdoelstellingen die anders uitgebreide testharnas-ontwikkeling, dekkingsinstrumentatie en dekkingsmeting over een combinatorische testmatrix zouden vereisen.

Wanneer formele verificatie de moeite niet waard is. Voor software op DO-178C Level C of lager, en MIL-STD-882 Categorie III of IV, overtreft de overhead van formele methoden doorgaans het voordeel. Level C vereist 100% instructie- en beslissingsdekking — haalbaar met standaard testgestuurde ontwikkelingspraktijken en dekkingstooling. Het toepassen van formele methoden op Level C voegt kosten toe zonder proportionele zekerheidswaarde toe te voegen. Het technische oordeel is eenvoudig: pas formele methoden toe waar regelgevingsvereisten het verplichten (Level A, Level B voor complexe toestandsmachines) of waar de gevolgen van niet-gedetecteerde defecten — verlies van levens, systeemfalen in gevechten — de investering rechtvaardigen ongeacht de regelgevingsverplichting.

Beslissingsregel: Formele verificatie is vereist bij DO-178C Level A en MIL-STD-882 Categorie I. Het is sterk aanbevolen bij DO-178C Level B en Categorie II voor complexe gelijktijdige of protocol-implementerende componenten. Het is optioneel en doorgaans niet kosteneffectief bij Level C en lager. De grens is niet primair financieel — het is de grens tussen softwarefouten waarvan de gevolgen herstelbaar zijn en die waarvan de gevolgen dat niet zijn.

Het praktische pad voor de meeste defensieprogramma's is een gelaagde aanpak: TLA+-formele specificatie voor alle veiligheidskritische toestandsmachines en protocollen; SPARK Ada voor nieuwe of herschreven Level A-componenten; CBMC en MISRA C voor bestaande C-componenten die niet kunnen worden herschreven; en Frama-C/WP voor de meest veiligheidskritische C-functies waar volledige deductieve verificatie gerechtvaardigd is. Elke laag voegt zekerheid toe boven wat testen alleen biedt, en de uitvoer van elke laag genereert certificeringsbewijs dat de testlast op component- en integratietestniveaus vermindert.

Bespreek uw project

Corvus Intelligence ontwikkelt veiligheidskritische defensiesoftware met formele verificatiemethoden, SPARK Ada en DO-178C-conforme processen. Als u een veiligheidskritisch systeem ontwerpt of certificeert en wilt bespreken waar formele methoden passen in uw programma, zijn wij beschikbaar voor een technische briefing.

Defensie software-ontwikkeling → Briefing boeken

Deze analyse is opgesteld door Corvus Intelligence-ingenieurs die veiligheidskritische software bouwen en certificeren voor defensie- en overheidsprogramma's. Meer over ons team →

Veelgestelde vragen

Wat vereist DO-178C Level A precies vanuit een formele verificatieperspectief?

DO-178C Level A — van toepassing op software waarvan het falen een catastrofale toestand kan veroorzaken — verplicht 100% Modified Condition/Decision Coverage (MC/DC) voor structureel testen. Formele verificatie via het DO-333-supplement kan substituten voor structurele dekkingsdoelstellingen door wiskundig bewijs te leveren dat een eigenschap geldt voor alle mogelijke invoer, waardoor uitputtende testgevallen worden vervangen die combinatorisch onmogelijk te opsommen zijn. Het Plan for Software Aspects of Certification (PSAC) moet beschrijven hoe elke Level A-doelstelling wordt bereikt, of dit nu door testen, analyse of formele methoden is. Elke tool die wordt gebruikt om vereiste verificatieactiviteiten te elimineren, moet worden gekwalificeerd onder DO-330.

Kunnen TLA+-specificaties vereistendocumenten vervangen in defensieprogramma's?

TLA+-specificaties vullen aan maar vervangen niet de natuurlijk-taalvereisten in defensieprogramma's. Verwervingsregelgeving specificeert de vorm en inhoud van vereistendocumentatie — een formele specificatie alleen voldoet niet aan deze contractuele verplichtingen. De praktische waarde is bidirectioneel: natuurlijk-taalvereisten moeten worden geformaliseerd in TLA+ om ambiguïteit bloot te leggen voordat de implementatie begint, en TLA+-modellen moeten herleidbaar zijn naar natuurlijk-taalvereisten om DO-178C Tabel A-3 traceerbaarheidsdoelstellingen te voldoen.

Hoe verschilt de stroomanalyse van SPARK Ada van statische analysetools zoals Coverity of Polyspace?

De stroomanalyse van SPARK Ada is een heel-programma, semantisch-bewust bewijs dat bepaalde klassen van runtime-fouten aantoonbaar afwezig zijn — niet slechts statistisch onwaarschijnlijk. Wanneer GNATprove rapporteert dat een subprogramma vrij is van runtime-fouten, heeft het mechanisch geverifieerd dat geen uitvoeringspad een Constraint_Error of Program_Error kan veroorzaken onder de gestelde preconditites. Coverity en Polyspace zijn heuristische tools: ze rapporteren bevindingen die echte bugs kunnen zijn of valse positieven, en de afwezigheid van bevindingen garandeert niet de afwezigheid van bugs. De afweging is dat SPARK annotaties vereist (contracten, gegevensafhankelijkheden, globale toestandsdeclaraties) die conventioneel Ada niet vereist.

Wat is toestandsexplosie bij modelcontrole en hoe wordt het beheerd voor defensie-C2-protocollen?

Toestandsexplosie is de exponentiële groei van de toestandsruimte die een modelcontroleur moet verkennen: een systeem met N booleaanse variabelen heeft 2^N bereikbare toestanden, en gelijktijdige systemen vermenigvuldigen toestandsruimten multiplicatief over componenten. Defensieprogramma's beheren toestandsexplosie via abstractie (concrete waarden vervangen door abstracte domeinen), symmetriereductie (structurele equivalenties tussen knooppunten benutten), partiële-orde reductie (equivalente gelijktijdige gebeurtenisvolgordes samenvoegen) en begrensde modelcontrole (alle paden tot een bepaalde lengte controleren met SAT/SMT-solvers). De meeste protocoldefecten manifesteren zich in korte tegenvoorbeeldsporen van 4–20 stappen, dus begrensde modelcontrole met k=30 vindt de grote meerderheid van protocolfouten terwijl het haalbaar blijft.

Welke MISRA C-regels zijn vereiste voorwaarden voordat formele verificatie met Frama-C wordt toegepast?

De WP-plugin van Frama-C is het meest effectief op code die MISRA C:2012-regels over pointerrekenkunde (Regel 18.1), pointeraftrekking tussen niet-gerelateerde pointers (Regel 18.2) en dynamische geheugentoewijzing (Regel 21.3) naleeft. Ongedefinieerd gedrag in C-code — dat MISRA C-regels grotendeels elimineren — creëert ongeluide verificatieresultaten in Frama-C. Het eerst handhaven van MISRA C-naleving, geverifieerd door een gekwalificeerde checker, legt het geluide semantische fundament dat de analyses van Frama-C vereisen. MISRA C:2012 Amendment 3 (2023) behandelt ook C11-gelijktijdigheidsconstructies die eerdere edities niet bestreken.

Hoe schrijft u een TLA+-spec voor een toestandsmachine voor autorisatie van wapenafvuur?

Modelleer de vergrendeling als een toestandsmachine: definieer een VARIABLES-tuple die de fysieke en autorisatietoestand dekt, schrijf een Init-predicaat dat de veilige begintoestand vaststelt, en definieer Next als een disjunctie van alle toegestane overgangen. Druk de kritieke veiligheidseigenschap uit als een invariant — bijvoorbeeld dat de afvuurtoestand alleen kan worden bereikt wanneer beide bemanningsleden zich onafhankelijk hebben geverifieerd en geautoriseerd binnen een geldig tijdvenster. Voer de TLC-modelcontroleur uit op alle bereikbare toestanden; elk tegenvoorbeeldspoor is een reeks overgangen die de invariant schendt en vertegenwoordigt een echt ontwerpdefect dat moet worden opgelost in de specificatie voordat de implementatie begint.

Wat vereist DO-330-toolkwalificatie voor een formele verificatietool gebruikt in een Level A-programma?

DO-330 definieert vijf Tool Qualification Levels (TQL-1 tot TQL-5). Een formele verificatietool die een vereist DO-178C-softwareverificatieproces elimineert, moet worden gekwalificeerd op TQL-1. TQL-1-kwalificatie vereist een Tool Qualification Plan, Tool Operational Requirements, Tool Accomplishment Summary en testbewijs dat de uitvoer van de tool correct is. Programma's gebruiken doorgaans vooraf gekwalificeerde toolversies van leveranciers — AdaCore's SPARK Pro en MathWorks Polyspace Verifier bevatten beide DO-330-kwalificatiekits — in plaats van open-source tools intern te kwalificeren. De kwalificatieartefacten worden onderdeel van het certificeringsgegevenspakket van het programma.

Hoe gaat CBMC om met onbegrensde lussen in C-defensiecode?

CBMC verwerkt lussen via lusafwikkeling: het vervangt elke lus door een eindige reeks kopieën van de lusromp tot een door de gebruiker opgegeven grens, en voegt een afwikkelingsbevestiging in die activeert als enige uitvoering meer iteraties vereist dan de grens. Voor realtime defensiecode die al begrensde lussen heeft (zoals vereist door MISRA C Regel 15.4 en JSF++ Regel 188), kan CBMC eigenschappen verifiëren met de exacte afwikkelingscount. Wanneer een afwikkelingsbevestiging activeert, betekent dit dat CBMC niet kan garanderen dat de eigenschap geldt voor paden langer dan de grens — vergroot de grens of bewijs luseindige apart. Defensiecode die recursieve functies verbiedt, elimineert het recursieve geval volledig.

Kan formele verificatie worden toegepast op AI/ML-componenten in defensiesystemen?

Formele verificatie van neurale netwerk-componenten is een actief onderzoeksgebied, nog niet volwassen voor Level A-certificering. Tools zoals Marabou kunnen lokale robuustheidseigenschappen van feedforward-netwerken verifiëren maar schalen slecht voorbij een paar honderd neuronen. De huidige defensiepraktijk voor AI/ML-componenten is om ze te behandelen als niet-deterministische zwarte dozen buiten de formeel geverifieerde veiligheidsomgeving: het formele model verifieert dat het omringende systeem veilig blijft ongeacht wat de AI-component uitvoert — via mens-in-de-lus overschrijvingsgaranties, uitvoerbereikshandhaving door een geverifieerde wrapper, of architecturale scheiding zodat de AI-uitvoer alleen informeert in plaats van commando's geeft.

Wat zijn de typische kostenoverkop van SPARK Ada formele verificatie versus conventioneel Ada op een C2-component?

Industriegegevens van AdaCore en defensie-integrators tonen consistent een 20–40% ontwikkelingskostentoename voor SPARK Ada ten opzichte van conventioneel Ada op nieuwe componenten, toe te schrijven aan annotatie-inspanning en bewijsontlading. Dezelfde gegevens tonen echter een 50–70% reductie van stroomafwaartse verificatiekosten: structurele dekkingstesten, codebeoordeling-checklists en testgeval-opsomming worden aanzienlijk verminderd wanneer de bewijzer al de afwezigheid van runtime-fouten heeft aangetoond. Het netto-effect voor Level A-programma's — waar verificatie doorgaans 40–60% van de totale softwarekosten is — is een algehele reductie van totale levenscycluskosten van 15–25%, naast kwalitatief sterkere zekerheid dan testen alleen biedt.