CSLTA is a stochastic logic which is able to express properties on the behavior of a CTMC, in particular in terms of the possible executions of the CTMC (like the probability that the set of paths that exhibits a certain behavior is above/below a certain threshold). This paper presents the new version of the the stochastic model checker MC4CSLTA, which verifies CSLTA formulas against a Continuous Time Markov Chain, possibly expressed as a Generalized Stochastic Petri Net. With respect to the first version of the model checker presented in, version 2 features a totally new solution algorithm, which is able to verify complex, nested formulas based on the timed automaton, while, at the same time, is capable of reaching a time and space complexity similar to that of the CSL model checkers when the automaton specifies a neXt or an Until formulas. In particular, the goal of this paper is to present a new way of generating the MRP, which, together with the new MRP solution method presented in provides the two cornerstone results which are at the basis of the current version. The model checker has been evaluated and validated against PRISM (for whose CSLTA formulas which can be expressed in CSL) and against the statistical model checker Cosmos (for all types of formulas).

Improving and Assessing the Efficiency of the MC4CSLTA Model Checker

AMPARORE, ELVIO GILBERTO;Donatelli, Susanna
2013-01-01

Abstract

CSLTA is a stochastic logic which is able to express properties on the behavior of a CTMC, in particular in terms of the possible executions of the CTMC (like the probability that the set of paths that exhibits a certain behavior is above/below a certain threshold). This paper presents the new version of the the stochastic model checker MC4CSLTA, which verifies CSLTA formulas against a Continuous Time Markov Chain, possibly expressed as a Generalized Stochastic Petri Net. With respect to the first version of the model checker presented in, version 2 features a totally new solution algorithm, which is able to verify complex, nested formulas based on the timed automaton, while, at the same time, is capable of reaching a time and space complexity similar to that of the CSL model checkers when the automaton specifies a neXt or an Until formulas. In particular, the goal of this paper is to present a new way of generating the MRP, which, together with the new MRP solution method presented in provides the two cornerstone results which are at the basis of the current version. The model checker has been evaluated and validated against PRISM (for whose CSLTA formulas which can be expressed in CSL) and against the statistical model checker Cosmos (for all types of formulas).
2013
Computer Performance Engineering: 10th European Workshop, EPEW2013
Venezia
September 16-17, 2013
Computer Performance Engineering: 10th European Workshop, EPEW 2013, Venice, Italy, September 16-17, 2013. Proceedings
Springer Berlin Heidelberg
8168
206
220
978-3-642-40725-3
http://dx.doi.org/10.1007/978-3-642-40725-3_16
stochastic model checking
Amparore, Elvio Gilberto; and Donatelli, Susanna
File in questo prodotto:
File Dimensione Formato  
Amparore-Donatelli-EPEW2013.pdf

Accesso aperto

Descrizione: Articolo principale
Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 1.58 MB
Formato Adobe PDF
1.58 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/1624731
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact