I recently finished my bachelor thesis and will present a part of it as a short paper at the 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS) in L’Aquila, Italy.
Simulink Design Verifier vs. SPIN – A Comparative Case Study Florian Leitner and Stefan Leue
Keywords
State Space Exploration, Matlab Simulink, SPIN, Automotive SoftwareAbstract
An increasing number of industrial strength software design tools come along with verification tools that offer some property checking capabilities. On the other hand, there is a large number of general purpose model checking tools available. The question whether users of the industrial strength design tool preferably use the built-in state space exploration tool or a general purpose model checking tool arises quite naturally. Using the case study of an AUTOSAR compliant memory management module we compare the Simulink Design Verifier and the SPIN model checking tool in terms of their suitability to verify important correctness properties of this module. The comparison is both functional in that it analyzes the suitability to verify a set of basic system properties, and quantitative in comparing the computational efficiency of both tools.