Simulink Design Verifier

Hauptmerkmale

  • Engines für die formale Analyse von Polyspace® und Prover Plug-In®
  • Erkennung von fehlerhafter Logik, Integer- und Festkommaüberläufen, Teilung durch Null und Verletzungen der Entwurfseigenschaften
  • Blöcke und Funktionen zur Modellierung funktionaler und sicherheitsspezifischer Anforderungen
  • Testvektorgenerierung aus funktionalen Anforderungen und Modellabdeckungszielen, einschließlich Bedingung, Entscheidung und Modified Condition/Decision, MCDC)
  • Eigenschaftenprüfung mit Generierung von Beispielen für Verletzungen zur Analyse und zum Debuggen
  • Unterstützung für Festkomma- und Gleitkommamodelle

Mit Simulink Design Verifier können Sie die Modellanalyse in der Simulink®-Umgebung durchführen. Damit können Sie Ihre Entwürfe verifizieren und Anforderungen frühzeitig validieren, ohne Programmcode generieren zu müssen. Daher können Sie während des gesamten Entwicklungsprozesses Verifizierungen und Validierungen durchführen. Die Modellanalyse mit Simulink Design Verifier ergänzt die Simulation, indem Sie Simulationsergebnisse als Eingaben für die Analyse mit formalen Methoden nutzen können.

Simulink Design Verifier unterstützt den zeitdiskreten Teilsatz von Simulink und Stateflow®, der in der Regel bei Entwürfen mit eingebetteter Steuerung eingesetzt wird.

Design error detection in a model using Simulink Design Verifier.
Entwurfsfehlererkennung in einem Modell mithilfe von Simulink Design Verifier. Der in Rot hervorgehobene Block weist einen Entwurfsfehler auf. Das in Grün hervorgehobene Subsystem wurde als korrekt bestätigt.

Formale Methoden in Model-Based Design

Simulink Design Verifier nutzt Verfahren der formalen Analyse, die vom Prover Plug-In von Prover Technology und der Polyspace-Engine für die formale Analyse von MathWorks bereitgestellt werden. Diese Verfahren basieren auf streng mathematischen Prozeduren, um die möglichen Ausführungspfade Ihres Modells für Testfälle und Gegenbeispiele zu durchsuchen. Im Gegensatz zu herkömmlichen Testmethoden, bei denen Testszenarien und erwartete Ergebnisse in konkreten Datenwerten ausgedrückt werden, können Sie bei formalen Analysetechniken mit Modellen des Systemverhaltens statt mit konkreten Datenwerten arbeiten. Ein Modell des Systemverhaltens kann Modelle von Testszenarien und Verifizierungszielen umfassen, die gewünschte bzw. unerwünschte Systemverhaltensweisen beschreiben. Die mit solchen Modellen durchgeführte formale Analyse ergänzt die Simulation und bietet ein tieferes Verständnis Ihres Entwurfs.

Fehlererkennung mithilfe formaler Methoden

Im Gegensatz zur semantischen Prüfung oder Analyse bei der Simulation können die in Simulink Design Verifier verwendeten formalen Methoden feststellen, ob und unter welchen Umständen spezifische dynamische Ausführungsszenarien eintreten können. Mithilfe dieser Informationen können dann entweder der Entwurf und seine Anforderungen verbessert werden, oder sie werden zur Simulation für Debugging und Validierung herangezogen. Simulink Design Verifier erfasst folgende häufige Entwurfsfehler: Integerüberlauf, Teilen durch Null, fehlerhafte Logik und Assertion-Verletzungen.

Erkennen von Integerüberlauf und Teilen durch Null

Mithilfe des Entwurfsfehlererkennungs-Modus in Simulink Design Verifier können Sie Integerüberlauf und Teilen durch Null feststellen. Die Analyse erfolgt automatisch und erfordert keinerlei zusätzliche Anwendereingriffe. Die zulässigen Bereiche für alle Signale in allen Blöcken helfen Ihnen dabei, die Ursache des Problems zu ermitteln. Am Ende der Analyse können Sie die Ergebnisse direkt im Modell oder in einem HTML-Bericht überprüfen.

Im Modell sind Blöcke grün, gelb oder rot markiert. Bei grünen Blöcken wurde bestätigt, dass sie keinen Integerüberlauf oder kein Teilen durch Null verursachen können. Gelbe Blöcke kommen vor, wenn die Analyse kein eindeutiges Ergebnis ergibt oder das Zeitlimit für die Analyse überschritten wurde. Wird im Modellausführungspfad ein Fehler festgestellt, werden alle nachfolgenden Blöcke im Pfad, die einen Integerüberlauf oder ein Teilen durch Null enthalten können, gelb markiert.

Rote Blöcke weisen Entwurfsfehler auf. Für rote Blöcke generiert Simulink Design Verifier einen Testfall, mit dem das Problem während der Simulation oder Tests reproduziert werden kann. Sie können den Testfall direkt in Simulink aufrufen und eine Simulation ausführen.

Erkennen fehlerhafter Logik

Mithilfe des Testgenerierungsmodus in Simulink Design Verifier können Sie fehlerhafte Logik erfassen, also Modellobjekte, die entweder veraltet sind oder bei denen bestätigt wurde, dass sie während der Ausführung inaktiv bleiben. Fehlerhafte Logik wird oft durch einen Entwurfs- oder Anforderungsfehler verursacht. Bei der Codegenerierung führt fehlerhafte Logik zu totem Code. Fehlerhafte Logik ist allein durch Simulationstests schwierig zu erkennen, weil es selbst nach Ausführung vieler Simulationsläufe schwierig sein kann, zu bestätigen, dass ein bestimmtes Verhalten nicht aktiviert werden kann.

