Skip to main content
SpringerLink
Log in

Ten Years of Analyzing Actors: Rebeca Experience

  • Chapter
Book cover Formal Modeling: Actors, Open Systems, Biological Systems

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7000))

Abstract

In this paper, we provide a survey of the different analysis techniques that are provided for the modeling language Rebeca. Rebeca is designed as an imperative actor-based language with the goal of providing an easy to use language for modeling concurrent and distributed systems, with formal verification support. Throughout the paper the language Rebeca and the supporting model checking tools are explained. Abstraction and compositional verification, as well as state-based reduction techniques including symmetry, partial order reduction, and slicing of Rebeca are discussed. We give an overview of a few extensions of Rebeca. For example, we present the modular schedulability analysis of timed actor-based models and formal techniques to check correctness of self-adaptive systems using Rebeca. A summary of design decisions and a brief general comparison of the analysis methods are provided at the end of the paper while specific sections are accompanied with examples and corresponding related work.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Adler, R., Schaefer, I., Schuele, T., Vecchié, E.: From model-based design to formal verification of adaptive embedded systems. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 76–95. Springer, Heidelberg (2007)

    Google Scholar 

  2. Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1990)

    Google Scholar 

  3. Afra: a SystemC verifier, http://ece.ut.ac.ir/FML/afra.htm

  4. Agha, G.: The structure and semantics of actor languages. In: de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1990. LNCS, vol. 489, pp. 1–59. Springer, Heidelberg (1991)

    Google Scholar 

  5. Agha, G., Mason, I., Smith, S., Talcott, C.L.: A foundation for actor computation. Journal of Functional Programming 7, 1–72 (1997)

    Google Scholar 

  6. Agha, G., Mason, I.A., Smith, S.F., Talcott, C.L.: Towards a theory of actor computation. In: Cleaveland, R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 565–579. Springer, Heidelberg (1992)

    Google Scholar 

  7. Altisen, K., Gößler, G., Sifakis, J.: Scheduler modeling based on the controller synthesis paradigm. Real-Time Systems 23(1-2), 55–84 (2002)

    Google Scholar 

  8. Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)

    Google Scholar 

  9. Barnat, J., Cerná, I.: Distributed breadth-first search ltl model checking. Formal Methods in System Design 29(2), 117–134 (2006)

    Google Scholar 

  10. Behjati, R., Sabouri, H., Razavi, N., Sirjani, M.: An effective approach for model checking systemc designs. In: Billington, J., Duan, Z., Koutny, M. (eds.) Proc. 8th International Conference on Application of Concurrency to System Design (ACSD 2008), pp. 56–61. IEEE (2008)

    Google Scholar 

  11. Bergstra, J.A., Middelburg, C.A.: Preferential choice and coordination conditions. J. Log. Algebr. Program. 70(2), 172–200 (2007)

    Google Scholar 

  12. de Boer, F., Chothia, T., Jaghoori, M.M.: Modular schedulability analysis of concurrent objects in Creol. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 212–227. Springer, Heidelberg (2010)

    Google Scholar 

  13. Bosnacki, D., Dams, D., Holenderski, L.: Symmetric SPIN. International Journal on Software Tools for Technology Transfer (STTT) 4(1), 92–106 (2002)

    Google Scholar 

  14. Bošnački, D., Donaldson, A.F., Leuschel, M., Massart, T.: Efficient approximate verification of promela models via symmetry markers. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 300–315. Springer, Heidelberg (2007)

    Google Scholar 

  15. Bradbury, J.S., Cordy, J.R., Dingel, J., Wermelinger, M.: A survey of self-management in dynamic software architecture specifications. In: Proc. 1st ACM SIGSOFT Workshop on Self-Managed Systems, WOSS 2004, pp. 28–33 (2004)

    Google Scholar 

  16. Chang, P.H., Agha, G.: Supporting reconfigurable object distribution for customized Web applications. In: The 22nd Annual ACM Symposium on Applied Computing (SAC 2007), pp. 1286–1292 (2007)

    Google Scholar 

  17. Chang, P.H., Agha, G.: Towards context-aware web applications. In: Indulska, J., Raymond, K. (eds.) DAIS 2007. LNCS, vol. 4531, pp. 239–252. Springer, Heidelberg (2007)

    Google Scholar 

  18. Cheong, E., Lee, E.A., Zhao, Y.: Viptos: a graphical development and simulation environment for tinyOS-based wireless sensor networks. In: Proc. 3rd International Conference on Embedded Networked Sensor Systems, SenSys 2005, pp. 302–302 (2005)

    Google Scholar 

  19. Cheng, B.H.C., de Lemos, R., Giese, H., Inverardi, P., Magee, J., Andersson, J., Becker, B., Bencomo, N., Brun, Y., Cukic, B., Di Marzo Serugendo, G., Dustdar, S., Finkelstein, A., Gacek, C., Geihs, K., Grassi, V., Karsai, G., Kienle, H.M., Kramer, J., Litoiu, M., Malek, S., Mirandola, R., Müller, H.A., Park, S., Shaw, M., Tichy, M., Tivoli, M., Weyns, D., Whittle, J.: Software Engineering for Self-Adaptive Systems: A Research Roadmap. In: Cheng, B.H.C., de Lemos, R., Giese, H., Inverardi, P., Magee, J. (eds.) Software Engineering for Self-Adaptive Systems. LNCS, vol. 5525, pp. 1–26. Springer, Heidelberg (2009)

    Google Scholar 

  20. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An openSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)

    Google Scholar 

  21. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (2000)

    Google Scholar 

  22. Clarke, E.M.: The birth of model checking. In: Proc. Symposium on “25 Years of Model Checking”, Federated Logic Conference (FLOC 2006) affiliated with CAV 2006, pp. 1–26 (August 2006)

    Google Scholar 

  23. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counter-example-guided abstraction refinement for symbolic model checking. J. ACM 50, 752–794 (2003)

    Google Scholar 

  24. Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 147–158. Springer, Heidelberg (1998)

    Google Scholar 

  25. Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9(1/2), 77–104 (1996)

    Google Scholar 

  26. Clinger, W.D.: Foundations of actor semantics. Tech. rep., Cambridge, MA, USA (1981)

    Google Scholar 

  27. Closse, E., Poize, M., Pulou, J., Sifakis, J., Venter, P., Weil, D., Yovine, S.: TAXYS: A tool for the development and verification of real-time embedded systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 391–395. Springer, Heidelberg (2001)

    Google Scholar 

  28. Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. Formal Methods in System Design 1(4), 385–415 (1992)

    Google Scholar 

  29. Donaldson, A.F., Miller, A.: Automatic symmetry detection for model checking using computational group theory. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 481–496. Springer, Heidelberg (2005)

    Google Scholar 

  30. Donaldson, A.F., Miller, A.: Extending symmetry reduction techniques to a realistic model of computation. Electronic Notes in Theoretical Computer Science 185, 63–76 (2007)

    Google Scholar 

  31. Donaldson, A.F., Miller, A., Calder, M.: Finding symmetry in models of concurrent systems by static channel diagram analysis. Electr. Notes Theor. Comput. Sci. 128(6), 161–177 (2005)

    Google Scholar 

  32. Donaldson, A.F., Miller, A., Calder, M.: Spin-to-Grape: A tool for analysing symmetry in Promela models. Electronic Notes in Theoretical Computer Science 139(1), 3–23 (2005)

    Google Scholar 

  33. Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for dpll(t). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)

    Google Scholar 

  34. Dwyer, M.B., Hatcliff, J., Hoosier, M., Ranganath, V., Robby, Wallentine, T.: Evaluating the effectiveness of slicing for model reduction of concurrent object-oriented programs. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 73–89. Springer, Heidelberg (2006)

    Google Scholar 

  35. Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 996–1072. Elsevier Science Publishers, Amsterdam (1990)

    Google Scholar 

  36. Emerson, E.A., Sistla, A.: Symmetry and model checking. Formal Methods in System Design 9(1-2), 105–131 (1996)

    Google Scholar 

  37. Erlang Programming Language Homepage, http://www.erlang.org

  38. Fersman, E., Krcal, P., Pettersson, P., Yi, W.: Task automata: Schedulability, decidability and undecidability. Information and Computation 205(8), 1149–1172 (2007)

    Google Scholar 

  39. Fredlund, L.Å., Svensson, H.: Mcerlang: a model checker for a distributed functional programming language. SIGPLAN Not 42(9), 125–136 (2007)

    Google Scholar 

  40. Garcia, J.J.G., Gutierrez, J.C.P., Harbour, M.G.: Schedulability analysis of distributed hard real-time systems with multiple-event synchronization. In: Proc. 12th Euromicro Conference on Real-Time Systems, pp. 15–24. IEEE (2000)

    Google Scholar 

  41. Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 176–185. Springer, Heidelberg (1991)

    Google Scholar 

  42. Groote, J.F., Mathijssen, A., Reniers, M.A., Usenko, Y.S., van Weerdenburg, M.: The formal specification language mcrl2. In: Brinksma, E., Harel, D., Mader, A., Stevens, P., Wieringa, R. (eds.) MMOSS. Dagstuhl Seminar Proceedings, vol. 06351. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl (2006)

    Google Scholar 

  43. Hendriks, M., Behrmann, G., Larsen, K.G., Niebert, P., Vaandrager, F.W.: Adding symmetry reduction to UPPAAL. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 46–59. Springer, Heidelberg (2004)

    Google Scholar 

  44. 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)

    Google Scholar 

  45. Hewitt, C.: What Is Commitment? Physical, Organizational, and Social (Revised). In: Noriega, P., Vázquez-Salceda, J., Boella, G., Boissier, O., Dignum, V., Fornara, N., Matson, E. (eds.) COIN 2006. LNCS (LNAI), vol. 4386, pp. 293–307. Springer, Heidelberg (2007)

    Google Scholar 

  46. Hewitt, C.: Orgs for scalable, robust, privacy-friendly client cloud computing. IEEE Internet Computing 12(5), 96–99 (2008)

    Google Scholar 

  47. Hewitt, C.: Actorscript(tm): Industrial strength integration of local and nonlocal concurrency for client-cloud computing. CoRR abs/0907.3330 (2009)

    Google Scholar 

  48. Hojjat, H., Sirjani, M., Mousavi, M., Groote, J.: Sarir: A Rebeca to mCRL2 translator (tool paper). In: Proc. 7th International Conference on Application of Concurrency to System Design (ACSD 2007) (July 2007)

    Google Scholar 

  49. Holzmann, G.J.: The model checker SPIN. Software Engineering 23(5), 279–295 (1997)

    Google Scholar 

  50. IceRose homepage - projects, http://en.ru.is/icerose/applying-formal-methods/projects

  51. Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design 9(1-2), 41–75 (1996)

    Google Scholar 

  52. Ip, C.N.: State Reduction Methods for Automatic Formal Verification. Ph.D. thesis, Department of Computer Science, Stanford University (1996)

    Google Scholar 

  53. Jaghoori, M.M., de Boer, F.S., Chotia, T., Sirjani, M.: Schedulability of asynchronous real-time concurrent objects. Journal of Logic and Algebraic Programming 78(5), 402–416 (2009)

    Google Scholar 

  54. Jaghoori, M.M., Chothia, T.: Timed automata semantics for analyzing Creol. In: Proc. Foundations of Coordination Languages and Software Architectures (FOCLASA 2010). EPTCS, vol. 30, pp. 108–122 (2010)

    Google Scholar 

  55. Jaghoori, M.M., Longuet, D., de Boer, F.S., Chothia, T.: Schedulability and compatibility of real time asynchronous objects. In: Proc. 2008 Real-Time Systems Symposium (RTSS), Barcelona, pp. 70–79. IEEE Computer Society (2008)

    Google Scholar 

  56. Jaghoori, M.M., Sirjani, M., Mousavi, M., Khamespanah, E., Movaghar, A.: Symmetry and partial order reduction techniques in model checking Rebeca. Acta Informatica 47, 33–66 (2010)

    Google Scholar 

  57. Jaghoori, M.M., Movaghar, A., Sirjani, M.: Modere: the model-checking engine of Rebeca. In: Haddad, H. (ed.) Proc. ACM Symposium on Applied Computing (SAC 2006), Dijon, France, April 23-27, pp. 1810–1815. ACM (2006)

    Google Scholar 

  58. Jahania, M.: Using SAT-Solvers to model check Rebeca for data-centric applications - Master thesis, Sharif University of Technology (2008)

    Google Scholar 

  59. Jaghoori, M.M., Sirjani, M., Mousavi, M.R., Movaghar, A.: Efficient symmetry reduction for an actor-based model. In: Chakraborty, G. (ed.) ICDCIT 2005. LNCS, vol. 3816, pp. 494–507. Springer, Heidelberg (2005)

    Google Scholar 

  60. Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Software and Systems Modeling 6(1), 35–58 (2007)

    Google Scholar 

  61. Johnsen, E.B., Owe, O., Arnestad, M.: Combining active and reactive behavior in concurrent objects. In: Langmyhr, D. (ed.) Proc. of the Norwegian Informatics Conference (NIK 2003), pp. 193–204. Tapir Academic Publisher (November 2003)

    Google Scholar 

  62. Johnsen, E.B., Owe, O., Yu, I.C.: Creol: A type-safe object-oriented model for distributed concurrent systems. Theoretical Computer Science 365(1-2), 23–66 (2006)

    Google Scholar 

  63. Kakoee, M.R., Shojaei, H., Ghasemzadeh, H., Sirjani, M., Navabi, Z.: A new approach for design and verification of transaction level models. In: International Symposium on Circuits and Systems (ISCAS 2007), pp. 3760–3763 (2007)

    Google Scholar 

  64. Karmani, R.K., Shali, A., Agha, G.: Actor frameworks for the JVM platform: a comparative analysis. In: PPPJ 2009: Proc. 7th International Conference on Principles and Practice of Programming in Java, pp. 11–20. ACM, New York (2009)

    Google Scholar 

  65. Khakpour, N., Jalili, S., Sirjani, M., Goltz, U.: Context specific behavioral equivalence of policy-based self-adaptive systems. In: Proc. 13th International Conference on Formal Engineering Methods (ICFEM 2011) (to appear, 2011)

    Google Scholar 

  66. Khakpour, N., Jalili, S., Talcott, C.L., Sirjani, M., Mousavi, M.R.: Formal modeling of evolving adaptive systems. In: Science of Computer Programming - Special issue of FACS 2009 (2009) (accepted)

    Google Scholar 

  67. Khakpour, N., Jalili, S., Talcott, C.L., Sirjani, M., Mousavi, M.R.: PobSAM: Policy-based managing of actors in self-adaptive systems. Electr. Notes Theor. Comput. Sci. 263, 129–143 (2010)

    Google Scholar 

  68. Khakpour, N., Khosravi, R., Sirjani, M., Jalili, S.: Formal analysis of policy-based self-adaptive systems. In: Proc. 25nd Annual ACM Symposium on Applied Computing (SAC 2010), pp. 2536–2543 (2010)

    Google Scholar 

  69. Kloukinas, C., Yovine, S.: Synthesis of safe, QoS extendible, application specific schedulers for heterogeneous real-time systems. In: Proc. 15th Euromicro Conference on Real-Time Systems (ECRTS 2003), Portugal, pp. 287–294. IEEE CS (2003)

    Google Scholar 

  70. Krinke, J.: Advanced Slicing of Sequential and Concurrent Programs. Ph.D. thesis, Universitat Passau, Fakaltat fr Mathematic und Informatik (April 2003)

    Google Scholar 

  71. Kupferman, O., Vardi, M.Y., Wolper, P.: Module checking. Information and Computation 164(2), 322–344 (2001)

    Google Scholar 

  72. Krinke, J.: Context sensitive slicing of concurrent programs. ACM SIGSOFT Software Engineering Notes, 178–187 (2003)

    Google Scholar 

  73. Lamport, L.: Composition: A way to make proofs harder. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 402–407. Springer, Heidelberg (1998)

    Google Scholar 

  74. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21, 558–565 (1978)

    Google Scholar 

  75. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. Journal on Software Tools for Technology Transfer (STTT) 1(1-2), 134–152 (1997)

    Google Scholar 

  76. Lauterburg, S., Karmani, R., Marinov, D., Agha, G.: Evaluating ordering heuristics for dynamic partial-order reduction techniques. In: Rosenblum, D., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp. 308–322. Springer, Heidelberg (2010)

    Google Scholar 

  77. Lauterburg, S., Karmani, R.K., Marinov, D., Agha, G.: Basset: a tool for systematic testing of actor programs. In: SIGSOFT FSE, pp. 363–364 (2010)

    Google Scholar 

  78. Lee, E.A., Neuendorffer, S., Wirthlin, M.J.: Actor-oriented design of embedded hardware and software systems. Journal of Circuits, Systems, and Computers 12(3), 231–260 (2003)

    Google Scholar 

  79. Leuschel, M., Massart, T.: Efficient approximate verification of B via symmetry markers. In: Proc. of the International Symmetry Conference, Edinburgh, UK, pp. 71–85 (2007)

    Google Scholar 

  80. Magee, J., Kramer, J.: Dynamic structure in software architectures. In: Proc. Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering (1996)

    Google Scholar 

  81. Mason, I.A., Talcott, C.L.: Actor languages: Their syntax, semantics, translation, and equivalence. Theoretical Computer Science 220(2), 409–467 (1999)

    Google Scholar 

  82. Maude Homepage, http://maude.cs.uiuc.edu

  83. McMillan, K.L.: A methodology for hardware verification using compositional model checking. Science of Computer Programming 37(1–3), 279–309 (2000)

    Google Scholar 

  84. Metayer, D.L.: Describing software architecture styles using graph grammars. Software Engineering, IEEE Transactions on 24(7), 521–533 (1998)

    Google Scholar 

  85. Microsoft: Asynchronous agents library, http://msdn.microsoft.com/en-us/library/dd492627VS.100.aspx

  86. Miller, A., Donaldson, A.F., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. 38(3) (2006)

    Google Scholar 

  87. Mohapatra, D., Mall, R., Kumar, R.: An overview of slicing techniques for object-oriented programs. Informatica (Slovenia), 253–277 (2006)

    Google Scholar 

  88. NuSMV user manual, http://nusmv.irst.itc.it/NuSMV/userman/index-v2.html

  89. Open SystemC Initiative: IEEE 1666: SystemC Language Reference Manual (2005), www.systemc.org

  90. Oreizy, P., Medvidovic, N., Taylor, R.N.: Architecture-based runtime software evolution. In: International Conference on Software Engineering, pp. 177–186 (1998)

    Google Scholar 

  91. Ptolemy homepage, http://ptolemy.berkeley.edu/ptolemyII

  92. 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, 19:1–19:35 (2011)

    Google Scholar 

  93. Ren, S., Yu, Y., Chen, N., Marth, K., Poirot, P.E., Shen, L.: Actors, roles and coordinators — A coordination model for open distributed and embedded systems. In: Ciancarini, P., Wiklicky, H. (eds.) COORDINATION 2006. LNCS, vol. 4038, pp. 247–265. Springer, Heidelberg (2006)

    Google Scholar 

  94. Ren, S., Agha, G.: RTsynchronizer: language support for real-time specifications in distributed systems. ACM SIGPLAN Notices 30(11), 50–59 (1995)

    Google Scholar 

  95. de Roever, W.P., Langmaack, H., Pnueli, A. (eds.): COMPOS 1997. LNCS, vol. 1536. Springer, Heidelberg (1998)

    Google Scholar 

  96. Sabouri, H., Sirjani, M.: Actor-based slicing techniques for efficient reduction of Rebeca models. Sci. Comput. Program. 75(10), 811–827 (2010)

    Google Scholar 

  97. Sabouri, H., Sirjani, M.: Slicing-based reductions for Rebeca. Electr. Notes Theor. Comput. Sci. 260, 209–224 (2010)

    Google Scholar 

  98. Scala Programming Language Homepage, http://www.scala-lang.org

  99. Schaefer, I., Poetzsch-Heffter, A.: Using abstraction in modular verification of synchronous adaptive systems. In: Autexier, S., Merz, S., van der Torre, L.W.N., Wilhelm, R., Wolper, P. (eds.) Trustworthy Software. OASICS, vol. 3. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl (2006)

    Google Scholar 

  100. Schneider, K., Schuele, T., Trapp, M.: Verifying the adaptation behavior of embedded systems. In: Proc. 2006 International Workshop on Self-Adaptation and Self-Managing Systems, SEAMS 2006, pp. 16–22. ACM, New York (2006)

    Google Scholar 

  101. Sen, K., Agha, G.: Cute and jcute: Concolic unit testing and explicit path model-checking tools. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 419–423. Springer, Heidelberg (2006)

    Google Scholar 

  102. Sirjani, M., Movaghar, A.: An actor-based model for formal modelling of reactive systems: Rebeca. Tech. Rep. CS-TR-80-01, Tehran, Iran (2001)

    Google Scholar 

  103. Sirjani, M., Movaghar, A., Iravanchi, H., Jaghoori, M., Shali, A.: Model checking Rebeca by SMV. In: Proc. Workshop on Automated Verification of Critical Systems (AVoCS 2003), Southampton, UK, pp. 233–236 (April 2003)

    Google Scholar 

  104. Sirjani, M., Movaghar, A., Mousavi, M.: Compositional verification of an object-based reactive system. In: Proc. Workshop on Automated Verification of Critical Systems (AVoCS 2001), Oxford, UK, pp. 114–118 (April 2001)

    Google Scholar 

  105. Sirjani, M., Movaghar, A., Shali, A., de Boer, F.: Modeling and verification of reactive systems using Rebeca. Fundamenta Informatica 63(4), 385–410 (2004)

    Google Scholar 

  106. Sirjani, M., Movaghar, A., Shali, A., de Boer, F.: Model checking, automated abstraction, and compositional verification of Rebeca models. Journal of Universal Computer Science 11(6), 1054–1082 (2005)

    Google Scholar 

  107. Sirjani, M., Shali, A., Jaghoori, M., Iravanchi, H., Movaghar, A.: A front-end tool for automated abstraction and modular verification of actor-based models. In: Proceedings of Fourth International Conference on Application of Concurrency to System Design (ACSD 2004), pp. 145–148. IEEE Computer Society (2004)

    Google Scholar 

  108. Sirjani, M., de Boer, F.S., Movaghar, A., Shali, A.: Extended Rebeca: A component-based actor language with synchronous message passing. In: Proceedings of Fifth International Conference on Application of Concurrency to System Design (ACSD 2005), pp. 212–221. IEEE Computer Society (2005)

    Google Scholar 

  109. Sirjani, M., de Boer, F.S., Movaghar, A.: Modular verification of a component-based actor language. Journal of Universal Computer Science 11(10), 1695–1717 (2005)

    Google Scholar 

  110. Sirjani, M., Movaghar, A., Iravanchi, H., Jaghoori, M.M., Shali, A.: Model checking in Rebeca. In: Arabnia, H.R., Mun, Y. (eds.) Proc. International Conference on Parallel and Distributed Processing Techniques and Applications, vol. 4, pp. 1819–1822. CSREA Press (2003)

    Google Scholar 

  111. Spin: Spin User Manual, http://spinroot.com/spin/Man/Manual.html

  112. Taentzer, G., Goedicke, M., Meyer, T.: Dynamic change management by distributed graph transformation: Towards configurable distributed systems. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) TAGT 1998. LNCS, vol. 1764, pp. 179–193. Springer, Heidelberg (2000)

    Google Scholar 

  113. Talcott, C.L.: Composable semantic models for actor theories. Higher-Order and Symbolic Computation 11(3), 281–343 (1998)

    Google Scholar 

  114. Talcott, C.L.: Actor theories in rewriting logic. Theoretical Computer Science 285(2), 441–485 (2002)

    Google Scholar 

  115. Talcott, C.L.: Coordination models based on a formal model of distributed object reflection. Electr. Notes Theor. Comput. Sci. 150, 143–157 (2006)

    Google Scholar 

  116. Talcott, C.L.: Policy-based coordination in PAGODA: A case study. Electr. Notes Theor. Comput. Sci. 181, 97–112 (2007)

    Google Scholar 

  117. Valmari, A.: A stubborn attack on state explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991)

    Google Scholar 

  118. Vardi, M.Y.: Branching vs. linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 1–22. Springer, Heidelberg (2001)

    Google Scholar 

  119. Varela, C., Agha, G.: Programming dynamically reconfigurable open systems with SALSA. ACM SIGPLAN Notices 36(12), 20–34 (2001)

    Google Scholar 

  120. Yonezawa, A.: ABCL: An Object-Oriented Concurrent System. Series in Computer Systems. MIT Press (1990)

    Google Scholar 

  121. Weiser, M.: Program slicing. In: Proc. 5th International Conference on Software Engineering, pp. 439–449 (1981)

    Google Scholar 

  122. Zhang, J., Cheng, B.H.C.: Specifying adaptation semantics. ACM SIGSOFT Software Engineering Notes 30(4), 1–7 (2005)

    Google Scholar 

  123. Zhang, J., Cheng, B.H.C.: Model-based development of dynamically adaptive software. In: Proc. 28th International Conference on Software Engineering, ICSE 2006, pp. 371–380. ACM, New York (2006)

    Google Scholar 

  124. Zhang, J., Goldsby, H.J., Cheng, B.H.: Modular verification of dynamically adaptive systems. In: Proc. 8th ACM International Conference on Aspect-Oriented Software Development, AOSD 2009, pp. 161–172. ACM, New York (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Reykjavik University, Reykjavik, Iceland

    Marjan Sirjani

  2. University of Tehran, Tehran, Iran

    Marjan Sirjani

  3. CWI, Amsterdam, The Netherlands

    Mohammad Mahdi Jaghoori

Authors
  1. Marjan Sirjani
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mohammad Mahdi Jaghoori
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Thomas M. Siebel Center for Computer Science, University of Illinois, 201 N. Goodwin Avenue, MC 258, 61801, Urbana, IL, USA

    Gul Agha

  2. Department of Computer Science, Aarhus University, Abogade 34, 8200, Aarhus N, Denmark

    Olivier Danvy

  3. University of Illinois at Urbana-Champaign, USA

    José Meseguer

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Sirjani, M., Jaghoori, M.M. (2011). Ten Years of Analyzing Actors: Rebeca Experience. In: Agha, G., Danvy, O., Meseguer, J. (eds) Formal Modeling: Actors, Open Systems, Biological Systems. Lecture Notes in Computer Science, vol 7000. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24933-4_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-24933-4_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-24932-7

  • Online ISBN: 978-3-642-24933-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation