Skip to main content
SpringerLink
Log in

Modeling Actor Systems Using Dynamic I/O Automata

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9609))

  • 427 Accesses

Abstract

Actor-based programming has become an important technique for the development of concurrent and distributed systems. This paper presents a new automaton model for actor systems and demonstrates how the model can be used for compositional verification. The model allows expressing the detailed behavior of actor components where components are built from actors and other components. It abstracts from internal and environment behavior, supports encapsulation of actors, and captures the dynamic aspects of actor creation and exposure of actor names to the component environment, which are crucial for verification. We handle these changes at the component interface by specializing dynamic I/O automata. The model can be used as a foundation of different verification techniques. We illustrate this by combining weakest precondition techniques on the actor level with simulation proofs on the component level.

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 EPUB and 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

Notes

  1. 1.

    \(\alpha \textsf {ABS}\) does not support suspension of tasks or wait statements.

  2. 2.

    For simplicity, we have only one worker per session. It is easy to extend the example to support pools of workers.

  3. 3.

    We use abbreviations for automata to also represent “a single automaton”. The usage is apparent from the context.

References

  1. Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of dynamic register automata. In: FSTTCS, pp. 653–665 (2014)

    Google Scholar 

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

    Google Scholar 

  3. Agha, G., Thati, P.: An algebraic theory of actors and its application to a simple object-based language. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol. 2635, pp. 26–57. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Sci. Comput. Program. 77(12), 1289–1309 (2012)

    Article  MATH  Google Scholar 

  5. Apt, K.R.: Ten years of Hoare’s logic: a survey part II: nondeterminism. Theor. Comput. Sci. 28, 83–109 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  6. Attie, P.C., Lynch, N.A.: Dynamic Input/Output automata: a formal model for dynamic systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 137–151. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. Attie, P.C., Lynch, N.: Dynamic Input/Output automata: a formal and compositional model for dynamic systems. Inf. Comput. (2015) (To appear)

    Google Scholar 

  8. Bollig, B., Cyriac, A., Hélouët, L., Kara, A., Schwentick, T.: Dynamic communicating automata and branching high-level MSCs. In: Dediu, A.-H., Martín-Vide, C., Truthe, B. (eds.) LATA 2013. LNCS, vol. 7810, pp. 177–189. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  9. Bollig, B., Hélouët, L.: Realizability of dynamic MSC languages. In: Ablayev, F., Mayr, E.W. (eds.) CSR 2010. LNCS, vol. 6072, pp. 48–59. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Boudjadar, A., Vaandrager, F., Bodeveix, J.-P., Filali, M.: Extending UPPAAL for the modeling and verification of dynamic real-time systems. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 111–132. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  11. Dam, M., Fredlund, L., Gurov, D.: Toward parametric verification of open distributed systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 150–185. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  12. Din, C.C., Dovland, J., Johnsen, E.B., Owe, O.: Observable behavior of distributed systems: component reasoning for concurrent objects. J. Log. Algebr. Program. 81(3), 227–256 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  13. Din, C.C., Owe, O.: Compositional and sound reasoning about active objects with shared futures. Research report 437 (2014)

    Google Scholar 

  14. D’Osualdo, E., Kochems, J., Ong, C.-H.L.: Automatic verification of erlang-style concurrency. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 454–476. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  15. Dovland, J., Johnsen, E.B., Owe, O.: Verification of concurrent objects with asynchronous method calls. In: SwSTE, pp. 141–150 (2005)

    Google Scholar 

  16. Duarte, C.H.C.: Proof-theoretic foundations for the design of actor systems. Math. Struct. Comput. Sci. 9(3), 227–252 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  17. Fisher, J., Henzinger, T.A., Nickovic, D., Piterman, N., Singh, A.V., Vardi, M.Y.: Dynamic reactive modules. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 404–418. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  18. Gaspari, M., Zavattaro, G.: An algebra of actors. In: Ciancarini, P., Fantechi, A., Gorrieri, R. (eds.) FMOODS. Springer, New York (1999)

    Google Scholar 

  19. Haller, P., Odersky, M.: Scala actors: unifying thread-based and event-based programming. Theor. Comput. Sci. 410(2–3), 202–220 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  20. International Telecommunication Union - Telecommunication Standardization. Open distributed processing - reference models parts 1–4. Technical report, ISO/IEC (1995)

    Google Scholar 

  21. International Telecommunication Union - Telecommunication Standardization. Recommendation Z.120: Message Sequence Chart (MSC). Technical report, ISO/IEC (2011)

    Google Scholar 

  22. Jaghoori, M.M., Chothia, T.: Timed automata semantics for analyzing Creol. In: FOCLASA, pp. 108–122 (2010)

    Google Scholar 

  23. Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Kurnia, I.W.: An automata-theoretic approach to open actor system verification. Ph.D. thesis, University of Kaiserslautern, January 2015

    Google Scholar 

  25. Kurnia, I.W., Poetzsch-Heffter, A.: A relational trace logic for simple hierarchical actor-based component systems. In: AGERE! 2012, pp. 47–58. ACM (2012)

    Google Scholar 

  26. Kurnia, I.W., Poetzsch-Heffter, A.: Verification of open concurrent object systems. In: Giachino, E., Hähnle, R., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 7866, pp. 83–118. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  27. Lamport, L.: What good is temporal logic? In: IFIP Congress, pp. 657–668 (1983)

    Google Scholar 

  28. Leo, J.: Dynamic process creation in a static model. Master’s thesis, MIT (1990)

    Google Scholar 

  29. Lynch, N., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: PODC, pp. 137–151 (1987)

    Google Scholar 

  30. Misra, J., Mani Chandy, K.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417–426 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  31. Montanari, U., Pistore, M.: Ugo Montanari and Marco Pistore. ENTCS 10, 170–188 (1997)

    Google Scholar 

  32. Montanari, U., Pistore, M.: History-dependent automata: an introduction. In: Bernardo, M., Bogliolo, A. (eds.) SFM-Moby 2005. LNCS, vol. 3465, pp. 1–28. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  33. Nipkow, T., Slind, K.: I/O automata in Isabelle/HOL. In: Dybjer, P., Nordström, B., Smith, J. (eds.) TYPES. LNCS, vol. 996, pp. 101–119. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  34. Olderog, E.-R., Apt, K.R.: Fairness in parallel programs: the transformational approach. ACM TOPLAS 10(3), 420–455 (1988)

    Article  Google Scholar 

  35. OSGi core release 5 (2012). http://www.osgi.org

  36. Schacht, S.: Formal reasoning about actor programs using temporal logic. In: Agha, G., De Cindio, F., Rozenberg, G. (eds.) APN 2001. LNCS, vol. 2001, pp. 445–460. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  37. Sirjani, M., Jaghoori, M.M., Baier, C., Arbab, F.: Compositional semantics of an actor-based language using constraint automata. In: Ciancarini, P., Wiklicky, H. (eds.) COORDINATION 2006. LNCS, vol. 4038, pp. 281–297. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  38. Smith, S., Talcott, C.L.: Specification diagrams for actor systems. High.-Order Symb. Comput. 15(4), 301–348 (2002)

    Article  MATH  Google Scholar 

  39. Thati, P., Talcott, C., Agha, G.: Techniques for executing and reasoning about specification diagrams. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 521–536. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  40. Zufferey, D., Wies, T., Henzinger, T.A.: Ideal abstractions for well-structured transition systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 445–460. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Kaiserslautern, Kaiserslautern, Germany

    Ilham W. Kurnia & Arnd Poetzsch-Heffter

Authors
  1. Ilham W. Kurnia
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Arnd Poetzsch-Heffter
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ilham W. Kurnia .

Editor information

Editors and Affiliations

  1. Innopolis University, Innopolis, Russia

    Manuel Mazzara

  2. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Kurnia, I.W., Poetzsch-Heffter, A. (2016). Modeling Actor Systems Using Dynamic I/O Automata. In: Mazzara, M., Voronkov, A. (eds) Perspectives of System Informatics. PSI 2015. Lecture Notes in Computer Science(), vol 9609. Springer, Cham. https://doi.org/10.1007/978-3-319-41579-6_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-41579-6_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-41578-9

  • Online ISBN: 978-3-319-41579-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation