Formale Verifikation mit mathematischem Beweis

BTC EmbeddedValidator ergänzt klassische Testverfahren durch formale Verifikation auf Basis von Model-Checking-Technologie. Das Werkzeug beweist mathematisch, ob eine sicherheitskritische Anforderung unter allen möglichen Bedingungen eingehalten wird, oder liefert ein konkretes Gegenbeispiel, falls dies nicht der Fall ist.

Durch die nahtlose Integration in automatisierte Workflows und moderne Benutzeroberflächen wird formale Verifikation praxistauglich, skalierbar und für den täglichen Einsatz in sicherheitskritischen Softwareprojekten geeignet.