Model Checking

Eine vollständige mathematische Analyse von Ansi-C Seriencode.

Model Checking

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.

Was ist Model Checking?

Model Checking entstand in den 1980er Jahren und sollte nicht mit dem Prüfen von Modelling Guidelines in Umgebungen wie Simulink verwechselt werden. Zwei Gruppen in den USA (Clark, Emmerson, McMillan) und in Frankreich (Quielle, Sifakis) entwickelten unabhängig voneinander ein effizientes Suchverfahren für endliche Automaten, um festzustellen, ob sie eine in temporaler Logik ausgedrückte Spezifikation erfüllen. Später wurde der Ansatz durch Konzepte wie „Symbolic Model Checking“ und „Reduced Ordered Binary Decision Diagrams“ verfeinert.

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.

Wie sieht die Integration von Model Checking in der BTC EmbeddedPlatform aus?

Die BTC EmbeddedPlatform kombiniert verschiedene Model Checking Methoden wie Binary Decision Diagrams und SAT-Solver. Abhängig vom zu testenden System wird die passende Methode auf intelligente Weise ausgewählt. Der Input und die semantische Grundlage des Model Checkings in der BTC EmbeddedPlatform ist ANSI C-Code, so dass die Technologie sowohl bei modellbasierter Entwicklung mit automatischer Code-Generierung, als auch bei handgeschriebenem Code zum Einsatz kommen kann.

Welche Use Cases nutzen Model Checking in der BTC EmbeddedPlatform?

Die Model Checking Technologie wird in verschiedenen, hochautomatisierten Use Cases in der BTC EmbeddedPlatform eingesetzt. Ein Beispiel ist die Generierung struktureller Testdaten für vollständige Code Coverage im BTC EmbeddedTester. In einem solchen Use Case ist es nicht das Ziel, die Abwesenheit von Fehlern zu zeigen, sondern die Erstellung von Gegenbeispielen auszunutzen, um strukturelle Testfälle in Form von Stimuli Vektoren zu erhalten. Dazu werden sogenannte „Trap Properties“ verwendet, die bspw. behaupten, eine Decision in einem If-Statement sei nicht erreichbar (=dead code). Der Model Checker prüft diese Trap Property und findet ein Gegenbeispiel: einen strukturellen Testfall der diese Decision erreicht.

Ein weiterer Anwendungsfall ist das Requirements-based Test Generation Add-On für BTC EmbeddedTester BASE, welches Model Checking verwendet, um funktionale Testfälle aus formalisierten Requirements zu generieren. Außerdem nutzt BTC EmbeddedValidator die Model Checking Technologie, um automatisch einen vollständigen mathematischen Beweis zu erstellen, der zeigt, dass ein bestimmtes Safety-Requirement vom zu testenden System nie verletzt werden kann.