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.

  1. Die Evaluation soll ohne umfangreiches Studium der Dokumentation des Modelcheckers in kurzer Zeit durchzuführen sein.
  2. 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.


Weitere Informationen


  • 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


  • Diplomarbeit_JP.pdf
  • Diplomarbeit „Anforderungen an einen Modelchecker für Matlab/Simulink“


Kontakt


RWTH Aachen - Lehrstuhl Informatik 11 - Ahornstr. 55 - 52074 Aachen - Deutschland