Model Checking Timed and Stochastic Properties with CSL\textsuperscriptTA

Susanna Donatelli Serge Haddad 1 Jeremy Sproston
1 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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. Systems can be modelled directly as Markov chains, or with a higher-level formalism for which Markov chains represent the underlying semantics. Markov chains are widely used to study the performance of computer and telecommunication systems. 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. Furthermore, the choice of using automata rather than the classical temporal operators Next and Until should help in enlarging the accessibility of model checking to a larger public. We also present a model-checking algorithm for CSLTA.
Type de document :
Article dans une revue
IEEE Transactions on Software Engineering, Institute of Electrical and Electronics Engineers, 2009, 35 (2), pp.224-240. 〈10.1109/TSE.2008.108〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00772639
Contributeur : Stefan Haar <>
Soumis le : jeudi 10 janvier 2013 - 20:28:19
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Identifiants

Collections

Citation

Susanna Donatelli, Serge Haddad, Jeremy Sproston. Model Checking Timed and Stochastic Properties with CSL\textsuperscriptTA. IEEE Transactions on Software Engineering, Institute of Electrical and Electronics Engineers, 2009, 35 (2), pp.224-240. 〈10.1109/TSE.2008.108〉. 〈hal-00772639〉

Partager

Métriques

Consultations de la notice

141