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 [1], 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 [2] provides the two cornerstone results which are at the basis of the current version. The model checker has been evaluated and validated against PRISM [3] (for whose CSLTA formulas which can be expressed in CSL) and against the statistical model checker Cosmos[4] (for all types of formulas).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Amparore, E.G., Donatelli, S.: MC4CSLTA: an efficient model checking tool for CSLTA. In: International Conference on Quantitative Evaluation of Systems, pp. 153–154. IEEE Computer Society, Los Alamitos (2010)
Amparore, E.G., Donatelli, S.: A component-based solution for reducible markov regenerative processes. Performance Evaluation 70, 400–422 (2013)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic Model Checking for Performance and Reliability Analysis. Performance Evaluation 36, 40–45 (2009)
Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a statistical model checker for the hybrid automata stochastic logic. In: Proceedings of the 8th International Conference on Quantitative Evaluation of Systems (QEST 2011), pp. 143–144. IEEE Computer Society Press, Aachen (2011)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Transactions on Computational Logic 1, 162–170 (2000)
Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Performance Evaluation 68, 90–104 (2011)
Heiner, M., Rohr, C., Schwarick, M.: Marcie - model checking and reachability analysis done efficiently. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 389–399. Springer, Heidelberg (2013)
Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSLTA. IEEE Transactions on Software Engineering 35, 224–240 (2009)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Comp. Science 126, 183–235 (1994)
Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Model checking of continuous-time Markov chains against timed automata specifications. Logical Methods in Computer Science 7 (2011)
Barbot, B., Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Efficient ctmc model checking of linear real-time objectives. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 128–142. Springer, Heidelberg (2011)
Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: HASL: An expressive language for statistical verification of stochastic models. In: Proceedings of the 5th International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS 2011), Cachan, France, pp. 306–315 (2011)
Amparore, E.G.: States, actions and path properties in Markov chains. PhD thesis, University of Torino, Italy (2013)
German, R.: Iterative analysis of Markov regenerative models. Performance Evaluation 44, 51–72 (2001)
Amparore, E.G., Donatelli, S.: Revisiting the Iterative Solution of Markov Regenerative Processes. Numerical Linear Algebra with Applications, Special Issue on Numerical Solutions of Markov Chains 18, 1067–1083 (2011)
Amparore, E.G., Donatelli, S.: Model Checking CSLTA with Deterministic and Stochastic Petri Nets. In: Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE Computer Society Press (2010); DSN-PDS 2010
Amparore, E.G., Donatelli, S.: The MC4CSLTA model checker (2013), http://www.di.unito.it/~amparore/mc4cslta/
Baarir, S., Beccuti, M., Cerotti, D., Pierro, M.D., Donatelli, S., Franceschinis, G.: The GreatSPN tool: recent enhancements. SIGMETRICS Performance Evaluation Review 36, 4–9 (2009)
Lecca, Priami: Cell Cycle Control in Eukaryotes - Prism case studies (2011), http://www.prismmodelchecker.org/casestudies/cyclin.php
Lecca, P., Priami, C.: Cell cycle control in eukaryotes: A BioSpi model. In: Proc. Workshop on Concurrent Models in Molecular Biology (BioConcur 2003). Electronic Notes in Theoretical Computer Science (2003)
van der Aalst, W.M.P.: Business process management demystified: A tutorial on models, systems and standards for workflow management. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 1–65. Springer, Heidelberg (2004)
Amparore, E.G., Ballarini, P., Beccuti, M., Donatelli, S., Franceschinis, G.: Expressing and Computing Passage Time Measures of GSPN models with HASL. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 110–129. Springer, Heidelberg (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amparore, E.G., Donatelli, S. (2013). Improving and Assessing the Efficiency of the MC4CSLTA Model Checker. In: Balsamo, M.S., Knottenbelt, W.J., Marin, A. (eds) Computer Performance Engineering. EPEW 2013. Lecture Notes in Computer Science, vol 8168. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40725-3_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-40725-3_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40724-6
Online ISBN: 978-3-642-40725-3
eBook Packages: Computer ScienceComputer Science (R0)