2020
Journal article  Open Access

Synthesis of orchestrations and choreographies: bridging the gap between supervisory control and coordination of services

Basile D., Ter Beek M. H., Pugliese R.

Orchestration  and Cluster Computing  Computer Science - Formal Languages and Automata Theory  Computer Science - Distributed  Controller Synthesis  FOS: Electrical engineering  Choreography  Electrical Engineering and Systems Science - Systems and Control  Parallel  Contract Automata  electronic engineering  FOS: Computer and information sciences  Systems and Control (eess.SY)  Distributed  and Cluster Computing (cs.DC)  Formal Languages and Automata Theory (cs.FL)  Service Contracts  information engineering 

We present a number of contributions to bridging the gap between supervisory control theory and coordination of services in order to explore the frontiers between coordination and control systems. Firstly, we modify the classical synthesis algorithm from supervisory control theory for obtaining the so-called most permissive controller in order to synthesise orchestrations and choreographies of service contracts formalised as contract automata. The key ingredient to make this possible is a novel notion of controllability. Then, we present an abstract parametric synthesis algorithm and show that it generalises the classical synthesis as well as the orchestration and choreography syntheses. Finally, through the novel abstract synthesis, we show that the concrete syntheses are in a refinement order. A running example from the service domain illustrates our contributions.

Source: Logical Methods in Computer Science 16 (2020). doi:10.23638/LMCS-16(2:9)2020

Publisher: Technische Universität Braunschweig, Institute of Theoretical Computer Science, Braunschweig, Germany, Germania


