Deadlock-Freeness Verification of Cloud Composite Services Using Event-B

摘要

With the emergence of the Cloud computing paradigm, interests were focused on representing and verifying the Cloud architecture in a formal way in order to prevent eventual failures and deadlocks. Service composition promotes reuse, interoperability, and loosely coupled interaction. However, verifying the correctness of a composite service remains a tedious task. To ensure the correctness of a composition, critical properties such as deadlock freeness must be verified. In this paper, we propose a novel formal approach to verify Cloud composite services correctness based on the Event-B method. We consider that both behavioral incompatibilities and conflicted resource may lead the composite service execution to failure. Event-B provides rigorous mathematical reasoning that helps building trust on developed software. A verification and validation approach combining both model proofs and model checking is finally performed to check the soundness of the proposed model.