BTC EmbeddedValidator ist ein Werkzeug zur formalen Verifikation von sicherheitskritischen Anforderungen.
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.