Formalising Cloud Service Semantics for Automated Compatibility Analysis
Verifying Compatibility of Message Queues and Key-Value Stores
B.V. van Vliet (TU Delft - Electrical Engineering, Mathematics and Computer Science)
A. Katsifodimos – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Reinier Goeman – Mentor (Sue B.V.)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
While cloud-native architectures promise massive scalability and decoupling, their reliance on managed distributed services introduces a hidden risk: vendor lock-in. Even services with similar functionality and identical APIs may differ in fundamental guarantees such as delivery, ordering, and consistency. These differences could lead to subtle, unpredictable errors during migration. Current infrastructure-as-code tools like Terraform focus on provisioning and fail to capture these underlying behavioural constraints.
To bridge this semantic gap, this thesis introduces a formal framework leveraging the Quint specification language to automate cloud service compatibility analysis. By representing distributed systems as rigorous compositions of partially ordered guarantees, this framework generates specific correctness invariants to verify compatibility between systems, defined in terms of invariant preservation across migrations. The approach is empirically validated through trace-based execution against a concrete Redis instance.
Our compatibility experiments reveal an asymmetry in cloud migrations: while key-value stores exhibit high interoperability (primarily bottlenecked by strict causality), message queue compatibility is highly fragmented by conflicting delivery (at_most_once) and ordering (fifo_ordering) invariants. Furthermore, we demonstrate an application of this framework by feeding these formal, invariant-based violations back into Large Language Models (LLMs) as structured guidance. Experimental results show this formal feedback drastically constrains the generative search space, reducing the median iterations required to synthesise a correct distributed system by approximately 58%.
Ultimately, this research provides a machine-checkable foundation to safely navigate cloud migrations, moving beyond ad-hoc testing to enable the verifiable design of genuinely cloud-agnostic architectures.