Model Checking

BTC Embedded Systems ist sicherlich ein Pionier im Zusammenhang mit der Integration von Model Checking Technologie in kommerzielle Entwicklungswerkzeuge. Indem wir diese hochautomatisierte Technologie für die Industrie verfügbar machen, tragen wir zu einer signifikanten Steigerung von Effizienz und Qualität in den Entwicklungsprojekten unserer Kunden bei. 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.

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 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.

Model Checking Technologie wird in verschiedenen, hochautomatisierten Use-Cases in der BTC EmbeddedPlatform eingesetzt. Ein Beispiel ist die Generierung struktureller Test-Daten für vollständige Code Coverage im BTC EmbeddedTester. In einem solchen Use Case ist das Ziel nicht, 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 Entscheidung 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 den BTC EmbeddedTester BASE, welches Model Checking verwendet um funktionale Testfälle aus formalisierten Requirements zu generieren. Schließlich nutzt BTC EmbeddedValidator die Model Checking Technologie um automatisch einen vollständigen mathematischen Beweis zu erstellen der zeigt, dass ein bestimmtes Requirement nicht vom zu testenden System verletzt werden kann.