====== Anforderungen an einen Modelchecker für Matlab/Simulink ======
~~NOTOC~~
\\
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.

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

===== Kontakt =====

  * [[:lehrstuhl:mitarbeiter:palczynski]]