TSMV: A symbolic model checker for quantitative analysis of systems. 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.
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Lepri, Daniela; Ábrahám, Erika; Ölveczky, Peter Csaba: A timed CTL model checker for real-time maude (2013) ioport
- Lepri, Daniela; Ábrahám, Erika; Ölveczky, Peter Csaba: Timed CTL model checking in Real-Time Maude (2012)