Skip to main content

2016 | OriginalPaper | Buchkapitel

Correct-by-Construction Evolution of Realisable Conversation Protocols

verfasst von : Sarah Benyagoub, Meriem Ouederni, Neeraj Kumar Singh, Yamine Ait-Ameur

Erschienen in: Model and Data Engineering

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

Distributed software systems are often built by composing independent and autonomous peers with cross-organisational interaction and no centralised control. These peers can be administrated and executed by geographically distributed and autonomous companies. In a top-down design of distributed software systems, the peers’ interaction is often described by a global specification called Conversation Protocol (CP) and one have to check its realisability i.e., whether there exists a set of peers implementing this CP. In dynamic environments, CP needs to be updated wrt. new environment changes and end-user interaction requirements. This paper tackles CP evolution such that its realisability must be preserved. We define some evolution patterns and prove that they ensure the realisability. We also show how our proposal can be supported by existing methods and tools based on refinement and theorem proving, using the event-B langage and RODIN development tools.

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!

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!

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!

Literatur
1.
Zurück zum Zitat Bultan, T.: Modeling interactions of web software. In: Proceedings of WWV 2006, pp. 45–52. IEEE(2006) Bultan, T.: Modeling interactions of web software. In: Proceedings of WWV 2006, pp. 45–52. IEEE(2006)
2.
Zurück zum Zitat Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: Proceedings of POPL 2012, pp. 191–202. ACM (2012) Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: Proceedings of POPL 2012, pp. 191–202. ACM (2012)
3.
Zurück zum Zitat Rinderle, S., Wombacher, A., Reichert, M.: On the controlled evolution of process choreographies. In: Proceedings of ICDE 2006, pp. 124–124. IEEE (2006) Rinderle, S., Wombacher, A., Reichert, M.: On the controlled evolution of process choreographies. In: Proceedings of ICDE 2006, pp. 124–124. IEEE (2006)
4.
Zurück zum Zitat Ryu, S.H., Casati, F., Skogsrud, H., Benatallah, B., Saint-Paul, R.: Supporting the dynamic evolution of web service protocols in service-oriented architectures. ACM Trans. Web (TWEB) 2(2), 13 (2008) Ryu, S.H., Casati, F., Skogsrud, H., Benatallah, B., Saint-Paul, R.: Supporting the dynamic evolution of web service protocols in service-oriented architectures. ACM Trans. Web (TWEB) 2(2), 13 (2008)
5.
Zurück zum Zitat Roohi, N., Salaün, G.: Realizability and dynamic reconfiguration of chor specifications. Informatica (Slovenia) 35(1), 39–49 (2011)MATH Roohi, N., Salaün, G.: Realizability and dynamic reconfiguration of chor specifications. Informatica (Slovenia) 35(1), 39–49 (2011)MATH
6.
Zurück zum Zitat Güdemann, M., Salaün, G., Ouederni, M.: Counterexample guided synthesis of monitors for realizability enforcement. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 238–253. Springer, Heidelberg (2012)CrossRef Güdemann, M., Salaün, G., Ouederni, M.: Counterexample guided synthesis of monitors for realizability enforcement. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 238–253. Springer, Heidelberg (2012)CrossRef
8.
Zurück zum Zitat Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory. Languages and Computation. Addison Wesley, Reading (1979)MATH Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory. Languages and Computation. Addison Wesley, Reading (1979)MATH
9.
Zurück zum Zitat Farah, Z., Ait-Ameur, Y., Ouederni, M., Tari, K.: A correct-by-construction model for asynchronously communicating systems. Int. J. Softw. Tools Technol. Transfer 1–21 (2016) Farah, Z., Ait-Ameur, Y., Ouederni, M., Tari, K.: A correct-by-construction model for asynchronously communicating systems. Int. J. Softw. Tools Technol. Transfer 1–21 (2016)
10.
Zurück zum Zitat Ben-Abdallah, H., Leue, S.: Syntactic detection of process divergence and non-local choice in message sequence charts. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 259–274. Springer, Heidelberg (1997) Ben-Abdallah, H., Leue, S.: Syntactic detection of process divergence and non-local choice in message sequence charts. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 259–274. Springer, Heidelberg (1997)
11.
Zurück zum Zitat Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)CrossRefMATH Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)CrossRefMATH
13.
Zurück zum Zitat Medvidovic, N.: ADLs and dynamic Architecture Changes. In: Proceedings of SIGSOFT 1996 Workshops, pp. 24–27. ACM (1996) Medvidovic, N.: ADLs and dynamic Architecture Changes. In: Proceedings of SIGSOFT 1996 Workshops, pp. 24–27. ACM (1996)
14.
Zurück zum Zitat Leite, L.A., Oliva, G.A., Nogueira, G.M., Gerosa, M.A., Kon, F., Milojicic, D.S.: A Systematic Literature Review of Service Choreography Adaptation. SOCA 7(3), 199–216 (2013)CrossRef Leite, L.A., Oliva, G.A., Nogueira, G.M., Gerosa, M.A., Kon, F., Milojicic, D.S.: A Systematic Literature Review of Service Choreography Adaptation. SOCA 7(3), 199–216 (2013)CrossRef
15.
Zurück zum Zitat Wombacher, A.: Alignment of choreography changes in BPEL processes. In: Proceedings of SCC 2009. pp. 1–8. IEEE (2009) Wombacher, A.: Alignment of choreography changes in BPEL processes. In: Proceedings of SCC 2009. pp. 1–8. IEEE (2009)
16.
Zurück zum Zitat Rinderle, S., Wombacher, A., Reichert, M.: Evolution of process choreographies in DYCHOR. In: Meersman, R., Tari, Z. (eds.) OTM 2006. LNCS, vol. 4275, pp. 273–290. Springer, Heidelberg (2006)CrossRef Rinderle, S., Wombacher, A., Reichert, M.: Evolution of process choreographies in DYCHOR. In: Meersman, R., Tari, Z. (eds.) OTM 2006. LNCS, vol. 4275, pp. 273–290. Springer, Heidelberg (2006)CrossRef
17.
Zurück zum Zitat Dalla Preda, M., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J.: Dynamic choreographies. In: Holvoet, T., Viroli, M. (eds.) Coordination Models and Languages. LNCS, vol. 9037, pp. 67–82. Springer, Heidelberg (2015) Dalla Preda, M., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J.: Dynamic choreographies. In: Holvoet, T., Viroli, M. (eds.) Coordination Models and Languages. LNCS, vol. 9037, pp. 67–82. Springer, Heidelberg (2015)
18.
Zurück zum Zitat Fdhila, W., Indiono, C., Rinderle-Ma, S., Reichert, M.: Dealing with change in process choreographies: design and implementation of propagation algorithms. Inf. Syst. 49, 1–24 (2015)CrossRef Fdhila, W., Indiono, C., Rinderle-Ma, S., Reichert, M.: Dealing with change in process choreographies: design and implementation of propagation algorithms. Inf. Syst. 49, 1–24 (2015)CrossRef
19.
Zurück zum Zitat Jureta, I.J., Faulkner, S., Thiran, P.: Dynamic requirements specification for adaptable and open service-oriented systems. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 270–282. Springer, Heidelberg (2007)CrossRef Jureta, I.J., Faulkner, S., Thiran, P.: Dynamic requirements specification for adaptable and open service-oriented systems. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 270–282. Springer, Heidelberg (2007)CrossRef
20.
Zurück zum Zitat Börger, E., Schewe, K.D.: Concurrent abstract state machines. Acta Informatica 1–24 (2015) Börger, E., Schewe, K.D.: Concurrent abstract state machines. Acta Informatica 1–24 (2015)
Metadaten
Titel
Correct-by-Construction Evolution of Realisable Conversation Protocols
verfasst von
Sarah Benyagoub
Meriem Ouederni
Neeraj Kumar Singh
Yamine Ait-Ameur
Copyright-Jahr
2016
DOI
https://doi.org/10.1007/978-3-319-45547-1_21

Premium Partner