Evaluation von Matlab/Simulink-Modelcheckern
Im Rahmen der Diplomarbeit Anforderungen an einen Modelchecker für Matlab/Simulink an unserem Lehrstuhl entstand eine Modellsuite, mit der Modelchecker für Matlab/Simulink schnell bewertet werden können.
Motivation
Nachdem die Anforderungen formuliert worden sind, stellt sich die Frage, wie überprüft werden kann, ob und welche Modelchecker diese erfüllen. Wichtig sind dabei zwei Punkte.
Die Evaluation soll ohne umfangreiches Studium der Dokumentation des Modelcheckers in kurzer Zeit durchzuführen sein.
Die Ergebnisse mehrerer solcher Evaluationen sollen vergleichbar sein.
Aktueller Umfang
Aktuell umfasst diese Suite
Modelle für die Überprüfung syntaktischer Fähigkeiten der Modelchecker,
Modelle für die Messung der Effizienz der Modelchecker,
eine Simulink-Bibliothek, in der die Grundbausteine der Suitemodelle abgelegt sind und
ein Vorgehensmodell, dass den Benutzer durch den Evaluierungsprozess leitet.
Wenn Sie Interesse an der Suite haben, wenden Sie sich bitte an
Jacob Palczynski. Bald wird es auch möglich sein, die Suite von hier herunterzuladen.
Eine Kurzvorstellung der Suite finden Sie in: Jacob Palczynski, Bastian Schlich, and Stefan Kowalewski. Eine Evaluationssuite zur schnellen Bewertung von Matlab/Simulink-Modelcheckern. 4. Workshop Automotive Software Engineering. In Informatik 2006: Informatik für Menschen, Band 1. Volume P-93 of Lecture Notes in Informatics (LNI). 2006.
Downloads
Kontakt