100%-ige Sicherheit durch mathematisch vollständige formale Verifikation
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.
BTC Embedded Systems ist Pionier bei der Integration der Model Checking Technologie in ein kommerzielles Entwicklungswerkzeug. Wir machen diese hochautomatisierte Technologie für die Industrie verfügbar und tragen zu einer signifikanten Steigerung von Effizienz und Qualität in den Entwicklungsprojekten unserer Kunden bei. Das Ziel eines Model Checkers ist es, das Verhalten eines Systems vollständig auf eine bestimmte temporale Eigenschaft zu überprüfen und automatisch zu beweisen, dass diese Eigenschaft stets erfüllt ist. Ist dies nicht möglich, liefert der Model Checker ein Gegenbeispiel, das explizit zeigt, wie die zu prüfende Eigenschaft verletzt werden kann. Im Gegensatz zur Ausführung von Testfällen analysiert der Model Checker alle möglichen Läufe eines Systems und liefert einen vollständigen mathematischen Beweis, der das dynamische Verhalten des Systems über die Zeit berücksichtigt. Insbesondere die Bereitstellung eines Gegenbeispiels unterscheidet Model Checking von anderen automatischen Analysemethoden wie der Abstract Interpretation.
In einem Modell-basierten Entwicklungsprozess ist die intuitivste Debug-Umgebung mit Sicherheit das Simulink Modell. BTC EmbeddedValidator generiert dazu eine “Sandbox” als Kopie des Modells, welche auch direkt die entsprechenden Test- und Kalibrations-daten enthält. Um das Verhalten auf Code-Ebene genauer zu analysieren, kann ebenfalls ein Microsoft Visual Studio Projekt oder eine IDE-unabhängige Debug-Umgebung exportiert werden.
Sie möchten unsere Tools in Ihrer Entwicklungsumgebung testen? Gerne stellen wir Ihnen eine kostenfreie Evaluierungslizenz zur Verfügung., inkl. Kick-Off Trainings-Workshop und Support durch unser Team.
Sie haben Fragen oder Interesse an einer persönlichen Tool Demo? Nutzen Sie unten stehenden Link, um ein unverbindliches Meeting mit unserem Engineering Team zu buchen.
Sie möchten unsere Tools in Ihrer Entwicklungsumgebung testen? Gerne stellen wir Ihnen eine kostenfreie Evaluierungslizenz zur Verfügung., inkl. Kick-Off Trainings-Workshop und Support durch unser Team.
Sie haben Fragen oder Interesse an einer persönlichen Tool Demo? Nutzen Sie unten stehenden Link, um ein unverbindliches Meeting mit unserem Engineering Team zu buchen.
Unser Blog mit Artikeln rund um die Themen Embedded Software Entwicklung, Model-based Design, Serien-Code Generierung, ISO 26262, Continuous Integration und mehr.
Entdecken Sie die wichtigsten Features unserer Tools in diesen kurzen Demo Videos.
Intuitive formale Spezifikation von sicherheitskritischen Anforderungen
Wir entwickeln automatisierte und intelligente Test Lösungen, welche unseren Kunden weltweit dabei helfen, eine hohe Software Qualität im Einklang mit dem ISO 26262 Standard zu erreichen
Copyright © 2024 BTC Embedded Systems
