Event-B Based Approach for Verifying Dynamic Composite Service Transactional Behavior

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.