Automated synthesis of application-layer connectors from automata-based specifications. (English) Zbl 1423.68066
Summary: Ubiquitous and Pervasive Computing, and the Internet of Things, promote dynamic interaction among heterogeneous systems. To achieve this vision, interoperability among heterogeneous systems represents a key enabler, and mediators are often built to solve protocol mismatches. Many approaches propose the synthesis of mediators. Unfortunately, a rigorous characterization of the concept of interoperability is still lacking, hence making hard to assess their applicability and soundness. In this paper, we provide a framework for the synthesis of mediators that allows us to: (i) characterize the conditions for the mediator existence and correctness; and (ii) establish the applicability boundaries of the synthesis method.
MSC:
| 68M14 | Distributed systems |
| 68M12 | Network protocols |
| 68Q45 | Formal languages and automata |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Keywords:
automated mediator synthesis; interoperability; protocols; heterogeneous applications; communication; coordination; protocol mismatchesSoftware:
LearnLibReferences:
| [1] | Weiser, M., The computer for the 21st century, Sci. Am., 265, 3, 94-104 (1991) |
| [2] | Atzori, L.; Lera, A.; Morabito, G., The Internet of things: a survey, Comput. Netw., 54, 15, 2787-2805 (2010) · Zbl 1208.68071 |
| [3] | Inverardi, P.; Autili, M.; Di Ruscio, D.; Pelliccione, P.; Tivoli, M., Producing software by integration: challenges and research directions (keynote), (Proc. of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013 (2013), ACM: ACM New York, NY, USA), 2-12 |
| [4] | Calvert, K. L.; Lam, S. S., Formal methods for protocol conversion, IEEE J. Sel. Areas Commun., 8, 1, 127-142 (1990) |
| [5] | Lam, S. S., Correction to “protocol conversion”, IEEE Trans. Softw. Eng., 14, 9, 1376 (1988) |
| [6] | Okumura, K., A formal protocol conversion method, (SIGCOMM (1986)), 30-37 |
| [7] | Kumar, R.; Nelvagal, S.; Marcus, S. I., A discrete event systems approach for protocol conversion, Discret. Event Dyn. Syst., 7, 3 (1997) · Zbl 0960.93034 |
| [8] | Yellin, D. M.; Strom, R. E., Protocol specifications and component adaptors, ACM Trans. Program. Lang. Syst., 19 (1997) |
| [9] | Canal, C.; Poizat, P.; Salaün, G., Model-based adaptation of behavioral mismatching components, IEEE Trans. Softw. Eng., 34, 4, 546-563 (2008) |
| [10] | Benatallah, B.; Casati, F.; Grigori, D.; Nezhad, H. R.M.; Toumani, F., Developing adapters for web services integration, (Proceedings of the International Conference on Advanced Information Systems Engineering (CAiSE) (2005), Springer Verlag: Springer Verlag Porto, Portugal), 415-429 |
| [11] | Motahari Nezhad, H. R.; Xu, G. Y.; Benatallah, B., Protocol-aware matching of web service interfaces for adapter development, (Proceedings of the 19th International Conference on World Wide Web, WWW ’10 (2010), ACM: ACM New York, NY, USA), 731-740 |
| [12] | Wiederhold, G.; Genesereth, M., The conceptual basis for mediation services, IEEE Intell. Syst. Appl., 12, 5, 38-47 (1997) |
| [13] | Vaculín, R.; Sycara, K., Towards automatic mediation of OWL-S process models, (IEEE International Conference on Web Services (2007)), 1032-1039 |
| [14] | Vaculín, R.; Neruda, R.; Sycara, K. P., An agent for asymmetric process mediation in open environments, (Kowalczyk, R.; Huhns, M. N.; Klusch, M.; Maamar, Z.; Vo, Q. B., SOCASE. SOCASE, Lecture Notes in Computer Science, vol. 5006 (2008), Springer), 104-117 |
| [15] | Motahari Nezhad, H. R.; Benatallah, B.; Martens, A.; Curbera, F.; Casati, F., Semi-automated adaptation of service interactions, (WWW ’07: Proceedings of the 16th International Conference on World Wide Web (2007), ACM: ACM New York, NY, USA), 993-1002 |
| [16] | Williams, S. K.; Battle, S. A.; Cuadrado, J. E., Protocol mediation for adaptation in semantic web services, (ESWC (2006)), 635-649 |
| [17] | Spalazzese, R.; Inverardi, P.; Issarny, V., Towards a formalization of mediating connectors for on the fly interoperability, (Proceedings of the Joint Working IEEE/IFIP Conference on Software Architecture and European Conference on Software Architecture (WICSA/ECSA 2009) (2009)), 345-348 |
| [18] | Inverardi, P.; Issarny, V.; Spalazzese, R., A Theory of Mediators for Eternal Connectors, Proceedings of ISoLA 2010 - 4th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Part II, vol. 6416, 236-250 (2010), Springer: Springer Heidelberg |
| [19] | Spitznagel, B.; Garlan, D., A compositional formalization of connector wrappers, (ICSE (2003)), 374-384 |
| [20] | Autili, M.; Inverardi, P.; Mignosi, F.; Spalazzese, R.; Tivoli, M., Automated synthesis of application-layer connectors from automata-based specifications, (Dediu, A.-H.; Formenti, E.; Martín-Vide, C.; Truthe, B., Language and Automata Theory and Applications. Language and Automata Theory and Applications, Lecture Notes in Computer Science, vol. 8977 (2015), Springer International Publishing), 3-24 · Zbl 1423.68065 |
| [21] | Keller, R. M., Formal verification of parallel programs, Commun. ACM, 19, 7, 371-384 (1976) · Zbl 0329.68016 |
| [22] | Lo, D.; Mariani, L.; Santoro, M., Learning extended FSA from software: an empirical assessment, J. Syst. Softw., 85, 9 (2012) |
| [23] | Lorenzoli, D.; Mariani, L.; Pezzè, M., Automatic generation of software behavioral models, (Proc. of ICSE08 (2008)) |
| [24] | Ernst, M. D.; Cockrell, J.; Griswold, W. G.; Notkin, D., Dynamically discovering likely program invariants to support program evolution, IEEE Trans. Software Eng., 27, 2 (2001) |
| [25] | Dallmeier, V.; Knopp, N.; Mallon, C.; Fraser, G.; Hack, S.; Zeller, A., Automatically generating test cases for specification mining, IEEE Trans. Softw. Eng., 38, 2 (2011) |
| [26] | Bertolino, A.; Inverardi, P.; Pelliccione, P.; Tivoli, M., Automatic synthesis of behavior protocols for composable web-services, (Proc. of ESEC/FSE (2009)) |
| [27] | Raffelt, H.; Steffen, B.; Berg, T.; Margaria, T., Learnlib: a framework for extrapolating behavioral models, Int. J. Softw. Tools Technol. Transf., 11, 5 (2009) |
| [28] | Milner, R., Communication and Concurrency, PHI Series in Computer Science (1989), Prentice Hall · Zbl 0683.68008 |
| [29] | Uchitel, S.; Kramer, J.; Magee, J., Incremental elaboration of scenario-based specifications and behavior models using implied scenarios, ACM Trans. Softw. Eng. Methodol., 13, 1, 37-85 (2004) |
| [30] | Margaria, T., The semantic web services challenge: tackling complexity at the orchestration level, (ICECCS’08 (2008)) |
| [31] | Lausen, H.; Küster, U.; Petrie, C.; Zaremba, M.; Komazec, S., SWS Challenge Scenarios, 13-27 (2009), Springer US: Springer US Boston, MA |
| [32] | Spalazzese, R.; Inverardi, P., Mediating connector patterns for components interoperability, (ECSA (2010)), 335-343 |
| [33] | Aßmann, U.; Zschaler, S.; Wagner, G., Ontologies, Meta-Models, and the Model-Driven Paradigm (2006), Springer |
| [34] | Kalfoglou, Y.; Schorlemmer, M., Ontology mapping: the state of the art, Knowl. Eng. Rev., 18, 1 (2003) |
| [35] | Baader, F.; Calvanese, D.; McGuinness, D. L.; Nardi, D.; Patel-Schneider, P. F., The Description Logic Handbook (2003), Cambridge University Press · Zbl 1058.68107 |
| [36] | Tivoli, M.; Inverardi, P., Failure-free coordinators synthesis for component-based architectures, Sci. Comput. Program., 71, 3, 181-212 (2008) · Zbl 1151.68463 |
| [37] | Autili, M.; Chilton, C.; Inverardi, P.; Kwiatkowska, M. Z.; Tivoli, M., Towards a connector algebra, (Leveraging Applications of Formal Methods, Verification, and Validation, ISoLA 2010. Leveraging Applications of Formal Methods, Verification, and Validation, ISoLA 2010, Heraklion, Crete, Greece, 18-21 October, 2010, Proceedings, Part II (2010)), 278-292 |
| [38] | Davis, R.; Shrobe, H.; Szolovits, P., What is a knowledge representation?, AI Mag., 14, 1, 17-33 (1993) |
| [39] | Sowa, J. F., Knowledge Representation: Logical, Philosophical and Computational Foundations (2000), Brooks/Cole Publishing Co.: Brooks/Cole Publishing Co. Pacific Grove, CA, USA |
| [40] | Brachman, R.; Levesque, H., Knowledge Representation and Reasoning (2004), Morgan Kaufmann Publishers Inc.: Morgan Kaufmann Publishers Inc. San Francisco, CA, USA |
| [41] | van Harmelen, F.; van Harmelen, F.; Lifschitz, V.; Porter, B., Handbook of Knowledge Representation (2007), Elsevier Science: Elsevier Science San Diego, USA |
| [42] | (Staab, S.; Studer, R., Handbook on Ontologies, International Handbooks on Information Systems (2004), Springer) · Zbl 1429.68001 |
| [43] | Studer, R.; Benjamins, V. R.; Fensel, D., Knowledge engineering: principles and methods, Data Knowl. Eng., 25, 1-2, 161-197 (1998) · Zbl 0896.68114 |
| [44] | Baader, F.; Horrocks, I.; Sattler, U., Description Logics, 21-43 (2009), Springer: Springer Berlin Heidelberg, Berlin, Heidelberg |
| [45] | Kalfoglou, Y.; Schorlemmer, M., Ontology mapping: the state of the art, Knowl. Eng. Rev., 18, 1, 1-31 (2003) |
| [46] | Pavel, S.; Euzenat, J., Ontology matching: state of the art and future challenges, IEEE Trans. Knowl. Data Eng., 25, 1, 158-176 (2013) |
| [47] | Wiederhold, G., Mediators in the architecture of future information systems, IEEE Computer, 25, 38-49 (1992) |
| [48] | Cavallaro, L.; Nitto, E. D.; Pradella, M., An automatic approach to enable replacement of conversational services, (ICSOC/ServiceWave (2009)) |
| [49] | Stollberg, M.; Cimpian, E.; Mocan, A.; Fensel, D., A semantic web mediation architecture, (Proceedings of the 1st Canadian Semantic Web Working Symposium, CSWWS 2006 (2006), Springer) |
| [50] | Cimpian, E.; Mocan, A., Wsmx process mediation based on choreographies, (Bussler, C.; Haller, A., Business Process Management Workshops, vol. 3812 (2005)), 130-143 |
| [51] | Passerone, R.; de Alfaro, L.; Henzinger, T. A.; Sangiovanni-Vincentelli, A. L., Convertibility verification and converter synthesis: two faces of the same coin, (Proceedings of the 2002 IEEE/ACM International Conference on Computer-Aided Design, ICCAD ’02 (2002)), 132-139 |
| [52] | Bruni, R.; Lanese, I.; Montanari, U., A basic algebra of stateless connectors, Theor. Comput. Sci., 366, 1, 98-120 (2006) · Zbl 1153.68331 |
| [53] | Inverardi, P.; Tivoli, M., Automatic synthesis of modular connectors via composition of protocol mediation patterns, (Proceedings of ICSE’13 (2013)) |
| [54] | Bennaceur, A.; Chilton, C.; Isberner, M.; Jonsson, B., Automated mediator synthesis: combining behavioural and ontological reasoning, (Software Engineering and Formal Methods - 11th International Conference, SEFM 2013. Software Engineering and Formal Methods - 11th International Conference, SEFM 2013, Madrid, Spain, 25-27 September, 2013, Proceedings (2013)), 274-288 |
| [55] | Bennaceur, A.; Issarny, V., Automated synthesis of mediators to support component interoperability, IEEE Trans. Softw. Eng., 41, 3, 221-240 (2015) |
| [56] | Autili, M.; Inverardi, P.; Tivoli, M., Choreography realizability enforcement through the automatic synthesis of distributed coordination delegates, Sci. Comput. Program., 160, 3-29 (2018) |
| [57] | Basu, S.; Bultan, T.; Ouederni, M., Deciding choreography realizability, (Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’12 (2012)), 191-202 · Zbl 1321.68183 |
| [58] | Basu, S.; Bultan, T., Automated choreography repair, (Fundamental Approaches to Software Engineering (2016), Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg), 13-30 |
| [59] | Tivoli, M.; Autili, M., Synthesis, a tool for synthesizing correct and protocol-enhanced adaptors, RSTI - L’objet, Coordination and Adaptation Techniques, 12, 1, 77-103 (2006) |
| [60] | Autili, M.; Mostarda, L.; Navarra, A.; Tivoli, M., Synthesis of decentralized and concurrent adaptors for correctly assembling distributed component-based systems, J. Syst. Softw., 81, 12, 2210-2236 (2008) |
| [61] | Autili, M.; Inverardi, P.; Tivoli, M., Automated synthesis of service choreographies, IEEE Softw., 32, 1, 50-57 (2015) |
| [62] | Autili, M.; Di Salle, A.; Gallo, F.; Pompilio, C.; Tivoli, M., Aiding the realization of service-oriented distributed systems, (34th Annual ACM Symp. on Applied Computing, SAC ’19 (2019)) |
| [63] | Diekert, V.; Rozenberg, G., The Book of Traces (1995), World Scientific |
| [64] | Nostro, N.; Spalazzese, R.; Giandomenico, F. D.; Inverardi, P., Achieving functional and non functional interoperability through synthesized connectors, J. Syst. Softw., 111, 185-199 (2016) |
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.
