A Correct-by-Construction Model for Verifying Cloud Deployment Requirements of FOSS Applications

Abstract

This repository contains the complete Event-B formal specifications, contexts, proof obligation records, and ProB animation scripts for the CDM4FOSS framework (Correct Deployment Model for FOSS-based Applications). CDM4FOSS provides a correct-by-construction approach to model, verify, and validate multi-layered cloud deployment constraints for Free and Open Source Software (FOSS) applications at design time. Repository Contents The repository includes the complete Rodin project archive containing: Event-B Contexts (DC_c0 to DC_c3): Define static sets, constants, and axioms for infrastructure resources, port interfaces, topological constraints, and Semantic Versioning (SemVer 2.0.0). Event-B Machines (DM_m0 to DM_m3): Implement the four-level refinement chain enforcing lifecycle states, dependency bindings, spatial constraints (collocation, incompatibility, exclusivity), and version upgrades/downgrades. Animation & Case Study Models (DM_m4, WordPress_c0, WordPress_c1, WordPress_c2): Concrete animation contexts for validating realistic deployment scenarios (WordPress, MySQL, Apache2, Nginx, Varnish, Load Balancers) using ProB. Refinement Chain Overview Level 1 (DC_c0, DM_m0): General deployment constraints, VM hosting restrictions, capacity thresholds, and baseline FOSS lifecycle events (deploy, install, run, stop, uninstall). Level 2 (DC_c1, DM_m1): Functional dependencies and port bindings (instBinding, runBinding). Level 3 (DC_c2, DM_m2): Composition deployment constraints using relational algebra (CDC1: Incompatibility, CDC2: VM Exclusivity, CDC3: Collocation, CDC4: Full Deployment, CDC5: Mutual Exclusion). Level 4 (DC_c3, DM_m3): Release conflict constraints (RCC1: Version compatibility via SemVer lexicographical comparison, RCC2/RCC3: Release upgrade/downgrade rules). Formal Verification & Proof Statistics Total Proof Obligations (POs): 136 POs generated within the Rodin platform. Automatic Proofs: 109 POs (80.1%) discharged automatically using Atelier B provers and SMT solvers (CVC4, veriT). Interactive Proofs: 27 POs (19.9%) discharged interactively. Software Requirements Rodin Platform (v3.x or higher). Rodin Plugins: ProB Model Checker / Animator, SMT Solvers, Atelier B Provers.