| Title |
Cloud-based Provisioning of Formal Verification Tools for Microservice Architectures |
| DOI |
https://doi.org/10.5573/ieie.2026.63.6.35 |
| Keywords |
Formal verification; Microservice architectures; Containerization; Coq; Cloud provisioning; CI/CD |
| Abstract |
As microservice architectures (MSA) become increasingly prevalent, ensuring service correctness and compositional integrity remains a key challenge. This paper presents vMSA, a containerized tool that integrates a Coq-based formal verification toolchain with an automated pipeline spanning verification to deployment. vMSA automates five stages - specification validation, formal verification, code generation, deployment, and benchmarking - while preventing configuration errors through verified configurations. Experiments on MSAs of up to seven services (up to 3,734 lines of Coq) show that containerization overhead is dominated by a fixed startup latency (approximately 680 ms on average) and that parallel verification achieves up to a 2.82× speedup. The full pipeline completes within 10 seconds locally and 23 seconds on a remote cluster for the seven-service MSA, demonstrating its practical suitability for CI/CD integration. |