|author:||Daan van Beek|
|title:||Comparing the LTSmin and NuSMV reachability tools via automatic translation of their respective input languages|
|keywords:||Symbolic Model Checking, LTSmin, NuSMV, reachability|
Jaco van de Pol
Gijs Kant ,
In this thesis we:
- Provide automatic translations from SMV to an LTSmin input language.
- Formalize and prove these translations to be correct.
- Use the translations to translate several SMV models to mCRL2 models and execute them on SMV and LTSmin in order to obtain experimental results.
- Explain the results by using the theory behind the NuSMV and LTSmin reachability tools.