Compliance Verification of 5G Service Level Agreements using Event-B
Riham Badra, Lazhar Hamel, Layth Sliman, Ralp Bou Nader · 2025
Service Level Agreements (SLAs) play a critical role in modern service ecosystems, formalizing commitments between providers and customers to ensure compliance with performance metrics and Quality of Service (QoS) requirements. However, the lack of standardized, user-friendly tools for defining and customizing 5G SLAs in machine-readable formats, such as XML, hinders automation and interoperability in service management. To address this challenge, we propose a formal approach based on the Event-B method to model SLA contracts and ensure their correctness and reliability. We define an incremental Event-B model that captures SLA constraints and verify their consistency using proof obligations and animation. This ensures that SLA enforcement does not alter the expected execution semantics of contracts.