Was wäre, wenn Ihr Computer Ihre Anforderungen verstehen könnte?
Der Bremsbefehl muss sich nach dem Freigabesignal stabilisieren – innerhalb kurzer Zeit.
Zwischen einer schriftlichen Anforderung und einem sicheren System klaffen zwei Lücken. Auch beliebig viele Tests schließen sie nicht.
Verschiedene Ingenieure verstehen informelle Anforderungen unterschiedlich. „Schnell“, „kurz danach“, „stabil“ – jeder füllt die Lücken auf seine Weise. Auch die korrekte Umsetzung einer falsch verstandenen Anforderung führt zum falschen System.
Tests prüfen die Verhaltensweisen, an die Sie gedacht haben. Sie können jedoch nicht alle Eingaben, Zustände und Kalibrierungen abdecken. Deshalb bleibt selbst bei einer vollständig bestandenen Testsuite die entscheidende Frage offen: „Kann meine Sicherheitsanforderung jemals verletzt werden?“
Tests prüfen Stichproben. Formale Verifikation liefert den Nachweis.
Formale Methoden schließen beide Lücken: Sie präzisieren die Anforderung und weisen anschließend nach, dass der Code sie erfüllt.
BTC Universal Pattern ist eine grafische, intuitive Methode für das Requirements Engineering – Editor und Dokumentation sind dasselbe Artefakt. Sie beschreiben, welche Bedingung gelten muss; das Tool macht sie maschinenlesbar und bewahrt durchgängig die Rückverfolgbarkeit zur ursprünglichen Anforderung.
Markieren Sie die aussagekräftigen Ausdrücke in der Anforderung und wandeln Sie sie in wiederverwendbare Makros um.
Platzieren Sie die Makros grafisch als Auslöser, Aktion und Timing – das Muster beseitigt die Mehrdeutigkeit.
Binden Sie jedes Makro an echte Systemsignale. Die Anforderung ist nun maschinenlesbar und ausführbar.
Formale Spezifikationen von Hand zu erstellen war aufwendig. Eine Anforderung zu formalisieren ist im Kern eine sprachliche Aufgabe – genau darin ist moderne KI stark.
Der BTC AI Assistant erstellt aus einer schriftlichen Anforderung den Entwurf eines Universal Pattern mit Auslöser, Aktion und Zeitvorgabe. Sie können ihn anschließend verfeinern, freigeben oder daraus Testfälle generieren.
Maschinenlesbare Anforderungen = automatisierte Verifikation.
Vergleicht jeden vorhandenen Testfall gleichzeitig mit allen formalisierten Anforderungen und erkennt so Nebenwirkungen, für die ein Test nie entwickelt wurde, ohne zusätzlichen Aufwand.
Model Checking generiert genau die Testfälle, die in Ihrer Testsuite fehlen, und führt die Anforderungsabdeckung so deterministisch auf 100 % – statt durch Versuch und Irrtum.
Model Checking liefert den mathematischen Nachweis, dass eine Anforderung niemals verletzt werden kann – keine Kombination aus Eingaben und Kalibrierungen erreicht den unsicheren Zustand – oder gibt ein konkretes Gegenbeispiel zurück.
Formalisierung schafft Präzision – unklare Anforderungen werden erkannt, bevor Code und Tests entstehen.
Die Anforderungsabdeckung wird automatisch gemessen und vervollständigt – nicht geschätzt.
Jeder Test wird gegen alle Anforderungen geprüft – Regressionen werden ohne zusätzlichen Aufwand sichtbar.
Automatisch generierte Vektoren schließen die Lücken zur vollständigen Anforderungsabdeckung.
Eine Garantie für alle Eingaben und Kalibrierungen.
Eine Evaluierungslizenz umfasst einen Einführungsworkshop mit unseren Ingenieuren – vollständig eingerichtet anhand einer Ihrer realen Anforderungen.
