Abstract
Given the description of a model and a probabilistic formula, approximate model checking is a verification technique based on statistical reasoning that allows answering whether or not the model satisfies the formula. Only a subset of the properties that can be analyzed by exact model checking can be attacked by approximate methods. These latest methods, though, being based on simulation and sampling have the advantage of not requiring the generation of the complete state-space of the model.
Here we describe an efficient tool for the approximate model checking of services written in a stochastic variant of COWS, a process calculus for the orchestration of services.
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.
Similar content being viewed by others
References
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continous-time Markov chains. ACM Trans. on Computational Logic 1(1), 162–170 (2000)
Cappello, I., Quaglia, P.: A Tool for Checking Probabilistic Properties of COWS Services. In: Proceedings of TGC 2010 (2010), http://disi.unitn.it/~cappello/
De Nicola, R., Latella, D., Loreti, M., Massink, M.: MarCaSPiS: a Markovian Extension of a Calculus for Services. Electronic Notes in Theoretical Computer Science 229(4), 11–26 (2009)
Fujita, M., McGeer, P.C., Yang, J.C.-Y.: Multi-Terminal Binary Decision Diagrams: An efficient data structure for matrix representation. Formal Methods in System Design 10, 149–169 (1997)
Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 307–329. Springer, Heidelberg (2004)
Hérault, T., Lassaigne, R., Peyronnet, S.: APMC 3.0: Approximate Verification of Discrete and Continuous Time Markov Chains. In: Proc. 3rd Int. Conf. on Quantitative Evaluation of Systems, QEST 2006, pp. 129–130. IEEE, Los Alamitos (2006)
Hermanns, H., Herzog, U., Katoen, J.-P.: Process algebra for performance evaluation. Theoretical Computer Science 274(1-2), 43–87 (2002)
Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: Plateau, B., Stewart, W., Silva, M. (eds.) Proc. 3rd International Workshop on Numerical Solution of Markov Chains (NSMC 1999), pp. 188–207. Prensas Universitarias de Zaragoza (1999)
Hillston, J.: A compositional approach to performance modelling. Cambridge University Press, New York, NY, USA (1996)
Hoeffding, W.: Probability inequalities for sums of bounded random variables. Journal of the American Statistical Association 58(301), 13–30 (1963)
Younes, H.L.: Verification and Planning for Stochastic Processes with Asynchronous Events. PhD thesis, Computer Science Department, Carnegie Mellon University, Pittsburgh, Pennsylvania (2005)
Kuntz, G.W.M.: Symbolic Semantics and Verification of Stochastic Process Algebras. PhD thesis, Friedrich-Alexander-Universitaet Erlangen-Nuernberg, Erlangen (March 2006)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic Model Checking for Performance and Reliability Analysis. ACM SIGMETRICS Performance Evaluation Review 36(4), 40–45 (2009)
Lapadula, A., Pugliese, R., Tiezzi, F.: Calculus for Orchestration of Web Services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 33–47. Springer, Heidelberg (2007), http://rap.dsi.unifi.it/cows/
Prandi, D., Quaglia, P.: Stochastic COWS. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 245–256. Springer, Heidelberg (2007)
PRISM homepage, http://www.prismmodelchecker.org/
Schivo, S.: Statistical model checking of Web Services. PhD thesis, Int. Doctorate School in Information and Communication Technologies, University of Trento (2010)
Wald, A.: Sequential tests of statistical hypotheses. The Annals of Mathematical Statistics 16(2), 117–186 (1945)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Quaglia, P., Schivo, S. (2010). Approximate Model Checking of Stochastic COWS. In: Wirsing, M., Hofmann, M., Rauschmayer, A. (eds) Trustworthly Global Computing. TGC 2010. Lecture Notes in Computer Science, vol 6084. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15640-3_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-15640-3_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15639-7
Online ISBN: 978-3-642-15640-3
eBook Packages: Computer ScienceComputer Science (R0)