Nicolas Markey

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.

@inproceedings{qest2004-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {{TSMV}: Symbolic Model Checking for Simply Timed
                         Systems},
  booktitle =           {{P}roceedings of the 1st {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'04)},
  acronym =             {{QEST}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {330-331},
  year =                {2004},
  month =               sep,
  doi =                 {10.1109/QEST.2004.1348052},
  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.},
}