Open AccessTSMV: A Symbolic Model Checker for Quantitative Analysis of Systems
Author(s) -
Nicolas Markey,
Philippe Schnoebelen
Publication year - 2004
Publication title -
hal (le centre pour la communication scientifique directe)
Language(s) - English
Resource type - Conference proceedings
DOI - 10.1109/qest.2004.10028
Subject(s) - computer science , model checking , programming language , symbolic trajectory evaluation , theoretical computer science , software engineering
International audienceTSMV is an extension of NuSMV, the open-source symbolic model checker, aimed at dealing with timed versions of (models of) circuits, PLC controllers, protocols, etc. The underlying model is an extension of Kripke structures, where every transition carries an integer duration (possibly zero). This simple model supports efficient symbolic algorithms for RTCTL formulae
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom