The Community for Technology Leaders
Green Image
Issue No. 02 - March/April (2009 vol. 35)
ISSN: 0098-5589
pp: 224-240
Jeremy Sproston , Università di Torino, Torino
Serge Haddad , LSV, CBRS and École Normale Supérieure de Cachan, Cachan
Susanna Donatelli , Università di Torino, Torino
ABSTRACT
Markov chains are a well-known stochastic process that provide a balance between being able to adequately model the system's behavior and being able to afford the cost of the model solution. The definition of stochastic temporal logics like Continuous Stochastic Logic (CSL) and its variant asCSL, and of their model-checking algorithms, allows a unified approach to the verification of systems, allowing the mix of performance evaluation and probabilistic verification. In this paper we present the stochastic logic CSLTA, which is more expressive than CSL and asCSL, and in which properties can be specified using automata (more precisely, timed automata with a single clock). The extension with respect to expressiveness allows the specification of properties referring to the probability of a finite sequence of timed events. A typical example is the responsiveness property "with probability at least 0.75, a message sent at time 0 by a system A will be received before time 5 by system B and the acknowledgment will be back at A before time 7", a property that cannot be expressed in either CSL or asCSL. We also present a model-checking algorithm for CSLTA.
INDEX TERMS
Model checking, Markov processes, Temporal logic
CITATION
Jeremy Sproston, Serge Haddad, Susanna Donatelli, "Model Checking Timed and Stochastic Properties with CSL^{TA}", IEEE Transactions on Software Engineering, vol. 35, no. , pp. 224-240, March/April 2009, doi:10.1109/TSE.2008.108
100 ms
(Ver )