Subscribe
Issue No.02 - March/April (2009 vol.35)
pp: 224-240
Susanna Donatelli , Università di Torino, Torino
Serge Haddad , LSV, CBRS and École Normale Supérieure de Cachan, Cachan
Jeremy Sproston , 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
Susanna Donatelli, Serge Haddad, Jeremy Sproston, "Model Checking Timed and Stochastic Properties with CSL^{TA}", IEEE Transactions on Software Engineering, vol.35, no. 2, pp. 224-240, March/April 2009, doi:10.1109/TSE.2008.108
REFERENCES
 [1] C. Smith, Performance Engineering of Software Systems. Addison-Wesley, 1990. [2] UML Profile for Schedulabibity, Performance and Time Specification, Object Management Group, version 1.1, formal/05-01-02, Jan. 2005, [3] A UML Profile for Modeling and Analysis of Real Time Embedded Systems (MARTE), OMG, revised submission, 2007. [4] V. Cortellessa and R. Mirandola, “Deriving a Queuing Network Based Performance Model from UML Diagrams,” Proc. ACM Workshop Software and Performance, pp.58-70, Sept. 2000. [5] S. Bernardi and J. Merseguer, “Performance Evaluation of Uml Design with Stochastic Well-Formed Nets,” J. Systems and Software, vol. 80, no. 11, pp.1843-1865, Nov. 2007. [6] C. Canevet, S. Gilmore, J. Hillston, M. Prowse, and P. Stevens, “Performance Modelling with UML and Stochastic Process Algebras,” IEEE Proc.: Computers and Digital Techniques, vol. 150, no. 2, pp.107-120, Mar. 2003. [7] S. Balsamo, A. Di Marco, P. Inverardi, and M. Simeoni, “Model-Based Performance Prediction in Software Development: A Survey,” IEEE Trans. Software Eng., vol. 30, no. 5, pp.295-310, May 2004. [8] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, “Model-Checking Continuous Time Markov Chains,” ACM Trans. Computational Logic, vol. 1, no. 1, pp.162-170, 2000. [9] C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen, “Model-Checking Algorithms for Continuous-Time Markov Chains,” IEEE Trans. Software Eng., vol. 29, no. 6, pp.524-541, June 2003. [10] C. Baier, L. Cloth, B. Haverkort, M. Kuntz, M. Siegle, “Model Checking Action- and State-Labelled Markov Chains,” IEEE Trans. Software Eng., vol. 33, no. 4, pp.209-224, Apr. 2007. [11] M.Y. Vardi and P. Wolper, “Reasoning About Infinite Computations,” Information and Computation, vol. 115, no. 1, pp.1-37, 1994. [12] E.M. Clarke, O. Grumberg, and R.P. Kurshan, “A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems,” J. Logic Computation, vol. 2, no. 5, pp.605-618, 1992. [13] R. Alur and D.L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, no. 2, pp.183-235, 1994. [14] G. Behrmann, A. David, K.G. Larsen, J. Håkansson, P. Pettersson, W. Yi, and M. Hendriks, “UPPAAL 4.0,” Proc. IEEE Quantitative Evaluation of Systems, pp.125-126. [15] R. Alur, C. Courcoubetis, and D.L. Dill, “Model-Checking in Dense Real-Time,” Information and Computation, vol. 104, no. 1, pp.2-34, 1993. [16] R. Alur, T. Feder, and T.A. Henzinger, “The Benefits of Relaxing Punctuality,” J. ACM, vol. 43, no. 1, pp.116-146, 1996. [17] E.A. Emerson and J.Y. Halpern, ““Sometimes” and “Not Never” Revisited: On Branching Versus Linear Time Temporal Logic,” J.ACM, vol. 33, no. 1, pp.151-178, 1986. [18] G. Clark and J. Hillston, “Towards Automatic Derivation of Performance Measures from PEPA Models,” Proc. UK Performance Eng. Workshop, 1996. [19] W.D. Obal II and W.H. Sanders, “State-Space Support for Path-Based Reward Variables,” Performance Evaluation, vol. 35, nos.3/4, pp.233-251, 1999. [20] A. Bouajjani, Y. Lakhnech, and S. Yovine, “Model-Checking for Extended Timed Temporal Logics,” Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems, pp.306-325, 1996. [21] F. Laroussinie, N. Markey, and P. Schnoebelen, “Model Checking Timed Automata with One or Two Clocks,” Proc. Conf. Concurrency Theory, pp.387-401, 2004. [22] J. Ouaknine and J. Worrell, “On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap,” Proc. IEEE Logic in Computer Science, pp.54-63, 2004. [23] S. Donatelli, S. Haddad, and J. Sproston, “${\rm CSL}^{{\rm TA}}$ : An Expressive Logic for Continuous-Time Markov Chains,” Proc. IEEE Quantitative Evaluation of Systems, pp.31-40, 2007. [24] S. Yovine, “KRONOS: A Verification Tool for Real-Time Systems,” Software Tools for Technology Transfer, vol. 1, nos.1/2, pp.123-133, 1997. [25] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. MIT Press, 1999. [26] R. German, Performance Analysis of Communication Systems with Non-Markovian Stochastic Petri Nets. Wiley, 2000. [27] M. Ajmone Marsan and G. Chiola, “On Petri Nets with Deterministic and Exponentially Distributed Firing Times,” Proc. Int'l Conf. Application and Theory of Petri Nets and Other Models of Concurrency, pp.132-145, 1986. [28] A. Jensen, “Markov Chains as An aid in the Study of Markov Processes,” Skandinavisk Aktuarietidskrift, vol. 36, pp.87-91, 1953. [29] C. Lindemann, Performance Modelling with Deterministic and Stochastic Petri Nets. Wiley, 1998. [30] B. Haverkort, L. Cloth, H. Hermanns, J.-P. Katoen, and C. Baier, “Model Checking Performability Properties,” Proc. IEEE Int'l Conf. Dependable Systems and Networks, pp.103-112, 2002.