×

Modeling actor systems using dynamic I/O automata. (English) Zbl 1461.68135

Mazzara, Manuel (ed.) et al., Perspectives of system informatics. 10th international Andrei Ershov informatics conference, PSI 2015, in memory of Helmut Veith, Kazan and Innopolis, Russia, August 24–27, 2015. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 9609, 186-202 (2016).
Summary: 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.
For the entire collection see [Zbl 1347.68011].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

ABS
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of dynamic register automata. In: FSTTCS, pp. 653–665 (2014) · Zbl 1360.68575
[2] Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)
[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) · Zbl 1278.68064 · doi:10.1007/978-3-540-39993-3_4
[4] Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Sci. Comput. Program. 77(12), 1289–1309 (2012) · Zbl 1264.68050 · doi:10.1016/j.scico.2010.08.003
[5] Apt, K.R.: Ten years of Hoare’s logic: a survey part II: nondeterminism. Theor. Comput. Sci. 28, 83–109 (1984) · Zbl 0523.68015 · doi:10.1016/0304-3975(83)90066-X
[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) · Zbl 1006.68537 · doi:10.1007/3-540-44685-0_10
[7] Attie, P.C., Lynch, N.: Dynamic Input/Output automata: a formal and compositional model for dynamic systems. Inf. Comput. (2015) (To appear) · Zbl 1344.68114
[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) · Zbl 1377.68144 · doi:10.1007/978-3-642-37064-9_17
[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) · Zbl 1285.68080 · doi:10.1007/978-3-642-13182-0_5
[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) · Zbl 06487503 · doi:10.1007/978-3-642-40213-5_8
[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) · doi:10.1007/3-540-49213-5_7
[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) · Zbl 1247.68184 · doi:10.1016/j.jlap.2012.01.003
[13] Din, C.C., Owe, O.: Compositional and sound reasoning about active objects with shared futures. Research report 437 (2014) · Zbl 1343.68166
[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) · Zbl 06248450 · doi:10.1007/978-3-642-38856-9_24
[15] Dovland, J., Johnsen, E.B., Owe, O.: Verification of concurrent objects with asynchronous method calls. In: SwSTE, pp. 141–150 (2005) · doi:10.1109/SWSTE.2005.24
[16] Duarte, C.H.C.: Proof-theoretic foundations for the design of actor systems. Math. Struct. Comput. Sci. 9(3), 227–252 (1999) · Zbl 0931.68065 · doi:10.1017/S0960129599002765
[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) · Zbl 1343.68167 · doi:10.1007/978-3-642-23217-6_27
[18] Gaspari, M., Zavattaro, G.: An algebra of actors. In: Ciancarini, P., Fantechi, A., Gorrieri, R. (eds.) FMOODS. Springer, New York (1999) · Zbl 0928.68020
[19] Haller, P., Odersky, M.: Scala actors: unifying thread-based and event-based programming. Theor. Comput. Sci. 410(2–3), 202–220 (2009) · Zbl 1162.68396 · doi:10.1016/j.tcs.2008.09.019
[20] International Telecommunication Union - Telecommunication Standardization. Open distributed processing - reference models parts 1–4. Technical report, ISO/IEC (1995)
[21] International Telecommunication Union - Telecommunication Standardization. Recommendation Z.120: Message Sequence Chart (MSC). Technical report, ISO/IEC (2011)
[22] Jaghoori, M.M., Chothia, T.: Timed automata semantics for analyzing Creol. In: FOCLASA, pp. 108–122 (2010)
[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) · Zbl 06060083 · doi:10.1007/978-3-642-25271-6_8
[24] Kurnia, I.W.: An automata-theoretic approach to open actor system verification. Ph.D. thesis, University of Kaiserslautern, January 2015
[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) · doi:10.1145/2414639.2414647
[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) · Zbl 06325819 · doi:10.1007/978-3-642-40615-7_3
[27] Lamport, L.: What good is temporal logic? In: IFIP Congress, pp. 657–668 (1983)
[28] Leo, J.: Dynamic process creation in a static model. Master’s thesis, MIT (1990)
[29] Lynch, N., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: PODC, pp. 137–151 (1987) · doi:10.1145/41840.41852
[30] Misra, J., Mani Chandy, K.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417–426 (1981) · Zbl 0468.68030 · doi:10.1109/TSE.1981.230844
[31] Montanari, U., Pistore, M.: Ugo Montanari and Marco Pistore. ENTCS 10, 170–188 (1997)
[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) · Zbl 0925.68289 · doi:10.1007/11419822_1
[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)
[34] Olderog, E.-R., Apt, K.R.: Fairness in parallel programs: the transformational approach. ACM TOPLAS 10(3), 420–455 (1988) · doi:10.1145/44501.44504
[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) · Zbl 0976.68549 · doi:10.1007/3-540-45397-0_18
[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) · Zbl 05570422 · doi:10.1007/11767954_18
[38] Smith, S., Talcott, C.L.: Specification diagrams for actor systems. High.-Order Symb. Comput. 15(4), 301–348 (2002) · Zbl 1020.68051 · doi:10.1023/A:1022934504959
[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) · Zbl 1108.68415 · doi:10.1007/978-3-540-27815-3_39
[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) · Zbl 1326.68205 · doi:10.1007/978-3-642-27940-9_29
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.