====== Evaluation of Model Checkers for Matlab/Simulink ======
\\
In the context of the diploma thesis Requirements for a Model Checker for Matlab/Simulink (Anforderungen an einen Modelchecker für Matlab/Simulink) a model suite has been developed that enables the evaluation of model checkers for Matlab/Simulink in short time.

=== Motivation ===

After having set the requirements, the question now is how we can check whether and which model checkers meet them. Two points are important:\\
\\
  - The evaluation must be performed in short time without the need of reading the documentation extensively.
  - The results of several such evaluations must be comparable.

=== Current Scope ===

Currently the suite contains\\
\\
  * models for checking the syntactical abilities of model checkers,
  * models for measuring the efficiency of model checkers,
  * a simulink library containing the models' basic elements and
  * a process model, that guides the user during the evaluation of a model checker.

=== Further Information ===

  * If you are interested in the suite, please contact Jacob Palczynski. The suite will be available for download on this page soon.
  * A short introduction to the suite can be found 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 ===	

  * Diploma Thesis {{:forschung:diplomarbeit_jp.pdf|"Anforderungen an einen Modelchecker für Matlab/Simulink", 2.8 MB}}

=== Contact ===

  * [[:en:lehrstuhl:mitarbeiter:palczynski]]