Mehr als Testen

100%-ige Sicherheit durch mathematisch vollständige formale Verifikation.

BTC EmbeddedValidator

100%-ige Sicherheit durch mathematisch vollständige formale Verifikation

BTC EmbeddedValidator ist ein Werkzeug zur formalen Verifikation von sicherheitskritischen Anforderungen. Die formale Verifikation nutzt als Basis die formalisierten Anforderungen aus BTC EmbeddedSpecifier und wird auf dem Seriencode durchgeführt

Mehr als Testen

Bei einer typischen Softwarekomponente für eingebettete Systeme ist die Anzahl der Kombinationsmöglichkeiten aller Eingangssignale und Parameterwerte nahezu unendlich. Das bedeutet, dass selbst eine große Anzahl an Testfällen nicht in der Lage ist, alle möglichen Pfade und Kombinationen abzudecken. Damit bleibt auch mit einem guten Set an Testfällen am Ende die Frage offen: „Kann eine bestimmte Sicherheitsanforderung verletzt werden?“

BTC EmbeddedValidator nutzt Model Checking Technologie, um automatisch mit einem vollständigen mathematischen Beweis zu zeigen, dass eine Anforderung nicht verletzt werden kann. Damit wird garantiert, dass es keine Kombination von Eingangssignalen und Parameterwerten gibt, welche das System in einen Zustand bringt, der die Anforderung verletzt.

Automatische Testfall-Generierung für den Fehlerfall

Sollte es doch möglich sein eine Anforderung zu verletzen, generiert BTC EmbeddedValidator automatisch einen Testfall als Gegenbeispiel. Dieser Testfall zeigt, wie das System in einen Zustand gebracht werden kann, der die zugehörige Anforderung verletzt.

Umfassendes Debugging

Wenn ein Gegenbeispiel generiert wurde, können Sie mit den leistungsstarken Debugging-Möglichkeiten der BTC EmbeddedPlatform automatisch eine Debug-Umgebung als Simulink/TargetLink Modell oder Microsoft Visual Studio Projekt erstellen