TSMV
TCTL Symbolic Model Checking of Simply-Timed Systems"); SETMAILTO("Nicolas Markey", "http://www.lsv.ens-cachan.fr/~markey/"); $locale = '_GB'; SETLANG('en'); SETHEAD("TSMV: TCTL Symbolic Model Checking of Simply-Timed Systems"); STYLELSV(); MKPAGE(); ?>

TSMV is a prototype symbolic model checker that verifies TCTL formulas on Timed Kripke Structures, i.e. finite state graphs where transitions carry a duration. These durations can be arbitrary natural numbers.

TSMV is built on top of NuSMV, the open-source symbolic model checker [CCGR00].

Specific features:

Compared to other models of timed systems, the main specific feature of TKS's is that the durations of transitions are atomic : when moving from state s to state s' via a step that lasts 10 time units, there is no intermediary configuration (and intermediary time) between s at time t and s' at time t+10. This does change the semantics of TCTL formulae but this is not a big issue when using TKS as a timed model. The key motivation for this semantics is that it leads to simple and efficient model checking algorithms. Indeed, the model checking problem is provably easier with this semantics [LMS02].

Fig. 1 - Example of a Timed Kripke Structure.

In [MS03], we proposed symbolic algorithms for checking TCTL properties (and compute minimal and maximal durations) on such models. TSMV is the resulting implementation, based on the open-source, easy-to-adapt, NuSMV model checker.

Case studies

the bridge crossing problem: demonstrating how TSMV efficiently handles long durations.
the PCI local bus: counting specific events.
a lift-controller: quantitative analysis vs. temporal verification.

Download

Only the binary file is available for the moment. It has been compiled on a Pentium4 machine running RedHat 7.3, with gcc 2.95.3, and requires no special dynamic library.

Regarding a user's manual, we refer to sections 6 and 7 of [MS03]. This assumes some familiarity with NuSMV, for which a complete user's manual is available at http://nusmv.irst.itc.it/NuSMV/userman/index-v2.html

Bibliography:

[CCGR00] Alessandro Cimatti, Edmund Clarke, Fausto Giunchiglia and Marco Roveri. NuSMV: a new symbolic model verifier. In Proc. of the 11th Int. Conf. Computer-Aided Verification (CAV'99), Trento, Italy, July 1999, volume 1633 of Lecture Notes in Computer Science, pages 495-499. Springer, 1999.

[LMS02] Fran�ois Laroussinie, Nicolas Markey and Philippe Schnoebelen. On Model Checking Durational Kripke Structures (extended abstract). In Proc. 5th Int. Conf. Foundations of Software Science and Computation Structures (FoSSaCS'2002), Grenoble, France, Apr. 2002, volume 2303 of Lecture Notes in Computer Science, pages 264-279. Springer, 2002.

[MS03] Nicolas Markey and Philippe Schnoebelen. Symbolic Model Checking of Simply-Timed Systems. Research Report LSV-03-14, Lab. Specification and Verification, ENS de Cachan, Cachan, France, October 2003.

[CCGR00]	Alessandro Cimatti, Edmund Clarke, Fausto Giunchiglia and Marco Roveri. NuSMV: a new symbolic model verifier. In Proc. of the 11th Int. Conf. Computer-Aided Verification (CAV'99), Trento, Italy, July 1999, volume 1633 of Lecture Notes in Computer Science, pages 495-499. Springer, 1999.
[LMS02]	Fran�ois Laroussinie, Nicolas Markey and Philippe Schnoebelen. On Model Checking Durational Kripke Structures (extended abstract). In Proc. 5th Int. Conf. Foundations of Software Science and Computation Structures (FoSSaCS'2002), Grenoble, France, Apr. 2002, volume 2303 of Lecture Notes in Computer Science, pages 264-279. Springer, 2002.
[MS03]	Nicolas Markey and Philippe Schnoebelen. Symbolic Model Checking of Simply-Timed Systems. Research Report LSV-03-14, Lab. Specification and Verification, ENS de Cachan, Cachan, France, October 2003.