Daan van Beek - Comparing the LTSmin and NuSMV reachability tools via automatic translation of their respective input languages

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
committee:prof.dr. J.C. van de Pol (1st supervisor)
G. Kant MSc
prof.dr.ir. A. Rensink
graduation date:16 August 2013 (mark: 8)


Abstract

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.