An Event-B Capability-Centric Model for Cloud Service Discovery

Cloud computing has become increasingly adopted due to its ability to provide on-demand access to computing resources. However, the proliferation of cloud service offerings has introduced significant challenges in service discovery. Existing cloud service discovery approaches are often evaluated solely through simulation or experimentation and typically rely on unstructured service descriptions, which limits their precision and scalability. In this work, we address these limitations by proposing a formally verified architecture for capability-centric cloud service discovery, grounded in the Event-B method. The architecture is built upon a capability-centric service description model that captures service semantics through property-value representations. A core element of this model is the formally verified variantOf relation, which defines specialization among services. We prove that variantOf satisfies the properties of a partial order, enabling services to be structured as a Directed Acyclic Graph (DAG) and thus supporting hierarchical and scalable discovery. We formally verify the consistency of our model across multiple refinement levels. All proof obligations generated by the Rodin platform were successfully discharged. A scenario-based validation further confirms the correctness of dynamic operations within the system.