====== Requirements for a Model Checker for Matlab/Simulink  ======
~~NOTOC~~
\\
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.

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