Andova, S.; Groenewegen, L. P. J.; de Vink, E. P. Dynamic consistency in process algebra: from paradigm to ACP. (English) Zbl 1213.68398 Sci. Comput. Program. 76, No. 8, 711-735 (2011). Summary: The coordination modelling language Paradigm addresses collaboration between components in terms of dynamic constraints. Within a Paradigm model, component dynamics are consistently specified at various levels of abstraction. The operational semantics of Paradigm is given. For a large, general subclass of Paradigm models a translation into process algebra is provided. Once expressed in process algebra, relying on a correctness result, Paradigm models are amenable to process algebraic reasoning and to verification via the mCRL2 toolset. Examples of a scheduling problem illustrate the approach. MSC: 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) 68N99 Theory of software Keywords:branching bisimulation; collaboration; dynamic consistency; dynamic constraint; paradigm; process algebra; verification Software:mCRL2; Reo PDFBibTeX XMLCite \textit{S. Andova} et al., Sci. Comput. Program. 76, No. 8, 711--735 (2011; Zbl 1213.68398) Full Text: DOI References: [1] Allen, R.; Garlan, D.: A formal basis for architectural connection, ACM transactions on software engineering and methodology 6, 213-249 (1997) [2] Andova, S.; Groenewegen, L. P. J.; Stafleu, J.; De Vink, E. P.: Formalizing adaptation on-the-fly, Entcs 255, 23-44 (2009) · Zbl 1364.68272 [3] Andova, S.; Groenewegen, L. P. J.; Verschuren, J. H. S.; De Vink, E. P.: Architecting security with paradigm, Lncs 5835, 255-283 (2009) [4] Andova, S.; Groenewegen, L. P. J.; De Vink, E. P.: System evolution by migration coordination, Proc. BENEVOL 2008 2008, 18-22 (2008) [5] Arbab, F.: The IWIM model for coordination of concurrent activities, Lncs 1061, 34-56 (1996) [6] Arbab, F.: Reo: a channel-based coordination model for component composition, Mathematical structures in computer science 14, 329-366 (2004) · Zbl 1085.68552 [7] Baeten, J. C. M.; Basten, T.; Reniers, M. A.: Process algebra: equational theories of communicating processes, (2010) · Zbl 1234.68001 [8] Barros, T.; Henrio, L.; Madelaine, E.: Behavioural models for hierarchical components, Lncs 3639, 154-168 (2005) [9] Beek, M. H. Ter; Ellis, C. A.; Kleijn, J.; Rozenberg, G.: Team automata for spatial access control, Proc. ECSCW’01, 59-77 (2001) [10] Bergstra, J. A.; Ponse, A.; Smolka, S. A.: Handbook of process algebra, (2001) · Zbl 0971.00006 [11] Bradfield, J.; Stirling, C.: Modal mu-calculi, , 721-756 (2007) [12] Broy, M.; Krüger, I. H.; Meisinger, M.: A formal model of services, ACM transactions on software engineering and methodology 16 (2007) [13] Broy, M.; Stoelen, K.: Specification and development of interactive systems: focus on streams, interfaces, and refinement, (2001) · Zbl 0981.68115 [14] Carriero, N.; Gelernter, D.: Linda in context, Communications of the ACM 32, 444-458 (1989) [15] Ciancarini, P.: Coordination models and languages as software integrators, ACM computing surveys 28, 300-302 (1996) [16] De Nicola, R.; Vaandrager, F. W.: Three logics for branching bisimulation, Journal of the ACM 42, 458-487 (1995) · Zbl 0886.68064 [17] Engels, G.; Groenewegen, L. P. J.: SOCCA: specifications of coordinated and cooperative activities, Software process modelling and technology, 71-102 (1994) [18] Engels, G.; Groenewegen, L. P. J.; Kappel, G.: Coordinated collaboration of objects, Advances in object-oriented data modeling, 307-331 (2000) [19] Fokkink, W.: Introduction to process algebra, (2000) · Zbl 0941.68087 [20] Van Glabbeek, R. J.: The linear time–branching time spectrum II: The semantics of sequential systems with silent moves, Lncs 715, 66-81 (1993) [21] Van Glabbeek, R. J.: The linear time–branching time spectrum: the semantics of concrete, sequential processes, , 3-99 (2001) · Zbl 1035.68073 [22] Van Glabbeek, R. J.; Weijland, P.: Branching time and abstraction in bisimulation semantics, Journal of the ACM 43, 555-600 (1996) · Zbl 0882.68085 [23] L.P.J. Groenewegen, E.P. de Vink, Dynamic system adaptation by constraint orchestration. Technical Report CSR 08/29, Technische Universiteit Eindhoven, 2008. 20 pp, arXiv:0811.3492v1. [24] Groenewegen, L. P. J.; Van Kampenhout, N.; De Vink, E. P.: Delegation modelling with paradigm, Lncs 3454, 94-108 (2005) [25] Groenewegen, L. P. J.; De Vink, E. P.: Operational semantics for coordination in paradigm, Lncs 2315, 191-206 (2002) · Zbl 1053.68562 [26] Groenewegen, L. P. J.; De Vink, E. P.: Evolution-on-the-fly with paradigm, Lncs 4038, 97-112 (2006) [27] Groote, J. F.; Mathijssen, A. H. J.; Reniers, M. A.; Usenko, Y. S.; Van Weerdenburg, M. J.: The formal specification language mcrl2, Ibfi (2007) · Zbl 1171.68400 [28] Groote, J. F.; Reniers, M. A.: Algebraic process verification, , 1151-1208 (2001) · Zbl 1035.68069 [29] Kokash, N.; Koehler, C.; De Vink, E. P.: Data-aware design and verification of service composition with reo and mcrl2, ACM, 2399-2407 (2010) [30] Milner, R.: Operational and algebraic semantics of concurrent processes, , 1201-1242 (1990) · Zbl 0900.68217 [31] Möller, M.; Olderog, E. -R.; Rasch, H.; Wehrheim, H.: Integrating a formal method into a software engineering process with UML and Java, Formal aspects of computing 20, 161-204 (2008) · Zbl 1141.68024 [32] Pérez-Toledano, M. Á.; Martínez, A. N.; Murillo, J. M.; Canal, C.: A safe dynamic adaptation framework for aspect-oriented software development, Journal of universal computer science 14, 2212-2238 (2008) [33] Reisig, W.: Petri nets: an introduction, EATCS monographs on theoretical computer science 4 (1985) · Zbl 0555.68033 [34] Rodrigues, N. F.; Barbosa, L. S.: Architectural prototyping: from CCS to .net, Entcs 130, 151-167 (2005) [35] Roscoe, A. W.: The theory and practice of concurrency, (1998) [36] J. Stafleu, UML description of Paradigm. Master’s thesis, LIACS, Leiden University, 2009. Technical Report 09–16. [37] A.W. Stam, Interaction protocols in PARADIGM: extensions to a modelling language through tool development. Ph.D. Thesis, LIACS, Leiden University, 2009. [38] Steen, M. R.; Groenewegen, L. P. J.; Oosting, G.: Parallel control processes: modular parallelism and communication, Proc. intelligent autonomous systems, 562-579 (1987) 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.