• DocumentCode
    2550709
  • Title

    MC4CSLTA: An Efficient Model Checking Tool for CSLTA

  • Author

    Gilberto, Elvio Amparore ; Donatelli, Susanna

  • Author_Institution
    Dipt. di Inf., Univ. di Torino, Torino, Italy
  • fYear
    2010
  • fDate
    15-18 Sept. 2010
  • Firstpage
    153
  • Lastpage
    154
  • Abstract
    This demo presents MC4CSLTA, an efficient Markov chain Model Checker for (four) the stochastic logic CSLTA. In CSLTA formulas are either steady state queries or path formulas, where accepting paths are specified through a Deterministic Timed Automata (DTA). MC4CSLTA takes as input a labeled CTMC, a query, one or more DTA involved in the query (possibly expressed in parametric form), and computes the needed probability to assess the truth value of the formula. MC4CSLTA is written in C++, and is publicly available for the research community.
  • Keywords
    Markov processes; deterministic automata; formal logic; formal verification; CSLTA stochastic logic; MC4CSLTA model checking tool; Markov chain model checker; deterministic timed automata; Computational modeling; Electromagnetic compatibility; Markov processes; Materials requirements planning; Servers; Steady-state; CSLTA; model checker;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Quantitative Evaluation of Systems (QEST), 2010 Seventh International Conference on the
  • Conference_Location
    Williamsburg, VA
  • Print_ISBN
    978-1-4244-8082-1
  • Type

    conf

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