Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2015 | OriginalPaper | Buchkapitel

Formal Modelling and Verification of Transactional Web Service Composition: A Refinement and Proof Approach with Event-B

verfasst von : Idir Ait-Sadoune, Yamine Ait-Ameur

Erschienen in: Correct Software in Web Applications and Web Services

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Several languages for describing Web service compositions, like BPEL (Business Process Execution Language), make use of fault and compensation constructs to handle internal and/or external runtime errors of the composed service. This situation particularly occurs for transactional services. However, the absence of a rigorous definition of these BPEL constructors makes it difficult to correctly define the transactional behaviour of a BPEL process. The definitions of such constructs are usually given by their informal descriptions available in the standards. Our contribution proposes an approach to formally define the semantics of these operators. Thus, this paper presents a new Event-B semantics for formal modelling of Web service compositions that covers the scope, the fault and the compensation handlers introduced by the BPEL language specification. It also proposes a methodology showing how we can use Event-B method to design transactional BPEL processes. The proposed approach is illustrated by a case study.

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
Nächstes Kapitel Towards a Model of Services Based on Cocreation, Abstraction and Rights Distribution
Fußnoten
1
BPEL Designer Project: http://​eclipse.​org/​bpel/​
 
Literatur
1.
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)MATHCrossRef
2.
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRef
3.
Abrial, J.R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundam. Inform. 77, 1–28 (2007)MATHMathSciNet
4.
Ait-Ameur, Y., Baron, M., Kamel, N., Mota, J.M.: Encoding a process algebra using the Event B method. Int. J. Softw. Tools Technol. Transfer 11(3), 239–253 (2009)CrossRef
5.
Ait-Sadoune, I., Ait-Ameur, Y.: A proof based approach for modelling and verifying web services compositions. In: 14th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 1–10. IEEE Computer Society, Potsdam (2009)
6.
Ait-Sadoune, I., Ait-Ameur, Y.: Stepwise design of BPEL web services compositions, an Event B refinement based approach. In: 8th ACIS International Conference on Software Engineering Research, Management and Applications (SERA), pp. 51–68, Montreal (2010)
7.
Borger, E., Thalheim, B.: Modeling workflows, interaction patterns, web services and business processes: the ASM-based approach. In: Abstract State Machines, B and Z (ABZ 2008). Lecture Notes in Computer Science, vol. 5238. Springer, Heidelberg (2008)
8.
Butler, M., Ferreira, C., Ng, M.Y.: Precise modelling of compensating business transactions and its application to BPEL. J. Univers. Comput. Sci. 11(5), 712–743 (2005)
9.
Dijkstra, E.W.: A Discipline of Programming, 1st edn. Prentice Hall PTR, Upper Saddle River (1977)
10.
Fahland, D., Reisig, W.: ASM-based semantics for BPEL: the negative Control Flow. In: 12th International Workshop on Abstract State Machines, pp. 131–151 (2005)
11.
Farahbod, R., Glasser, U., Vajihollahi, M.: An abstract machine architecture for web service based business process management. In: Business Process Management Workshops. Lecture Notes in Computer Science, vol. 3812, pp. 144–157. Springer, Heidelberg (2005)
12.
Foster, H., Uchitel, S., Magee, J., Kramer, J.: Model-based verification of web service compositions. In: 18th IEEE International Conference on Automated Software Engineering (ASE’03), pp. 152–163 (2003)
13.
Guidi, C., Lucchi, R., Mazzara, M.: A formal framework for web services coordination. Electron. Notes Theor. Comput. Sci. 180, 55–70 (2007)CrossRef
14.
He, Y., Zhao, L., Wu, Z., Li, F.: Formal modeling of transaction behavior in WS-BPEL. In: International Conference on Computer Science and Software Engineering (CSSE 2008) (2008)
15.
Hinz, S., Schmidt, K., Stahl, C.: Transforming BPEL to petri nets. In: Springer-Verlag (ed.) 3rd International Conference on Business Process Management. Lecture Notes in Computer Science, vol. 2649. Springer, Heidelberg (2005)
16.
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580 (1969)MATHCrossRef
17.
Kovacs, M., Varro, D., Gonczy, L.: Formal analysis of BPEL workflows with compensation by model checking. Int. J. Ccomput. Syst. Sci. Eng. 23(5), 35–49 (2008)
18.
Leuschel, M., Butler, M.: ProB: a model checker for B. In: Formal Methods, International Symposium of Formal Methods Europe (FME’03). Lecture Notes in Computer Science, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
19.
Lohmann, N.: A feature-complete petri net semantics for WS-BPEL 2.0. In: Web Services and Formal Methods International Workshop WSFM 2007 (2007)
20.
Marconi, A., Pistore, M.: Synthesis and composition of web services. In: Formal Methods for Web Services - 9th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Web Services. Lecture Notes in Computer Science, vol. 5569. Springer, Heidelberg (2009)
21.
Nakajima, S.: Model-checking behavioral specification of BPEL applications. Electron. Notes Theor. Comput. Sci. 151, 89–105 (2006)CrossRef
22.
23.
24.
25.
Salaun, G., Bordeaux, L., Schaerf, M.: Describing and reasoning on web services using process algebra. In: IEEE International Conference on Web Services (ICWS’04), pp. 43–51 (2004)
26.
ter Beek, M.H., Bucchiarone, A., Gnesi1, S.: Formal methods for service composition. Ann. Math. Comput. Teleinformatics 1(5), 1–14 (2007)
27.
van der Aalst, W.M., Mooil, A.J., Stahl, C., Wolf, K.: Service interaction: patterns, formalization, and analysis. In: Formal Methods for Web Services - 9th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Web Services. Lecture Notes in Computer Science, vol. 5569. Springer, Heidelberg (2009)
28.
29.
30.
31.
Metadaten
Titel
Formal Modelling and Verification of Transactional Web Service Composition: A Refinement and Proof Approach with Event-B
verfasst von
Idir Ait-Sadoune
Yamine Ait-Ameur
Copyright-Jahr
2015
Buch
Correct Software in Web Applications and Web Services

Print ISBN: 978-3-319-17111-1

Electronic ISBN: 978-3-319-17112-8

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-17112-8_1

Premium Partner

    Bildnachweise