• DocumentCode
    1666024
  • 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
  • fYear
    2004
  • Firstpage
    330
  • Lastpage
    331
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Quantitative Evaluation of Systems, 2004. QEST 2004. Proceedings. First International Conference on the
  • Print_ISBN
    0-7695-2185-1
  • Type

    conf

  • DOI
    10.1109/QEST.2004.1348052
  • Filename
    1348052
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1666024