Abstract
Many distributed systems use broadcast communication for various reasons such as saving energy or increasing throughput. However, the actor model for concurrent and distributed systems does not directly support this kind of communication. In such cases, a broadcast must be modeled as multiple unicasts which leads to loss of modularity and state space explosion for any non-trivial system. In this paper, we extend Rebeca, an actor-based model language, to support asynchronous anonymous message broadcasting. Then, we apply counter abstraction for reducing the state space which efficiently bypasses the constructive orbit problem by considering the global state as a vector of counters, one per each local state. This makes the model checking of systems possible without further considerations of symmetry. This approach is efficient for fully symmetric system like broadcasting environments. We use a couple of case studies to illustrate the applicability of our method and the way their state spaces are reduced in size.
Chapter PDF
Similar content being viewed by others
References
Rebeca formal modeling language, http://www.rebeca-lang.org/wiki/pmwiki.php/Tools/Afra
Agha, G.A.: ACTORS - a model of concurrent computation in distributed systems. MIT Press series in artificial intelligence. MIT Press (1990)
Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Symbolic counter abstraction for concurrent software. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 64–78. Springer, Heidelberg (2009)
Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. Journal of the ACM 32(4), 824–840 (1985)
Cachin, C., Kursawe, K., Petzold, F., Shoup, V.: Secure and efficient asynchronous broadcast protocols. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol. 2139, pp. 524–541. Springer, Heidelberg (2001)
Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Computer Aided Verification, pp. 147–158. Springer (1998)
Correia, M., Veronese, G.S., Neves, N.F., Veríssimo, P.: Byzantine consensus in asynchronous message-passing systems: a survey. IJCCBS 2(2), 141–161 (2011)
Cui, T., Chen, L., Ho, T.: Distributed optimization in wireless networks using broadcast advantage. In: Decision and Control, pp. 5839–5844. IEEE (2007)
Dechter, R., Kleinrock, L.: Broadcast communications and distributed algorithms. Trans. Computers 35(3), 210–219 (1986)
Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: New techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999)
Fill, J.A., Mahmoud, H.M., Szpankowski, W.: On the distribution for the duration of a randomized leader election algorithm. Ann. Appl. Probab., 1260–1283 (1996)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer (1996)
Hewitt, C.: Viewing control structures as patterns of passing messages. Artif. Intell. 8(3), 323–364 (1977)
Jaghoori, M.M., Sirjani, M., Mousavi, M.R., Khamespanah, E., Movaghar, A.: Symmetry and partial order reduction techniques in model checking Rebeca. Acta Informatica 47(1), 33–66 (2010)
Katoen, J.: Model checking: One can do much more than you think? In: Fundamentals of Software Engineering, pp. 1–14. Springer (2011)
Larrea, M., Raynal, M., Arriola, I.S., Cortiñas, R.: Specifying and implementing an eventual leader service for dynamic systems. IJWGS 8(3), 204–224 (2012)
Levitan, S.P., Foster, C.C.: Finding an extremum in a network. In: 9th International Symposium on Computer Architecture, pp. 321–325. ACM (1982)
Martel, C.U.: Maximum finding on a multiple access broadcast network. Inf. Process. Lett. 52(1), 7–15 (1994)
McMillan, K.L.: Symbolic model checking. Kluwer (1993)
Melliar-Smith, P.M., Moser, L.E., Agrawala, V.: Broadcast protocols for distributed systems. Trans. Parallel Distrib. Syst. 1(1), 17–25 (1990)
Mostéfaoui, A., Raynal, M., Travers, C.: Crash-resilient time-free eventual leadership. In: 23rd International Symposium on Reliable Distributed Systems, pp. 208–217. IEEE Computer Society (2004)
Okun, M., Barak, A.: Efficient algorithms for anonymous byzantine agreement. Theory Comput. Syst. 42(2), 222–238 (2008)
Ostrovsky, R., Rajagopalan, S., Vazirani, U.V.: Simple and efficient leader election in the full information model. In: Proceedings of the Twenty-Sixth Annual ACM Symposium on Theory of Computing, pp. 234–242. ACM (1994)
Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0, 1, infty)-Counter Abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–122. Springer, Heidelberg (2002)
Reynisson, A.H., Sirjani, M., Aceto, L., Cimini, M., Jafari, A., Ingólfsdóttir, A., Sigurdarson, S.H.: Modelling and simulation of asynchronous real-time systems using Timed Rebeca. Sci. Comput. Program. 89, 41–68 (2014)
Sabouri, H., Khosravi, R.: Delta modeling and model checking of product families. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 51–65. Springer, Heidelberg (2013)
Shiau, S., Yang, C.: A fast maximum finding algorithm on broadcast communication. In: Li, M., Du, D.-Z. (eds.) COCOON 1995. LNCS, vol. 959, pp. 472–481. Springer, Heidelberg (1995)
Shiau, S., Yang, C.: A fast sorting algorithm and its generalization on broadcast communications. In: Du, D.-Z., Eades, P., Sharma, A.K., Lin, X., Estivill-Castro, V. (eds.) COCOON 2000. LNCS, vol. 1858, pp. 252–261. Springer, Heidelberg (2000)
Sirjani, M., de Boer, F.S., Movaghar, A., Shali, A.: Extended Rebeca: A component-based actor language with synchronous message passing. In: Fifth International Conference on Application of Concurrency to System Design, pp. 212–221. IEEE Computer Society (2005)
Sirjani, M., Jaghoori, M.M.: Ten years of analyzing actors: Rebeca experience. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 20–56. Springer, Heidelberg (2011)
Sirjani, M., Movaghar, A., Shali, A., de Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fundam. Inform. 63(4), 385–410 (2004)
Sirjani, M., Shali, A., Jaghoori, M.M., Iravanchi, H., Movaghar, A.: A front-end tool for automated abstraction and modular verification of actor-based models. In: 4th International Conference on Application of Concurrency to System Design, pp. 145–150. IEEE Computer Society (2004)
Varshosaz, M., Khosravi, R.: Modeling and verification of probabilistic actor systems using pRebeca. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 135–150. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 IFIP International Federation for Information Processing
About this paper
Cite this paper
Yousefi, B., Ghassemi, F., Khosravi, R. (2015). Modeling and Efficient Verification of Broadcasting Actors. In: Dastani, M., Sirjani, M. (eds) Fundamentals of Software Engineering. FSEN 2015. Lecture Notes in Computer Science(), vol 9392. Springer, Cham. https://doi.org/10.1007/978-3-319-24644-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-24644-4_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24643-7
Online ISBN: 978-3-319-24644-4
eBook Packages: Computer ScienceComputer Science (R0)