Am Ende Ihrer Testgenerierungsanalyse ist das Modell den Testgenerierungskriterien entsprechend farblich gekennzeichnet. Modellobjekte, die Logik enthalten, die in der Simulation nicht aktiviert werden kann, sind rot markiert, Modellobjekte mit Logik, die vollständig in der Simulation aktiviert werden kann, werden grün gekennzeichnet. Simulink Design Verifier generiert einen Testfall, mit dem die fehlerhafte Logik bei der Simulation reproduziert werden kann.

Dead logic in a Stateflow chart detected by Simulink Design Verifier.
Von Simulink Design Verifier rot markierter Übergang in einem Stateflow-Diagramm. Dieser Übergang enthält fehlerhafte Logik, weil die Bedingung „press < zero_thresh“ nie „false“ lauten kann.

Erkennen von Assertion-Verletzungen

Mit der Verletzungserkennungs-Einstellung des Eigenschaftsbestätigungsmodus in Simulink Design Verifier können Sie Assertion-Verletzungen erkennen. Simulink Design Verifier verifiziert, ob gültige Szenarien Assertions während der Simulation innerhalb der in den Analyseeinstellungen festgelegten Anzahl von Zeitschritten auslösen können. Sie können z. B. eine Assertion erstellen, die ausgelöst wird, wenn ein Schubumkehr-Stellglied aktiviert ist und ein Flugstatus-Indikator den Wert „true“ hat. Assertions, die in gültigen Szenarien verletzt werden können, werden rot hervorgehoben, und es wird ein Testvektor erstellt, der die Assertion auslöst. Zusätzlich zu den in Simulink verfügbaren Assertions bietet Simulink Design Verifier weitere Blöcke für die Definition von Beschränkungen für die Analyse, wodurch Sie das Verhalten umfassend analysieren und Entwurfsfehler vor der Ausführung einer Simulation finden können.

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.

Modellabdeckungsanalyse

Simulink Design Verifier analysiert Algorithmen und Logik in IhrenSimulink- und Stateflow-Modellen, um Testfälle und Parameter zu generieren, die durch Industriestandards für die Entwicklung von Hochintegritätssystemen vorgegeben werden. Die Testgenerierung für strukturelle Abdeckungskriterien umfasst Bedingung, Entscheidung und Modified Condition/Decision Coverage (MC/DC).

Testgenerierung

Die Testgenerierung für die Modellabdeckung erweitert anforderungsbasierte Tests, die manuell erstellt oder bei der Simulation des kompletten Systems erfasst wurden. Bei diesem Ansatz übernimmt Simulink Design Verifier vorhandene Modellabdeckungsinformationen und generiert weitere Testvektoren, die alle Abdeckungsziele erfüllen, die während der anforderungsbasierten Tests nicht erfüllt wurden.

Visual display of a generated test vector that activates previously untested functionality.

Visuelle Anzeige eines generierten Testvektors, der zuvor nicht getestete Funktionen aktiviert.

Mithilfe dieser Testvektoren gewinnen Sie ein besseres Verständnis zu fehlenden Anforderungen und können einen vollständigeren Testumfang erstellen. Um das Testen von Modellen mit vielen Eingangs-/Ausgangsanschlüssen zu vereinfachen, identifiziert Simulink Design Verifier unbenutzte Signale und entfernt sie automatisch aus dem Testumfang.

Alle generierten Testvektoren werden als MATLAB-Struktur erfasst, die dann direkt als Eingabe für die Testausführung in der Simulation, SIL oder PIL verwendet werden kann. Die erfassten Testdaten können auch zum Generieren eines Testumfangsmodells eingesetzt werden.

Validierung generierter Testvektoren

Um generierte Testvektoren zu validieren, die die strukturellen Abdeckungskriterien erfüllen, können Sie das Modellabdeckungs-Tool von Simulink Verification and Validation verwenden. Es überwacht die Simulation und misst, ob die bei der formalen Analyse gemeldeten Ziele erfüllt wurden. Zusätzlich zu Abdeckungszielen für Bedingungs-, Entscheidungs- und MC/DC-Abdeckung meldet das Modellabdeckungs-Tool auch die Abdeckung von Testzielen, Bestätigungszielen, Annahmen, Beschränkungen, Lookup-Tabellen und Signalbereichen, die während der Simulation aufgezeichnet wurden.

Simulink Design Verifier ist vom TÜV SÜD für den Einsatz in Entwicklungsprozessen zugelassen, die den Normen ISO 26262, IEC 61508 oder EN 50128 entsprechen müssen.

Analyse der Testabdeckung von generiertem Code

Simulink Design Verifier bietet Testautomationsfunktionen für die Automatisierung der Ausführung generierter Testfälle an Code in SIL und PIL. Codeverifizierungsfunktionen in Simulink Design Verifier erfordern Embedded Coder™. Während der Textausführung können Sie die Codeabdeckungs-Tools von Embedded Coder integrieren, um die Codeabdeckung zu erfassen.

Probieren Sie Simulink Design Verifier

Testsoftware anfordern

Frühzeitige Modellabsicherung in der Systementwicklung mit Simulink

Webinar anzeigen