Abstract
In this paper we propose the so-called composite actor model for specifying composed entities such as the Internet. This model extends the actor model of concurrent computation so that it follows the “Reflective Russian Dolls” pattern and supports an arbitrary hierarchical composition of entities. To enable statistical model checking we introduce a new scheduling approach for composite actor models which guarantees the absence of unquantified nondeterminism. The underlying executable specification formalism we use is the rewriting logic-based semantic framework Maude, its probabilistic extension PMaude, and the statistical model checker PVeStA. We formalize a model transformation which—given certain formal requirements—generates a scheduled specification. We prove the correctness of the scheduling approach and the soundness of the transformation by introducing the notions of strong zero-time rule confluence and time-passing bisimulation and by showing that the transformation is a time-passing bisimulation for strongly zero-time rule confluent composite actor specifications.
This work has been partially sponsored by the EU-funded projects FP7-257414 ASCENS and FP7-256980 NESSoS, and AFOSR Grant FA8750-11-2-0084. Tobias Mühlbauer is also partially supported by the Google Europe Fellowship in Structured Data Analysis. We thank Mirco Tribastone for his helpful comments on this paper. We further thank all reviewers for their valuable feedback.
Chapter PDF
Similar content being viewed by others
References
ØMQ: The Intelligent Transport Layer (August 07, 2012), http://www.zeromq.org/
Agha, G.: Actors: a model of concurrent computation in distributed systems. MIT Press (1986)
Agha, G., Hewitt, C.: Concurrent programming using actors. In: Object-Oriented Concurrent Programming, pp. 37–53. MIT Press (1988)
Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based Specification Language for Probabilistic Object Systems. ENTCS 153(2), 213–239 (2006)
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)
AlTurki, M., Meseguer, J., Gunter, C.A.: Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol. ENTCS 234, 3–18 (2009)
Armstrong, J., Virding, R., Wikström, C., Williams, M.: Concurrent Programming in Erlang. Prentice Hall (1996)
Bentea, L., Ölveczky, P.C.: Probabilistic real-time rewrite theories and their expressive power. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 60–79. Springer, Heidelberg (2011)
Bruni, R., Corradini, A., Gadducci, F., Lluch Lafuente, A., Vandin, A.: Modelling and Analyzing Adaptive Self-assembly Strategies with Maude. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 118–138. Springer, Heidelberg (2012)
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)
Eckhardt, J.: A Formal Analysis of Security Properties in Cloud Computing. Master’s thesis, LMU Munich, TU Munich (2011)
Eckhardt, J., Mühlbauer, T., AlTurki, M., Meseguer, J., Wirsing, M.: Stable Availability under Denial of Service Attacks through Formal Patterns. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 78–93. Springer, Heidelberg (2012)
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: WRLA. ENTCS, vol. 71, pp. 162–187 (2002)
Haller, P., Sommers, F.: Actors in Scala. Artima Developer (2012)
Hewitt, C., Baker, H.G.: Laws for communicating parallel processes. In: IFIP Congress, pp. 987–992 (1977)
Hewitt, C., Bishop, P., Steiger, R.: A universal modular actor formalism for artificial intelligence. In: IJCAI, pp. 235–245 (1973)
Kwiatkowska, M., Norman, G., Parker, D., Vigliotti, M.G.: Probabilistic Mobile Ambients. TCS 410(12-13), 1272–1303 (2009)
Larsen, K.G., Skou, A.: Bisimulation through Probabilistic Testing. Inf. Comput. 94(1), 1–28 (1991)
Meseguer, J., Talcott, C.: Semantic Models for Distributed Object Reflection. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 1–36. Springer, Heidelberg (2002)
Mühlbauer, T.: Formal Specification and Analysis of Cloud Computing Management. Master’s thesis, LMU Munich, TU Munich (2011)
Wirsing, M., Eckhardt, J., Mühlbauer, T., Meseguer, J.: Design and Analysis of Cloud-Based Architectures with KLAIM and Maude. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 54–82. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Eckhardt, J., Mühlbauer, T., Meseguer, J., Wirsing, M. (2013). Statistical Model Checking for Composite Actor Systems. In: Martí-Oliet, N., Palomino, M. (eds) Recent Trends in Algebraic Development Techniques. WADT 2012. Lecture Notes in Computer Science, vol 7841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37635-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-37635-1_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37634-4
Online ISBN: 978-3-642-37635-1
eBook Packages: Computer ScienceComputer Science (R0)