Formal Verification of Cloud Resource Allocation in Business Processes Using Event-B

Abstract

Nowadays, a growing number of companies are using Cloud Computing to optimize their business processes by using dynamically scalable and often virtualized resources on demand. Nevertheless, due to the lack of explicit and formal description of the resource perspective in existing business processes, Cloud resource allocation behavior cannot be efficiently and correctly managed. In this paper, we aim at formally verifying resource allocation in business processes using Event-B. More precisely, our aim is to specify the resource allocation behavior both at design time and at runtime, and to check its correctness according to users' needs. Our model also takes into account different cloud properties such as elasticity and shareability. In order to show its feasibility, our approach has been tested using a use case study from an industrial partner.

Cite this work

No public copy is stored for this record, so only the metadata is cited.

Stored only when both papers are in the corpus — 12 citations exist upstream.

Papers that cite the same references — the relational fallback while embeddings are still backfilling.