Event-B based approach for verifying dynamic composite service transactional behavior

  • Mohamed Graiet
  • , Imed Abbassi
  • , Lazhar Hamel
  • , Mohamed Tahar Bhiri
  • , Mourad Kmimech
  • , Walid Gaaloul

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Verifying Web service composition in a dynamic environment remains one of the most difficult tasks despite the efforts and the previous proposed research works because new services can be composed during the execution step and others can automatically appear, disappear, or be updated. To achieve the Web service composition specification and verification, we introduce a new concept, called dynamic pattern. A dynamic pattern is an extension of a static one. Then, we propose to formalize dynamic Web Service composition in Event-B using dynamic patterns. The resulting model is progressively verified using proofs. We use animator of model (ProB) to detect a variety of problems, such as deadlocks or other unexpected behavior of a model.

Original languageEnglish
Title of host publicationProceedings - IEEE 20th International Conference on Web Services, ICWS 2013
PublisherIEEE Computer Society
Pages251-259
Number of pages9
ISBN (Print)9780768550251
DOIs
Publication statusPublished - 1 Jan 2013
Event2013 IEEE 20th International Conference on Web Services, ICWS 2013 - Santa Clara, CA, United States
Duration: 27 Jun 20132 Jul 2013

Publication series

NameProceedings - IEEE 20th International Conference on Web Services, ICWS 2013

Conference

Conference2013 IEEE 20th International Conference on Web Services, ICWS 2013
Country/TerritoryUnited States
CitySanta Clara, CA
Period27/06/132/07/13

Keywords

  • ProB
  • Web services
  • dynamic Web service composition
  • event-B
  • formal verification
  • proof
  • transaction

Fingerprint

Dive into the research topics of 'Event-B based approach for verifying dynamic composite service transactional behavior'. Together they form a unique fingerprint.

Cite this