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