<< EEMCS (EWI)
Home News and Events People Research Education    » Courses    » ST Master    » BSc Projects    » MSc Projects    » Design Projects    » Internships Vacancies Intranet Contact
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
topics:
committee: Jaco van de Pol ,
Gijs Kant ,
Arend Rensink
started: February 2013
end: August 2013

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.

 

Additional Resources

  1. The paper