×

Compatibility in a multi-component environment. (English) Zbl 1292.68107

Summary: A distributed environment where many components interact may be functioning in a suboptimal manner due to two main factors: message loss and deadlocks. Message loss occurs when a component is not ready to receive as input a message sent to it. In the case of a deadlock, a system is indefinitely waiting for a message that never arrives. In [J. Carmona and J. Cortadella, Lect. Notes Comput. Sci. 2517, 360–377 (2002; Zbl 1019.68616)] a theory has been presented for characterizing when a pair of systems is compatible in the sense that they can engage in a dialog free from these two problems. The theory developed was restricted to only two components, a particular mode of synchronization and a closed environment. In this paper we lift all these assumptions to define a general notion of compatibility in a multi-component environment. For the extended definition of compatibility, we use team automata as a modeling formalism which allows arbitrary synchronization strategies and iterative/hierarchical composition. Moreover, it is shown how the general definition of compatibility presented in this paper can be used to determine the compatibility problems that arise in a team automaton built on the basis of an arbitrary synchronization strategy.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q45 Formal languages and automata

Citations:

Zbl 1019.68616
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Adámek, J.; Plasil, F., Component composition errors and update atomicity: static analysis, Journal of Software Maintenance and Evolution: Research and Practice, 17, 5, 363-377 (2005)
[4] Armstrong, J., Erlang, Communications of ACM, 53, 9, 68-75 (2010)
[5] Arnold, A., Finite Transition Systems (1994), Prentice Hall
[6] Bauer, S. S.; Hennicker, R.; Janisch, S., Behaviour protocols for interacting stateful components, Electronic Notes in Theoretical Computer Science, 263, 47-66 (2010)
[7] Bauer, S. S.; Mayer, P.; Schroeder, A.; Hennicker, R., On weak modal compatibility, refinement, and the MIO workbench, (Esparza, J.; Majumdar, R., TACAS. TACAS, Lecture Notes in Computer Science, vol. 6015 (2010), Springer), 175-189 · Zbl 1284.68339
[9] ter Beek, M. H.; Ellis, C.; Kleijn, J.; Rozenberg, G., Synchronizations in team automata for groupware systems, Computer Supported Cooperative Work—The Journal of Collaborative Computing, 12, 1, 21-69 (2003)
[10] Berry, G., The esterel v5 language primer. Technical Report, Centre de Mathématiques Appliquées, Ecole des Mines and INRIA (2004)
[12] Carmona, J.; Cortadella, J., Input/output compatibility of reactive systems, (Fourth International Conference on Formal Methods in Computer-Aided Design, FMCAD, Portland, Oregon, USA (2002), Springer-Verlag), 360-377 · Zbl 1019.68616
[13] Carmona, J.; Cortadella, J.; Kishinevsky, M.; Taubin, A., Elastic circuits, IEEE Transactions on CAD of Integrated Circuits and Systems, 28, 10, 1437-1455 (2009)
[14] Carmona, J.; Cortadella, J.; Pastor, E., Synthesis of reactive systems: application to asynchronous circuit design, (Cortadella, J.; Yakovlev, A.; Rozenberg, G., Advances in Concurrency and Hardware Design. Advances in Concurrency and Hardware Design, ACHD. Advances in Concurrency and Hardware Design. Advances in Concurrency and Hardware Design, ACHD, Lecture Notes in Computer Science, vol. 2549 (2002), Springer-Verlag), 108-151 · Zbl 1029.68505
[17] David, A.; Larsen, K. G.; Legay, A.; Nyman, U.; Wasowski, A., Timed I/O automata: a complete specification theory for real-time systems, (Johansson, K. H.; Yi, W., HSCC (2010), ACM), 91-100 · Zbl 1361.68143
[18] Dill, D. L., (Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits, ACM Distinguished Dissertations (1989), MIT Press)
[19] Ellis, C. A., Team automata for groupware systems, (Proceedings of the International ACM SIGGROUP Conference on Supporting Group Work: The Integration Challenge. Proceedings of the International ACM SIGGROUP Conference on Supporting Group Work: The Integration Challenge, Phoenix, Arizona (1997), ACM Press: ACM Press New York), 415-424
[20] Engels, G.; Groenewegen, L., Towards team-automata-driven object-oriented collaborative work, (Brauer, W.; Ehrig, H.; Karhumäki, J.; Salomaa, A., Formal and Natural Computing. Formal and Natural Computing, Lecture Notes in Computer Science, vol. 2300 (2002), Springer), 257-276 · Zbl 1060.68607
[21] Fernandes, F.; Royer, J.-C., The STSLib project: towards a formal component model based on sts, Electronic Notes in Theoretical Computer Science, 215, 131-149 (2008)
[22] Hennicker, R.; Knapp, A., Modal interface theories for communication-safe component assemblies, (Cerone, A.; Pihlajasaari, P., ICTAC. ICTAC, Lecture Notes in Computer Science, vol. 6916 (2011), Springer), 135-153 · Zbl 1350.68182
[23] Larsen, K. G.; Nyman, U.; Wasowski, A., Modal I/O automata for interface and product line theories, (Nicola, R. D., ESOP. ESOP, Lecture Notes in Computer Science, vol. 4421 (2007), Springer), 64-79 · Zbl 1187.68296
[25] Lynch, N. A.; Tuttle, M. R., (An Introduction to Input/Output Automata. An Introduction to Input/Output Automata, CWI-Quarterly, volume 2 (1989)), 219-246, Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands · Zbl 0677.68067
[26] Lectures on petri nets I: basic models, advances in petri nets, the volumes are based on the advanced course on petri nets, held in Dagstuhl, September 1996, (Reisig, W.; Rozenberg, G., Lecture Notes in Computer Science, vol. 1491 (1998), 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.