nach oben

Erschienen in:

2024 | OriginalPaper | Buchkapitel

Formalizing Microservices Patterns with Event-B: The Case of Service Registry

verfasst von : Sebastián Vergara, Laura González, Raúl Ruggia

Erschienen in: Service-Oriented Computing – ICSOC 2023 Workshops

Verlag: Springer Nature Singapore

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Microservices have emerged as an architectural style in which applications are composed of small and focused services. Several patterns have been proposed to guide the construction of microservices applications. However, they are usually stated in natural-language, which may lead to ambiguity and erroneous application. This paper addresses these issues by advancing in the formalization of microservices patterns using the Event-B method. An Event-B model for the Service Registry pattern is proposed, which is then leveraged for verification/validation purposes. The overall goal is to contribute to the comprehension of microservices patterns and the quality of microservices applications.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Towards a Systematic Comparison Framework for Cloud Services Customer Agreements

Nächstes Kapitel Privacy Engineering in the Data Mesh: Towards a Decentralized Data Privacy Governance Framework

Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, Cambridge (2010)CrossRef

Abrial, J.R.: On B and Event-B: principles, success and challenges. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. LNCS, vol. 10817, pp. 31–35. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4_3CrossRef

Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447–466 (2010). https://doi.org/10.1007/s10009-010-0145-yCrossRef

Afendi, M.: A correct by construction approach for the modeling and the verification of cyber-physical systems in Event-B. In: Raschke, A., Méry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 401–404. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_31CrossRef

Ait-Sadoune, I., Ait-Ameur, Y.: Formal modelling and verification of transactional web service composition: a refinement and proof approach with Event-B. In: Thalheim, B., Schewe, K.D., Prinz, A., Buchberger, B. (eds.) Correct Software in Web Applications and Web Services. TEXTSMONOGR, pp. 1–27. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17112-8_1CrossRef

Alencar, P.S.C., Cowan, D.D., de Lucena, C.J.P.: A formal approach to architectural design patterns. In: Gaudel, M.C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 576–594. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-60973-3_108CrossRef

Bayley, I., Zhu, H.: Formal specification of the variants and behavioural features of design patterns. J. Syst. Softw. 83(2), 209–221 (2010)CrossRef

Bergner, K.: Specification of Large ß Object Networks with Component Diagrams. CS-Press (1997)

Bravetti, M., Giallorenzo, S., Mauro, J., Talevi, I., Zavattaro, G.: A formal approach to microservice architecture deployment. In: Bucchiarone, A., et al. (eds.) Microservices, pp. 183–208. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-31646-4_8CrossRef

10.

Bryans, J.W., Wei, W.: Formal analysis of BPMN models using Event-B. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 33–49. Springer, Cham (2010). https://doi.org/10.1007/978-3-642-15898-8_3CrossRef

11.

Camilli, M., Bellettini, C., Capra, L., Monga, M.: A formal framework for specifying and verifying microservices based process flows. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 187–202. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-74781-1_14CrossRef

12.

Dwivedi, A.K., Rath, S.K., Chakravarthy, S.L.: Formalization of SOA design patterns using model-based specification technique. In: Chaki, N., Devarakonda, N., Sarkar, A., Debnath, N. (eds.) ICCIDE 2018. LNDECT, vol. 28, pp. 95–101. Springer, Singapore (2019). https://doi.org/10.1007/978-981-13-6459-4_11CrossRef

13.

González, L., Ruggia, R.: Formalizing a policy-based compliance control solution with Event-B. In: Proceedings of the 14th International Conference on Software Technologies. SCITEPRESS (2019)

14.

Hachicha, M., Dammak, E., Halima, R.B., Kacem, A.H.: A correct by construction approach for modeling and formalizing self-adaptive systems. In: 2016 17th IEEE/ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing (SNPD), pp. 379–384. IEEE (2016)

15.

Hallerstede, S.: On the purpose of Event-B proof obligations. Formal Aspects Comput. 23, 133–150 (2011). https://doi.org/10.1007/s00165-009-0138-3CrossRef

16.

Ladenberger, L., Leuschel, M.: BMotionWeb: a tool for rapid creation of formal prototypes. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 403–417. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41591-8_27CrossRef