[1] Acciai, L., Boreale, M., Zavattaro, G.: Behavioural contracts with request-response operations. Sci. Comp. Program. 78(2), 248-267 (2013). https://doi.org/10.1016/j.scico.2011.10.007
[2] de Alfaro, L., Henzinger, T.: Interface Automata. In: ESEC/FSE. pp. 109-120. ACM (2001). https://doi.org/10.1145/503209.503226
[3] Alur, R., Dill, D.: A Theory of Timed Automata. Theoret. Comp. Sci. 126(2), 183-235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8
[4] Apel, S., Batory, D.S., Kästner, C., Saake, G.: Feature-Oriented Software Product Lines: Concepts and Implementation. Springer (2013). https://doi.org/10.1007/978-3-642-37521-7
[5] Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller Synthesis for Timed Automata. IFAC Proc. Vol. 31(18), 447-452 (1998). https://doi.org/10.1016/S1474-6670(17)42032-5
[6] Atampore, F., Dingel, J., Rudie, K.: Automated Service Composition Via Supervisory Control Theory. In: WODES. pp. 28-35. IEEE (2016). https://doi.org/10.1109/WODES.2016.7497822
[7] Azzopardi, S., Pace, G.J., Schapachnik, F., Schneider, G.: Contract automata: An operational view of contracts between interactive parties. Artif. Intell. Law 24(3), 203-243 (2016). https://doi.org/10.1007/s10506-016-9185-2
[8] Bartoletti, M., Cimoli, T., Zunino, R.: Compliance in Behavioural Contracts: A Brief Survey. In: Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 103-121. Springer (2015). https://doi.org/10.1007/978-3-319-25527-9_9
[9] Basile, D., ter Beek, M.H., Degano, P., Legay, A., Ferrari, G.L., Gnesi, S., Di Giandomenico, F.: Controller synthesis of service contracts with variability. Science of Computer Programming (2019), submitted
[10] Basile, D., ter Beek, M.H., Legay, A.: Timed service contract automata. Innovations Syst. Softw. Eng. (2019). https://doi.org/10.1007/s11334-019-00353-3
[11] Basile, D., ter Beek, M.H., Legay, A., Traonouez, L..M.: Orchestration Synthesis for Real-Time Service Contracts. In: VECoS. LNCS, vol. 11181, pp. 31-47. Springer (2018). https://doi.org/10.1007/978-3- 030-00359-3_3
[12] Basile, D., ter Beek, M.H., Pugliese, R.: Bridging the Gap Between Supervisory Control and Coordination of Services: Synthesis of Orchestrations and Choreographies. In: COORDINATION. LNCS, vol. 11533, pp. 129-147. Springer (2019). https://doi.org/10.1007/978-3-030-22397-7_8
[13] Basile, D., Degano, P., Ferrari, G.L.: Automata for Specifying and Orchestrating Service Contracts. Log. Meth. Comp. Sci. 12(4:6), 1-51 (2016). https://doi.org/10.2168/LMCS-12(4:6)2016
[14] Basile, D., Degano, P., Ferrari, G.L., Tuosto, E.: Playing with Our CAT and Communication-Centric Applications. In: FORTE. LNCS, vol. 9688, pp. 62-73. Springer (2016). https://doi.org/10.1007/978- 3-319-39570-8_5
[15] Basile, D., Degano, P., Ferrari, G.L., Tuosto, E.: Relating two automata-based models of orchestration and choreography. J. Log. Algebr. Meth. Program. 85(3), 425-446 (2016). https://doi.org/10.1016/j.jlamp.2015.09.011
[16] Basile, D., Di Giandomenico, F., Gnesi, S., Degano, P., Ferrari, G.L.: Specifying Variability in Service Contracts. In: VaMoS. pp. 20-27. ACM (2017). https://doi.org/10.1145/3023956.3023965
[17] Batory, D.S.: Feature Models, Grammars, and Propositional Formulas. In: SPLC. LNCS, vol. 3714, pp. 7-20. Springer (2005). https://doi.org/10.1007/11554844_3
[18] van Beek, D.A., Fokkink, W.J., Hendriks, D., Hofkamp, A., Markovski, J., van de Mortel-Fronczak, J.M., Reniers, M.A.: CIF 3: Model-Based Engineering of Supervisory Controllers. In: TACAS. LNCS, vol. 8413, pp. 575-580. Springer (2014). https://doi.org/10.1007/978-3-642-54862-8_48
[19] ter Beek, M.H., Bucchiarone, A., Gnesi, S.: Web Service Composition Approaches: From Industrial Standards to Formal Methods. In: ICIW. IEEE (2007). https://doi.org/10.1109/ICIW.2007.71
[20] ter Beek, M.H., Carmona, J., Hennicker, R., Kleijn, J.: Communication Requirements for Team Automata. In: COORDINATION. LNCS, vol. 10319, pp. 256-277. Springer (2017). https://doi.org/10.1007/978-3-319-59746-1_14
[21] ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: Model checking of modal transition systems with variability constraints. J. Log. Algebr. Meth. Program. 85(2), 287-315 (2016). https://doi.org/10.1016/j.jlamp.2015.11.006
[22] ter Beek, M.H., Reniers, M.A., de Vink, E.P.: Supervisory Controller Synthesis for Product Lines Using CIF 3. In: ISoLA. LNCS, vol. 9952, pp. 856-873. Springer (2016). https://doi.org/10.1007/978-3-319- 47166-2_59
[23] ter Beek, M.H., de Vink, E.P., Willemse, T.A.C.: Family-Based Model Checking with mCRL2. In: FASE. LNCS, vol. 10202, pp. 387-405. Springer (2017). https://doi.org/10.1007/978-3-662-54494-5_23
[24] Bouguettaya, A., Singh, M., Huhns, M., Sheng, Q.Z., Dong, H., Yu, Q., Neiat, A.G., Mistry, S., Benatallah, B., Medjahed, B., Ouzzani, M., Casati, F., Liu, X., Wang, H., Georgakopoulos, D., Chen, L., Nepal, S., Malik, Z., Erradi, A., Wang, Y., Blake, B., Dustdar, S., Leymann, F., Papazoglou, M.: A Service Computing Manifesto: The Next 10 Years. Commun. ACM 60(4), 64-72 (2017). https://doi.org/10.1145/2983528
[25] Bruni, R., Lanese, I., Melgratti, H.C., Tuosto, E.: Multiparty Sessions in SOC. In: COORDINATION. LNCS, vol. 5052, pp. 67-82. Springer (2008). https://doi.org/10.1007/978-3-540-68265-3_5
[26] Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Springer (2006). https://doi.org/10.1007/978-0-387-68612-7
[27] Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient On-the-Fly Algorithms for the Analysis of Timed Games. In: CONCUR. LNCS, vol. 3653, pp. 66-80. Springer (2005). https://doi.org/10.1007/11539452_9
[28] Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On Global Types and Multi-Party Sessions. Log. Meth. Comp. Sci. 8(1:24), 1-45 (2012). https://doi.org/10.2168/LMCS-8(1:24)2012
[29] Castagna, G., Gesbert, N., Padovani, L.: A Theory of Contracts for Web Services. ACM Trans. Program. Lang. Syst. 31(5), 19:1-19:61 (2009). https://doi.org/10.1145/1538917.1538920
[30] Classen, A., Cordy, M., Schobbens, P..Y., Heymans, P., Legay, A., Raskin, J..F.: Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking. IEEE Trans. Softw. Eng. 39(8), 1069-1089 (2013). https://doi.org/10.1109/TSE.2012.86
[31] Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, W., Willemse, T.A.C.: An Overview of the mCRL2 Toolset and Its Recent Advances. In: TACAS. LNCS, vol. 7795, pp. 199-213. Springer (2013). https://doi.org/http://dx.doi.org/10.1007/978-3-642-36742-7_15
[32] Darondeau, P., Dubreil, J., Marchand, H.: Supervisory Control for Modal Specifications of Services. IFAC Proc. Vol. 43(12), 418-425 (2010). https://doi.org/10.3182/20100830-3-DE-4013.00069
[33] David, A., Larsen, K.G., Legay, A., Nyman, U., Wąsowski, A.: Timed I/O Automata: A Complete Specification Theory for Real-time Systems. In: HSCC. pp. 91-100. ACM (2010). https://doi.org/10.1145/1755952.1755967
[34] Dezani-Ciancaglini, M., de'Liguoro, U.: Sessions and Session Types: An Overview. In: WS-FM. LNCS, vol. 6194, pp. 1-28. Springer (2010). https://doi.org/10.1007/978-3-642-14458-5_1
[35] Feuillade, G., Pinchinat, S.: Modal Specifications for the Control Theory of Discrete Event Systems. Discrete Event Dyn. Syst. 17(2), 211-232 (2007). https://doi.org/10.1007/s10626-006-0008-6
[36] Gierds, C., Mooij, A.J., Wolf, K.: Reducing Adapter Synthesis to Controller Synthesis. IEEE Trans. Services Computing 5(1), 72-85 (2012). https://doi.org/10.1109/TSC.2010.57
[37] Gohari, P., Wonham, W.M.: On the complexity of supervisory control design in the RW framework. IEEE Trans. Syst., Man, Cybern. B, Cybern. 30(5), 643-652 (2000). https://doi.org/10.1109/3477.875441
[38] Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. In: POPL. pp. 273-284. ACM (2008). https://doi.org/10.1145/1328438.1328472
[39] Hüttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., Carbone, M., Deniélou, P..M., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Torres Vieira, H., Zavattaro, G.: Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv. 49(1), 3:1-3:36 (2016). https://doi.org/10.1145/2873052
[40] Kavantzas, N., Burdett, D., Ritzinger, G., Fletcher, T., Lafon, Y., Barreto, C.: Web Services Choreography Description Language v1.0. https://www.w3.org/TR/ws-cdl-10/ (2005)
[41] Křetínský, J.: 30 Years of Modal Transition Systems: Survey of Extensions and Analysis. In: Models, Algorithms, Logics and Tools, LNCS, vol. 10460, pp. 36-74. Springer (2017). https://doi.org/10.1007/978- 3-319-63121-9_3
[42] Laneve, C., Padovani, L.: An algebraic theory for web service contracts. Form. Asp. Comp. 27(4), 613-640 (2015). https://doi.org/10.1007/s00165-015-0334-2
[43] Lange, J., Tuosto, E., Yoshida, N.: From Communicating Machines to Graphical Choreographies. In: POPL. pp. 221-232. ACM (2015). https://doi.org/10.1145/2676726.2676964
[44] Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O Automata for Interface and Product Line Theories. In: ESOP. LNCS, vol. 4421, pp. 64-79. Springer (2007). https://doi.org/10.1007/978-3-540-71316-6_6
[45] Lynch, N., Tuttle, M.: An Introduction to Input/Output Automata. CWI Q. 2, 219-246 (1989)
[46] Michaux, J., Najm, E., Fantechi, A.: Session types for safe Web service orchestration. J. Log. Algebr. Program. 82(8), 282-310 (2013). https://doi.org/10.1016/j.jlap.2013.05.004
[47] Peltz, C.: Web Services Orchestration and Choreography. IEEE Comp. 36(10), 46-52 (2003)
[48] Pohl, K., Böckle, G., van der Linden, F.J.: Software Product Line Engineering: Foundations, Principles, and Techniques. Springer (2005). https://doi.org/10.1007/3-540-28901-1
[49] Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206-230 (1987). https://doi.org/10.1137/0325013
[50] Yi, Q., Liu, X., Bouguettaya, A., Medjahed, B.: Deploying and managing Web services: issues, solutions, and directions. VLDB J. 17(3), 735-572 (2008). https://doi.org/10.1007/s00778-006-0020-3

Metrics



Back to previous page
BibTeX entry
@article{oai:it.cnr:prodotti:423262,
	title = {Synthesis of orchestrations and choreographies: bridging the gap between supervisory control and coordination of services},
	author = {Basile D. and Ter Beek M.  H. and Pugliese R.},
	publisher = {Technische Universität Braunschweig, Institute of Theoretical Computer Science, Braunschweig, Germany, Germania},
	doi = {10.23638/lmcs-16(2:9)2020 and 10.48550/arxiv.1910.00849},
	journal = {Logical Methods in Computer Science},
	volume = {16},
	year = {2020}
}