×

Termination detection for active objects. (English) Zbl 1243.68221

Summary: We investigate deadlock detection for a modeling language based on active objects. To detect deadlock in an actor-like subset of Creol we focus on the communication between the active objects. For the analysis of the model we translate a Creol configuration to a process algebra featuring the Linda coordination primitives. The translation preserves the deadlock behaviour of the model and allows us to apply a formalism introduced by N. Busi, R. Gorrieri and G. Zavattaro [Inf. Comput. 156, No. 1–2, 90–121 (2000; Zbl 1046.68616)] to detect global deadlocks in the process algebra.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Citations:

Zbl 1046.68616

Software:

Rebeca; Creol
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ábrahám, E.; Grabe, I.; Grüner, A.; Steffen, M., Behavioral interface description of an object-oriented language with futures and promises, J. Logic Algebr. Program., 78, 7, 491-518 (2009), Special issue with selected contributions of NWPT’07. The paper is a reworked version of an earlier UiO Technical Report TR-364, October, 2007 · Zbl 1187.68130
[2] Agha, G. A., Actors: A Model of Concurrent Computation in Distributed Systems (1986), MIT Press: MIT Press Cambridge, MA
[3] Busi, N.; Gorrieri, R.; Zavattaro, G., On the expressiveness of Linda coordination primitives, Inform. Comput., 156, 1-2, 90-121 (2000) · Zbl 1046.68616
[4] de Boer, F. S.; Clarke, D.; Johnsen, E. B., A complete guide to the future, (de Nicola, R., Proceedings of Programming Languages and Systems. Proceedings of Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Vienna, Austria, LNCS, vol. 4421 (2007), Springer), 316-330 · Zbl 1475.68045
[5] de Boer, F. S.; Grabe, I., Automated deadlock detection in synchronized reentrant multithreaded call-graphs, (van Leeuwen, J.; Muscholl, A.; Peleg, D.; Pokorný, J.; Rumpe, B., SOFSEM 2010: Theory and Practice of Computer Science, 36th Conference on Current Trends in Theory and Practice of Computer Science. SOFSEM 2010: Theory and Practice of Computer Science, 36th Conference on Current Trends in Theory and Practice of Computer Science, LNCS, vol. 5901 (2010), Springer), 200-211 · Zbl 1274.68084
[6] Finkel, A.; Schnoebelen, P., Well-structured transition systems everywhere!, Theoret. Comput. Sci., 256, 1 (1998) · Zbl 0973.68170
[7] Giachino, E.; Laneve, C., Analysis of deadlocks in object groups, (FMOODS/FORTE. FMOODS/FORTE, Lecture Notes in Computer Science, vol. 6722 (2011), Springer), 168-182
[8] Johnsen, E. B.; Owe, O., An asynchronous communication model for distributed concurrent objects, Softw. Syst. Model., 6, 1, 35-58 (2007)
[9] Johnsen, E. B.; Owe, O.; Yu, I. C., Creol: a type-safe object-oriented model for distributed concurrent systems, Theoret. Comput. Sci., 365, 1-2, 23-66 (2006) · Zbl 1118.68031
[10] Sirjani, M., Rebeca: theory applications and tools, (FMCO. FMCO, Lecture Notes in Computer Science, vol.4709 (2007), Springer)
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.