17.

Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transfer 10(2), 185–203 (2008). https://doi.org/10.1007/s10009-007-0063-9CrossRef

18.

Llambías, G., Ruggia, R.: A middleware-based platform for the integration of bioinformatic services. CLEI Electron. J. 18 (2015)

19.

Marmsoler, D.: A framework for interactive verification of architectural design patterns in Isabelle/HOL. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 251–269. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02450-5_15CrossRef

20.

Mikkonen, T.: Formalizing design patterns. In: Proceedings of the 20th International Conference on Software Engineering, pp. 115–124. IEEE (1998)

21.

Montero, S., Díaz, P., Aedo, I.: Formalization of web design patterns using ontologies. In: Menasalvas, E., Segovia, J., Szczepaniak, P.S. (eds.) AWIC 2003. LNCS, vol. 2663, pp. 179–188. Springer, Cham (2003). https://doi.org/10.1007/3-540-44831-4_19CrossRef

22.

Nicholson, J., Eden, A.H., Gasparis, E., Kazman, R.: Automated verification of design patterns: a case study. Sci. Comput. Program. 80, 211–222 (2014)CrossRef

23.

ProB: Test case generation - ProB documentation (2023). https://prob.hhu.de/w/index.php?title=Test_Case_Generation

24.

Richardson, C.: Microservices Patterns: With Examples in Java, 1st edn. Manning Publications (2018)

25.

Ritter, D., Rinderle-Ma, S., Montali, M., Rivkin, A., Sinha, A.: Formalizing application integration patterns. In: 2018 IEEE 22nd International Enterprise Distributed Object Computing Conference (EDOC), pp. 11–20. IEEE (2018)

26.

Romanovsky, A., Thomas, M. (eds.): Industrial Deployment of System Engineering Methods. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-33170-1CrossRef

27.

Schieferdecker, I.: Model-based testing. IEEE Softw. 29(1), 14–18 (2012). https://doi.org/10.1109/MS.2012.13CrossRef

28.

Taibi, D., Lenarduzzi, V., Pahl, C.: Architectural patterns for microservices: a systematic mapping study. In: Proceedings of the 8th International Conference on Cloud Computing and Services Science, Portugal. SCITEPRESS (2018)

29.

Taibi, T., Ngo, D.C.L.: Formal specification of design patterns - a balanced approach. J. Object Technol. 2(4), 127–140 (2003)CrossRef

30.

Tounsi, I., Hadj Kacem, M., Hadj Kacem, A.: Building correct by construction SOA design patterns: modeling and refinement. In: Drira, K. (ed.) ECSA 2013. LNCS, vol. 7957, pp. 33–44. Springer, Cham (2013). https://doi.org/10.1007/978-3-642-39031-9_4CrossRef

31.

Tounsi, I., Hadj Kacem, M., Hadj Kacem, A., Drira, K.: A refinement-based approach for building valid SOA design patterns. Int. J. Cloud Comput. 4(1), 78–104 (2015)CrossRef

32.

Tounsi, I., Saidi, A., Hadj Kacem, M., Hadj Kacem, A.: Internet of Things design patterns modeling proven correct by construction: application to aged care solution. Future Gener. Comput. Syst. 148, 395–407 (2023)CrossRef

33.

Vergara, S., González, L., Ruggia, R.: Towards formalizing microservices architectural patterns with Event-B. In: 2020 IEEE International Conference on Software Architecture Companion (ICSA-C), pp. 71–74 (2020)

34.

Vergara, S., González, L., Ruggia, R.: Complementary material (2023). https://www.fing.edu.uy/owncloud/index.php/s/9Vs9rDde1wYpQxt

Titel: Formalizing Microservices Patterns with Event-B: The Case of Service Registry
verfasst von: Sebastián Vergara
Laura González
Raúl Ruggia
Verlag: Springer Nature Singapore
Buch: Service-Oriented Computing – ICSOC 2023 Workshops
Print ISBN: 978-981-9709-88-5

Electronic ISBN: 978-981-9709-89-2

Copyright-Jahr: 2024
DOI: https://doi.org/10.1007/978-981-97-0989-2_20

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner