Kokash, Natallia; Krause, Christian; De Vink, Erik Reo + \(\mathrm{mCRL2}\): a framework for model-checking dataflow in service compositions. (English) Zbl 1259.68129 Formal Asp. Comput. 24, No. 2, 187-216 (2012). Cited in 3 Documents MSC: 68Q60 Specification and verification (program logics, model checking, etc.) Keywords:formal methods for service-oriented computing; model checking; coordination languages Software:Design/CPN; Reo; PRISM; Woflan; CPN/Tools; TINA; mCRL2 PDFBibTeX XMLCite \textit{N. Kokash} et al., Formal Asp. Comput. 24, No. 2, 187--216 (2012; Zbl 1259.68129) Full Text: DOI References: [1] van der Aalst WMP (1998) The application of Petri nets to workflow management. J. Circuits Syst and Comput 8: 21–66 [2] van der Aalst WMP (1999) Woflan: a Petri-net-based workflow analyzer. Syst Anal Model Simul 35: 345–357 · Zbl 1030.68877 [3] Arbab F, Baier C, de Boer F, Rutten J, Sirjani M (2005) Synthesis of Reo circuits for implementation of component-connector automata specifications. In: Proceedings of COORDINATION’05. LNCS, vol 3454, pp 236–251 [4] Arbab F, Baier C, de Boer F, Rutten J (2007) Models and temporal logical specifications for timed component connectors. Softw Syst Model 6: 59–82 · Zbl 05149644 [5] Arbab F, Chothia T, van der Mei R, Sun M, Moon YJ, Verhoef C (2009) From coordination to stochastic models of QoS. In: Field J, Vasconcelos VT (eds) Proceedings of COORDINATION 2009. LNCS, vol 5521, pp 268–287 [6] Arbab F, Chothia T, Sun M, Moon Y-J (2007) Component connectors with QoS guarantees. In: Proceedings of COORDINATION 2007. LNCS, vol 4467, pp 286–304 [7] Alur R, Dill D (1994) A theory of timed automata. Theor Comput Sci 126(2): 183–235 · Zbl 0803.68071 [8] Arbab F, Koehler C, Maraikar Z, Moon YJ, Proenca J (2008) Modeling, testing and executing Reo connectors with the Eclipse Coordination Tools. Tool demo session at FACS’08 [9] Arbab F (1996) The IWIM model for coordination of concurrent activities. In: Ciancarini P, Hankin C (eds) Proceedings of COORDINATION’96. LNCS vol 1061, pp 34–56 [10] Arbab F (2004) Reo: a channel-based coordination model for component composition. Math Struct Comput Sci 14: 329–366 · Zbl 1085.68552 [11] Baier C (2005) Probabilistic models for Reo connector circuits. J Univers Comput Sci 11(10): 1718–1748 [12] Barbosa MA, Barbosa LS, Campos JC (2010) A coordination model for interactive components. In: Arbab F, Sirjani M (eds) Proceedings FSEN 2009. LNCS, vol 5961 pp 416–430 · Zbl 1274.68063 [13] Baier C, Blechmann T, Klein J, Klüppelholz S (2009) A uniform framework for modeling and verifying components and connectors. In: Field J, Vasconcelos VT (eds) Proceedings of COORDINATION 2009. LNCS, vol 5521 pp 268–287 · Zbl 1254.68143 [14] Baeten JCM, Basten T, Reniers MA (2010) Process algebra: equational theories of communicating processes. Number 50 in Cambridge Tracts in Theoretical Computer Science. CUP [15] Bonsangue M, Clarke D, Silva A (2009) Automata for context-dependent connectors. In Field J, Vasconcelos VT (eds) Proceedings of COORDINATION 2009. LNCS, vol 5521, pp 184–203 [16] ter Beek MH et al (2009) CMC-UMC: a framework for the verification of abstract service oriented properties. In: Proceedings of SAC’09. ACM, pp 2111–2117 [17] Bocchi L et al (2009) From architectural to behavioural specification of services. ENTCS 253: 3–21 [18] Berthomieu B, Ribet PO, Vernadat F (2004) The tool TINA: construction of abstract state spaces for Petri nets and time Petri nets. Int J Prod Res 42: 2741–2756 · Zbl 1060.68695 [19] Baier C, Sirjani M, Arbab F, Rutten J (2006) Modeling component connectors in Reo by constraint automata. Sci Comput Program 61: 75–113 · Zbl 1105.68058 [20] Clarke D, Costa D, Arbab F (2007) coloring I: Synchronization and context dependency. Sci Comput Program 66: 205–225 · Zbl 1121.68015 [21] Chothia T, Kleijn J (2007) Q-automata: modelling the resource usage of concurrent components. ENTCS 175: 153–167 [22] Changizi B, Kokash N, Arbab F (2010) A unified toolset for business process model formalization. In: Happe J, Buhnova B (eds) Proceedings of FESCA 2010. ENTCS, pp 147–156 [23] Costa D (2010) Formal models for context dependent connectors for distributed software components and services. PhD thesis, Vrije Universiteit Amsterdam [24] Clarke D, Proenca J, Lazovik A, Arbab F (2008) Deconstructing Reo. In: Canal C, Poizat P, Sirjani M (eds) Proceedings of FOCLASA 2008. ENTCS, vol 229, pp 43–58 [25] Groote JF et al (2007) The formal specification language $${{\(\backslash\)tt mCRL2}}$$ . In: Brinksma E et al (eds) Methods for modelling software systems. IBFI, Schloss Dagstuhl, pp 1–34 [26] Guermouche N, Godart C (2009) Asynchronous timed web service-aware choreography analysis. In: van Eck P et al (eds) Proceedings of CAiSE. LNCS, vol 5565, pp 364–378 [27] Gorton S, Montangero C, Reiff-Marganiec S, Semini L (2007) StPowla: SOA, policies and workflows. In: Di Nitto E, Ripeanu M (eds) Proceedings of ICSOC Workshops. LNCS, vol 4907, pp 351–362 · Zbl 1141.68511 [28] Guermouche N, Perrin O, Ringeissen C (2008) Timed specification for web services compatibility analysis. ENTCS 200: 155–170 [29] Huang S-M, Chu Y-T, Li S-H, Yen DC (2007) Enhancing conflict detecting mechanism for web services composition: a business process flow model transformation approach. Sci Comput Program 66(3): 205–225 · Zbl 1121.68015 [30] Hidders J, Kwasnikowska N, Sroka J, Tyszkiewicz J, den Bussche JV (2005) Petri net + nested relational calculus = dataflow. In: Meersman R et al (eds) Proceedings of CoopIS. LNCS, vol 3760, pp 220–237 [31] Hidders J, Kwasnikowska N, Sroka J, Tyszkiewicz J, den Bussche JV (2008) DFL: a dataflow language based on Petri nets and nested relational calculus. Inf Syst 33: 261–284 · Zbl 05353622 [32] Haller A, Oren E, Petkov S (2005) Survey of workflow management systems. Technical Report 2005-05-02, DERI [33] Hee van K, Post R, Somers L (2005) Yet another smart process editor. In: Feliz-Teixeira J, Carvalho Brito AE (eds) Proceedings of ESM’05, pp 527–530 [34] Ibanez MJ, Alvarez P, Ezpeleta J (2008) Flow and data compatibility for the correct interaction between web processes. In: Mohammadian M (ed) Proceedings of CIMCA-IAWTIC-ISE. IEEE, pp 715–721 [35] Jongmans S-STQ, Krause C, Arbab F (2011) Encoding context-sensitivity in reo into non-context-sensitive semantic models. In: Proceedings of COORDINATION 2011. LNCS, vol 6721, pp 31–48 [36] Kokash N, Changizi B, Arbab F (2010) A semantic model for service composition with coordination time delays. In: Dong JS, Zhu H (eds) Proceedings of ICFEM. LNCS, vol 6447, pp 106–121 [37] Kemper S (2009) SAT-based verification for timed component connectors. ENTCS 255: 103–118 · Zbl 1366.68172 [38] Kraemer FA, Herrmann P (2006) Service specification by composition of collaborations: an example. In: Proceedings of SerComp. IEEE pp 129–133 [39] Kokash N, Krause C, de Vink EP (2010) Data-aware design and verification of service composition with Reo and $${{\(\backslash\)tt mCRL2}}$$ . In: Proceedings of SAC 2010. ACM pp 2406–2413 [40] Kokash N, Krause C, de Vink EP (2010) Verification of context-dependent channel-based service models. In: de Boer F, Bonsangue M, Hallerstede S, and Leuschel M (eds) Proceedings of FMCO 2009. LNCS, vol 6286, pp 21–40 · Zbl 1312.68073 [41] Kokash N, Krause C, de Vink EP (2010) Time and data aware analysis of graphical service models in Reo. In: Maggiolo-Schettini A, Fiadeiro JL, Gnesi S (eds) Proceedings of SEFM’10. IEEE, pp 125–134 [42] Kwiatkowska M, Norman G, Parker D (2002) PRISM: probabilistic symbolic model checker. In: Field T, Harrison PG, Bradley JT, Harder U (eds) Proceedings of TOOLS 2002. LNCS, vol 2324, pp 200–204 · Zbl 1047.68533 [43] Kazhamiakin R, Pistore M (2006) Static verification of control and data in web service compositions. In: ICWS’06. IEEE, pp 83–90 · Zbl 1225.68032 [44] Kazhamiakin R, Pandya PK, Pistore M (2006) Timed modelling and analysis in web service compositions. In: ARES’06. IEEE, pp 840–846 [45] Krause C (2011) Reconfigurable Component Connectors. PhD thesis, Leiden University, The Netherlands [46] Lime D, Roux OH, Seidner C, Traonouez L-M (2009) Roméo: a parametric model-checker for Petri nets with stopwatches. In: Kowalewski S, Philippou A (eds) Proceedings of TACAS 2009. LNCS, vol 5505 pp 54–57 [47] Milner R (1989) Communication and concurrency. Prentice-Hall, Inc. Upper Saddle River · Zbl 0683.68008 [48] Mousavi M, Sirjani M, Arbab F (2006) Formal semantics and analysis of component connectors in Reo. Electron Notes Theor Comput Sci 154(1): 83–99 [49] Ratzer A et al (2003) CPN tools for editing, simulating, and analysing coloured Petri nets. In: van der Aalst WMP, Best E (eds) Proceedings of ICATPN 2003. LNCS, vol 2679, pp 450–462 [50] Raedts I, Petkovic M, Usenko YS, van der Werf JM, Groote JF, Somers L (2007) Transformation of BPMN models for behaviour analysis. In: Augusto JC, Barjis J, Ultes-Nitsche U (eds) Proceedings of MSVVEIS 2007. INSTICC Press, pp 126–137 [51] Trčka N, van der Aalst W, Sidorova N (2008) Analyzing control-flow and data-flow in workflow processes in a unified way. Technical report, Technische Universiteit Eindhoven 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.