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.

Unterstützung der Fehleranalyse

Ein integriertes Waveform-Diagramm zur schnellen Übersicht der Analysenergebnisse ist Teil von BTC EmbeddedValidator. Hinzu kommt eine automatische Unterstützung der Simulink-Simulation: Findet BTC EmbeddedValidator einen Fehler, wird für den Simulink-Simulator automatisch ein m-Skript erzeugt, das dann gemeinsam mit dem Modell per Knopfdruck gestartet werden kann.

Reportgenerierung

Neben den allgemeinen Details über Benutzer, Zeitpunkte oder Modellumgebungen erhalten Sie einen Bericht mit allen Informationen über das Profil der definierten Analysen und Beweise. Ganz nach Wunsch in HTML, TXT oder XML.
 




Kontakt

Vereinbaren Sie einen Termin mit uns.

Tel: +49 441 96 97 38-0

E-Mail: info@btc-es.de