Definition
Ergänzung zu DO-178C für die Anwendung formaler Methoden in der Software-Verifikation. Erlaubt mathematische Beweise als Ersatz oder Ergänzung zu klassischem Testen — besonders relevant bei DAL-A/B-Software, wo vollständige Testabdeckung praktisch unmöglich ist. Etabliert durch Tools wie SPARK, Astrée, Frama-C. Ermöglicht höhere Verifikationsabdeckung bei niedrigeren Testkosten.
In der Praxis
Formale Methoden sind der einzige Punkt in der Software-Zulassung, an dem Mathematik Testaufwand ersetzen darf — und genau dort liegen die Missverständnisse. DO-333 regelt, welche Verifikationsziele der DO-178C durch formale Beweise erfüllt werden dürfen und welche nicht; „wir testen nicht mehr" ist keine Option. Drei Fehler begegnen mir in Projekten. Erstens wird das formale Modell nicht validiert: Der Beweis ist korrekt, aber die Annahmen des Modells entsprechen nicht der realen Software — bewiesen ist dann eine Eigenschaft eines Artefakts, das es so nicht gibt. Zweitens wird ein Analysewerkzeug ohne Qualifizierung nach DO-330 vertraut, obwohl sein Output ungeprüft in den Zulassungsnachweis fließt. Drittens fehlt die Abdeckungsargumentation: Formale Nachweise und klassische Tests laufen nebeneinander, ohne dass dokumentiert ist, welches Ziel womit erfüllt wird. Richtig eingesetzt — etwa mit SPARK oder Astrée für Laufzeitfehlerfreiheit — senken formale Methoden den Verifikationsaufwand bei hohen Kritikalitäten erheblich.
Häufige Fragen zu DO-333
Was ist der Unterschied zwischen formalen Methoden und klassischem Testen?
Testen ist Stichprobe: Sie zeigen für ausgewählte Eingaben, dass sich die Software korrekt verhält — über alle anderen Eingaben sagt der Test nichts. Formale Methoden sind Beweis: Sie zeigen mathematisch, dass eine Eigenschaft für alle Eingaben gilt, die das zugrunde liegende Modell erfasst. Der Haken liegt genau in diesem Modell: Bewiesen wird, was formalisiert wurde — Annahmen, die nicht im Modell stehen, bleiben unbewiesen. Deshalb ersetzen formale Methoden nach DO-333 auch nur bestimmte Verifikationstätigkeiten, niemals alle; die Integration auf der Zielhardware etwa bleibt weiterhin zu prüfen. In der Praxis ergänzen sich beide: Formale Analyse für abgrenzbare, kritische Eigenschaften wie Laufzeitfehlerfreiheit, Tests für das Systemverhalten im Verbund.
Welche Regeln gelten, wenn wir formale Methoden im Zulassungsnachweis verwenden wollen?
DO-333 als Supplement zur DO-178C definiert den Rahmen: Sie müssen deklarieren, welche Verifikationsziele durch formale Methoden erfüllt werden, und nachweisen, dass die verwendeten Beweise korrekt und die Annahmen begründet sind. Zwei Punkte werden regelmäßig unterschätzt. Erstens die Werkzeugfrage: Wenn der Output eines Analysewerkzeugs ohne weitere Prüfung als Nachweis dient, muss das Werkzeug nach DO-330 qualifiziert sein — oder Sie verifizieren seine Ergebnisse auf anderem Weg. Zweitens die Kombinationslogik: Wo formale Nachweise und klassische Verifikation gemeinsam ein Ziel erfüllen, muss die Abdeckung dokumentiert und lückenlos sein. Die Anwendung ist im Zulassungsplan zu beschreiben und mit der Behörde abzustimmen — formale Methoden sind etabliert, aber deren Einsatzumfang ist immer Einzelfall (RTCA DO-333, Supplement zu DO-178C; RTCA DO-330).
Wie steigen wir in formale Methoden ein, ohne das Projektbudget zu sprengen?
Klein anfangen, klar abgrenzen. Erstens: Wählen Sie eine einzelne, gut abgrenzbare Eigenschaft — der Klassiker ist die Abwesenheit von Laufzeitfehlern wie Überläufen oder Divisionen durch null in einem kritischen Modul. Zweitens: Setzen Sie ein Werkzeug ein, für das ein Qualifizierungskit existiert; die DO-330-Qualifizierung aus eigener Kraft nachzuziehen, übersteigt die meisten Budgets. Drittens: Dokumentieren Sie von Beginn an, welche DO-178C-Ziele Sie mit dem formalen Nachweis adressieren und welche Annahmen Ihr Modell trifft — diese Annahmenliste ist das Herzstück des Arguments. Viertens: Stimmen Sie den Ansatz früh mit der Zulassungsbehörde oder dem zugelassenen Vertreter ab, idealerweise über das Certification Liaison, bevor Sie Skalierung planen. Und fünftens: Rechnen Sie den Nutzen ehrlich — formale Methoden lohnen sich bei hohen Kritikalitäten, wo vollständige Testabdeckung praktisch unerreichbar ist, nicht bei jeder Hilfsfunktion.