Title :
TSMV: a symbolic model checker for quantitative analysis of systems
Author :
Markey, Nicolas ; Schnoebelen, Philippe
Author_Institution :
Lab. d´´Inf., Univ. Libre de Bruxelles, Belgium
Abstract :
TSMV 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.
Keywords :
formal verification; public domain software; systems analysis; Kripke structures; quantitative system analysis; symbolic algorithms; symbolic model checker; Bridges; Circuits; Delay; Encoding; Lamps; Logic; Open source software; Programmable control; Protocols; Reactive power;
Conference_Titel :
Quantitative Evaluation of Systems, 2004. QEST 2004. Proceedings. First International Conference on the
Print_ISBN :
0-7695-2185-1
DOI :
10.1109/QEST.2004.1348052
