Abstract
Creol is an executable, formally defined modeling language with advanced object-oriented features, tailored for modeling software systems consisting of physically distributed components, each running on its own processor and communicating by means of asynchronous method calls. Creol is oriented towards qualitative analysis, abstracting away from underlying software and hardware system properties. In this paper we propose a probabilistic extension of Creol, oriented towards quantitative analysis, called PCreol, and give its operational semantics by means of probabilistic rewrite theories. This extension is motivated by the need to model a) communication over networks of different quality, b) software components running randomized algorithms, c) independent processor speeds, d) process scheduling, and e) an open environment exhibiting probabilistic behavior. The syntax of PCreol therefore includes means for modeling random expressions, a probabilistic choice operator, random assignment, call statements with priorities, and object creation statements that set an object’s computation speed, as well as its quality of communication with other objects. We give details on the implementation of a prototype PCreol interpreter—on top of the existing one for Creol—which is executable in Maude. Furthermore, we integrate PCreol with the VeStA tool, to support probabilistic reasoning of PCreol models by statistical model checking and quantitative analysis. By probabilistic modeling of independent processor speeds, representative runs of a PCreol model are obtained using discrete-event simulation, and the model checking problem of large models becomes feasible. We provide concrete examples of PCreol models and show how VeStA can be used to reason about them.
Partially supported by the EU project FP7-231620 HATS: Highly Adaptable and Trustworthy Software using Formal Models (http://www.hats-project.eu).
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
Ábrahám, E., Grabe, I., Grüner, A., Steffen, M.: Behavioral interface description of an object-oriented language with futures and promises. J. Log. Algebr. Program. 78(7), 491–518 (2009)
Agha, G.: Actors: A model of concurrent computation in distributed systems. MIT Press, Cambridge (1986)
Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. Electronic Notes in Theoretical Computer Science 153(2), 213–239 (2006); Proc. 3rd Workshop on Quantitative Aspects of Programming Languages (QAPL 2005)
AlTurki, M., Meseguer, J.: PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying Continuous Time Markov Chains. In: Alur, R., Henzinger, T. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)
Baier, C., Ciesinski, F., Grosser, M.: PROBMELA: A modeling language for communicating probabilistic processes. In: Proc. 2nd ACM and IEEE Intl. Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), pp. 57–66 (2004)
Bentea, L., Owe, O.: Towards an object-oriented modeling language for probabilistic open distributed systems. Technical Report 397, Univ. of Oslo (2010), http://www.ifi.uio.no/~lucianb/publications/2010/pcreol.pdf
Bjørk, J., Johnsen, E.B., Owe, O., Schlatte, R.: Lightweight time modeling in Timed Creol. Electronic Proceedings in Theoretical Computer Science 36, 67–81 (2010); Proc. 1st Intl. Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
den Hartog, J.: Probabilistic Extensions of Semantical Models. Ph.D. thesis, Vrije Univ., Amsterdam (2002)
Holzmann, G.: The Spin model checker: Primer and reference manual, 1st edn. Addison-Wesley Professional (2003)
Johnsen, E., Owe, O.: An asynchronous communication model for distributed concurrent objects. Software and Systems Modeling 6(1), 39–58 (2007)
Johnsen, E.B., Blanchette, J.C., Kyas, M., Owe, O.: Intra-object versus inter-object: Concurrency and reasoning in Creol. In: Proc. 2nd Intl. Workshop on Harnessing Theories for Tool Support in Software (TTSS 2008). Electronic Notes in Theoretical Computer Science, vol. 243, pp. 89–103. Elsevier (2009)
Johnsen, E.B., Owe, O., Axelsen, E.W.: A run-time environment for concurrent objects with asynchronous method calls. In: Martí-Oliet, N. (ed.) Proc. 5th Intl. Workshop on Rewriting Logic and its Applications (WRLA 2004). Electronic Notes in Theoretical Computer Science, vol. 117, pp. 375–392. Elsevier (January 2005)
Kim, M., Stehr, M.O., Talcott, C., Dutt, N., Venkatasubramanian, N.: A Probabilistic Formal Analysis Approach to Cross Layer Optimization in Distributed Embedded Systems. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 285–300. Springer, Heidelberg (2007)
Kumar, N., Sen, K., Meseguer, J., Agha, G.: Probabilistic rewrite theories: Unifying models, logics and tools. Technical report UIUCDCS-R-2003-2347, Department of Computer Science, Univ. of Illinois at Urbana-Champaign (2003)
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)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
Meseguer, J.: Membership Algebra as a Logical Framework for Equational Specification. In: Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)
Sen, K., Viswanathan, M., Agha, G.: Statistical Model Checking of Black-Box Probabilistic Systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004)
Sen, K., Viswanathan, M., Agha, G.: On Statistical Model Checking of Stochastic Systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266–280. Springer, Heidelberg (2005)
Sen, K., Viswanathan, M., Agha, G.A.: VESTA: A statistical model-checker and analyzer for probabilistic systems. In: Proc. 2nd Intl. Conf. on the Quantitative Evaluation of Systems (QEST 2005), pp. 251–252. IEEE Computer Society (2005)
Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 46–60. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bentea, L., Owe, O. (2012). A Probabilistic Framework for Object-Oriented Modeling and Analysis of Distributed Systems. In: Beckert, B., Damiani, F., Gurov, D. (eds) Formal Verification of Object-Oriented Software. FoVeOOS 2011. Lecture Notes in Computer Science, vol 7421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31762-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-31762-0_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31761-3
Online ISBN: 978-3-642-31762-0
eBook Packages: Computer ScienceComputer Science (R0)