TCTL Symbolic Model Checking of Simply-Timed Systems

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. |

- Private Pages
- Page maintained by Nicolas Markey.