Simulink Design Verifier

Verifizierung von Entwürfen in Bezug auf die Anforderungen

Funktionale Anforderungen für diskrete Systeme sind in der Regel explizite Anweisungen zum erwarteten Verhalten eines Systems sowie zu Verhaltensweisen, die nie vorkommen dürfen. Verhaltensweisen, die nie vorkommen dürfen, werden als Sicherheitsanforderungen bezeichnet.

Ausdrücken funktionaler Anforderungen in Simulink

Um formal zu verifizieren, dass sich der Entwurf diesen Anforderungen entsprechend verhält, müssen die Anforderungsanweisungen zunächst aus einer menschlichen Sprache in die Sprache übersetzt werden, die die Engine für formale Analyse versteht. Mit Simulink Design Verifier können Sie formale Anforderungen mithilfe von Simulink, MATLAB®-Funktionen und Stateflow ausdrücken. Jeder Anforderung in Simulink sind ein oder mehrere Verifizierungsziele zugeordnet. Diese Verifizierungsziele dienen dazu, zu melden, ob der Entwurf die funktionalen und Sicherheitsanforderungen erfüllt oder nicht.

Simulink Design Verifier stellt einen Satz von Bausteinen und Funktionen bereit, mit denen Sie Verifizierungsziele definieren und organisieren können. Die bereitgestellte Blockbibliothek umfasst Blöcke und Funktionen für Testziele, Bestätigungsziele, Assertions, Beschränkungen und einen dedizierten Satz temporaler Operatoren für die Modellierung von Verifizierungszielen mit temporalen Aspekten.

Sie können einzelne Anforderungen und deren zugeordnete Verifizierungsziele in Bibliotheken gruppieren, die Sie unabhängig vom Entwurf verwalten und prüfen können.

Simulink Design Verifier library of property examples.
Simulink Design Verifier-Bibliothek mit Eigenschaftsbeispielen.

Wenn Sie Simulink Design Verifier mit dem Requirements Management Interface in Simulink Verification and Validation™ verwenden, können Sie Blöcke und Funktionen, die zum Erfassen von Anforderungen und Verifizierungszielen dienen, mit den textbasierten Anforderungen außerhalb von Simulink verknüpfen.

Bestätigen von Entwürfen anhand der Anforderungen

Wenn Anforderungen und Verifizierungsziele im Verifizierungsmodell erfasst wurden, können sie zum Bestätigen der Richtigkeit eines Entwurfs mithilfe formaler Methoden herangezogen werden.

Um die Verifizierung funktionaler Anforderungen durchzuführen und Ihr System in den gewünschten Zustand zu bringen, können Sie Testzielblöcke und MATLAB-Funktionen zur Definition von Testzielen verwenden. Während der Testgenerierung versucht Simulink Design Verifier, einen gültigen Testfall zu finden, der die angegebenen Ziele erfüllt. Kann ein Ziel nie erfüllt werden, kann der Entwurf die erforderlichen Funktionen für einen bestimmten Satz von Analysebeschränkungen nicht ausführen.

Um zu verifizieren,dass Ihr Entwurf den Sicherheitsanforderungen entspricht, können Sie Proof Objective-Blöcke und MATLAB-Funktionen zur Definition der Bestätigungsziele verwenden. Bei der Analyse untersucht Simulink Design Verifier alle möglichen Eingabebedingungen, die das unerwünschte Verhalten verursachen können, und meldet die Ergebnisse dann. Für ein bestimmtes Bestätigungsziel kann der Entwurf als gültig bestätigt werden, oder es wird ermittelt, dass er die Sicherheitsanforderungen verletzt. Wird eine Verletzung festgestellt, generiert Simulink Design Verifier einen Testvektor, der die Verletzung in der Simulation demonstrieren kann.

Simulink Design Verifier report for verifying a design against safety requirements represented with proof objectives.
Simulink Design Verifier-Bericht zur Verifizierung eines Entwurfs anhand der durch Bestätigungsziele repräsentierten Sicherheitsanforderungen. Der Bericht zeigt die Liste der Ziele, für die der Entwurf als gültig bestätigt wurde, sowie die Liste der Ziele, für die die Analyse Gegenbeispiele fand.

Validieren der Analyseergebnisse

Mit Simulink, MATLAB-Funktionen und Stateflow ausgedrückte Anforderungen können parallel mit dem Entwurf simuliert werden. Sie können damit auch den generierten Code verifizieren, indem Sie eine Kosimulation im SIL- oder PIL-Modus durchführen. Das Modellabdeckungs-Tool sammelt Informationen über die Aktivierung von Verifizierungszielen während der Simulation und liefert Abdeckungsergebnisse über die Abdeckungsmetrik von Simulink Design Verifier. Sie können die Ursachenanalyse und das Debugging beschleunigen, indem Sie Bestätigungsziele verwenden, die Sicherheitsanforderungen repräsentieren, um die Simulation sofort bei deren Verletzung anzuhalten.

Weiter: Modellabdeckungsanalyse

Probieren Sie Simulink Design Verifier

Testsoftware anfordern

Modellbasierte Entwicklung und Testen von Steuerungs- und Überwachungs-Logiken

Webinar anzeigen