Abstract
Quantitative verification has gained an increasing attention as a promising approach for analysis of systems in various domains, especially for distributed systems, where the uncertainties of the environment cause the system to exhibit probabilistic and nondeterministic behavior. In this paper, we introduce pRebeca, an extension to the high-level actor-based modeling language Rebeca, that is used to model distributed and reactive systems with probabilistic and nondeterministic nature. We propose a simple syntax suitable for describing different aspects of a probabilistic system behavior and provide a formal semantics based on Markov decision processes. To model check a pRebeca model, it is converted to a Markov decision process and verified using the PRISM model checker against PCTL properties. Using a couple of examples, we show how a probabilistic system can be expressed in pRebeca in a simple way, while taking advantage of the PRISM model checker features.
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
Sirjani, M., Movaghar, A., Shali, A., de Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fundam. Inf. 63(4), 385–410 (2004)
Hewitt, C.: Description and theoretical analysis (using schemata) of PLANNER: A language for proving theorems and manipulating models in a robot. MIT Artificial Intelligence Technical Report 258, Department of Computer Science. MIT (April 1972)
Agha, G.: Actors: a model of concurrent computation in distributed systems. MIT Press, Cambridge (1986)
Agha, G., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. Journal of Functional Programming 7, 1–72 (1998)
Karmani, R.K., Shali, A., Agha, G.: Actor frameworks for the JVM platform: a comparative analysis. In: Proceedings of the 7th International Conference on Principles and Practice of Programming in Java, PPPJ 2009, pp. 11–20. ACM, New York (2009)
Hewitt, C.: Orgs for scalable, robust, privacy-friendly client cloud computing. IEEE Internet Computing 12(5), 96–99 (2008)
Hewitt, C.: Actorscript(tm): Industrial strength integration of local and nonlocal concurrency for client-cloud computing. CoRR abs/0907.3330 (2009)
Agha, G., Meseguer, J., Sen, K.: Pmaude: Rewrite-based specification language for probabilistic object systems. Electron. Notes Theor. Comput. Sci. 153(2), 213–239 (2006)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Razavi, N., Behjati, R., Sabouri, H., Khamespanah, E., Shali, A., Sirjani, M.: Sysfier: Actor-based formal verification of systemc. ACM Trans. Embed. Comput. Syst. 10(2), 19:1–19:35 (2011)
Baier, C., Kwiatkowska, M.Z.: Domain equations for probabilistic processes. Electr. Notes Theor. Comput. Sci. 7, 34–54 (1997)
den Hartog, J., de Vink, E.P.: Mixing up nondeterminism and probability: a preliminary report. Electr. Notes Theor. Comput. Sci. 22, 88–110 (1999)
Hansson, H.A.: Time and Probability in Formal Design of Distributed Systems. Elsevier Science Inc., New York (1994)
Larsen, K.G., Skou, A.: Compositional Verification of Probabilistic Processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 456–471. Springer, Heidelberg (1992)
Lowe, G.: Probabilistic and prioritized models of timed csp. Theor. Comput. Sci. 138(2), 315–352 (1995)
Penczek, W., Szałas, A. (eds.): MFCS 1996. LNCS, vol. 1113. Springer, Heidelberg (1996)
Tofts, C.: A Synchronous Calculus of Relative Frequency. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 467–480. Springer, Heidelberg (1990)
Ciesinski, F., Baier, C.: Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: Proc. 3rd International Conference on Quantitative Evaluation of Systems (QEST 2006), pp. 131–132. IEEE CS Press (2006)
Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The Ins and Outs of The Probabilistic Model Checker MRMC. In: Quantitative Evaluation of Systems (QEST), pp. 167–176. IEEE Computer Society (2009), www.mrmc-tool.org
Bohnenkamp, H.C., D’Argenio, P.R., Hermanns, H., Katoen, J.P.: Modest: A compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng. 32(10), 812–830 (2006)
Katoen, J.-P. (ed.): ARTS 1999. LNCS, vol. 1601. Springer, Heidelberg (1999)
Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), San Diego, California, USA, June 23-25. IEEE (2004)
Baier, C., Katoen, J.P.: Principles of Model Checking. Representation and Mind Series. The MIT Press (2008)
Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Information and Computation 88(1) (1990)
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
Varshosaz, M., Khosravi, R. (2012). Modeling and Verification of Probabilistic Actor Systems Using pRebeca. In: Aoki, T., Taguchi, K. (eds) Formal Methods and Software Engineering. ICFEM 2012. Lecture Notes in Computer Science, vol 7635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34281-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-34281-3_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34280-6
Online ISBN: 978-3-642-34281-3
eBook Packages: Computer ScienceComputer Science (R0)