BTC EmbeddedValidator
Beweisen Sie es sich
100 % Beweiskraft für Sicherheitskritische Systeme
In der modellbasierten Entwicklung gibt es immer wieder Bereiche, die 100 %ige Sicherheit erfordern. Zum Beispiel wenn es um die Erfüllung der strengen Auflagen der ISO 26262 geht – hier ist ein genaues Prüfen von Modell und Code unerlässlich.
Damit in hoch sicherheitsrelevanten Systemen künftig keine Zweifel mehr bestehen, haben wir ein Werkzeug entwickelt, das Ihnen 100 % mathematische Beweiskraft liefert: Den BTC EmbeddedValidator zur formalen Verifikation von TargetLink-Modellen.
Setzen Sie neue Qualitätsmaßstäbe im modellbasierten Prüfprozess und schaffen Sie sich die beste Basis für Creative Engineering.
Das sollten Sie gleich verifizieren
Der BTC EmbeddedValidator bietet Ihnen herausragende Möglichkeiten, um Ihr TargetLink-Modell formal zu prüfen:- Formale Modellverifikation
- Formale Requirements-Spezifikation
- Generierung von Gegenbeispielen
- Automatischer Debugging-Support
- Vollautomatisierte Überprüfung der Robustheit der Modelle
- Auffinden von unerreichbaren Modellteilen
- Unterstützt bzgl. der strengen Auflagen nach ISO 26262 und IEC 61508
- Nahtlose TargetLink-Integration
- Umfassendes Ergebnis-Reporting
- Benutzerdefinierte Erreichbarkeitsanalysen
Hält Ihr Modell, was es verspricht?
Als Ingenieur wissen Sie am besten, dass schon kleinste Mängel große Folgen haben können. Darum unterstützt BTC EmbeddedValidator zahlreiche Anwendungsfälle, mit denen Sie die Qualität Ihres Modells eindeutig überprüfen können.Formale Verifikation von Requirements
Ihr Nachweis über die Gültigkeit aller funktionalen und sicherheitskritischen Requirements eines Modells: Unter Verwendung des TargetLink-API kann EmbeddedValidator eine eindeutige mathematische Repräsentation eines TargetLink-Modells extrahieren und durch Model-Checking formal prüfen.Mehr Möglichkeiten kreativ zu sein
Robustheitsanalyse des Modells
- Range Violation Analyse
Gibt es ein Szenario, in dem bei bestimmten Variablen ein Über- oder Unterlauf auftritt? Die Range Violation Analyse verrät es Ihnen.
- Drive to State
Wählen Sie zwischen einer, mehreren oder allen Zuständen eines Stateflow-Charts, wenn Sie eine Erreichbarkeitsanalyse in einer Verifikationsaufgabe ausführen.
- Drive to Configuration
Eine Erweiterung der Drive-to-State Analyse, die Ihnen verrät, ob zwei oder mehr Zustände in verschiedenen parallelen Subcharts zum gleichen Zeitpunkt erreichbar sind.
- Drive to Property
Prüfen Sie, ob ein Modellzustand erreichbar ist, in dem eine bestimmte Eigenschaft erfüllt wird. Dazu werden alle verfügbaren Variablen und Zustände des ausgewählten Stateflow-Charts oder Subsystems angezeigt, um die entsprechende Eigenschaft in einem Booleschen Ausdruck zu formulieren.
