Web Service Compensation at Runtime: Formal Modeling and Verification Using the Event-B Refinement and Proof Based Formal Method

摘要

One of the key interests in web services is the ability to compose them in order to build more powerful and complex ones running in an interoperable and distributed setting. Several languages, like BPEL, that describe such services have been proposed. Similar to the usual complex systems, web service compositions may exhibit inappropriate behaviors in the presence of failures. Compensation mechanisms are available to express running services recovery in case of failures. This paper addresses the problem of the correct design of web service compositions in case of failures. It presents a novel correct-by-construction formal approach based on refinement using the Event-B method. The proposed approach defines a compensation mechanism to repair failed services at runtime. It addresses not only behavioral aspects but also, functional ones through the introduction of repairing invariants whose persistence is enforced during compensation at runtime. Different compensation scenarios and modes are addressed. A formal model for equivalent, degraded and upgraded service compensations relying on the Event-B formalization is defined. The proposal is illustrated on a case study.