Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917111959388160 |
|---|---|
| author | Wojtak, Connor Gajewski, Darek Cerny, Tomas |
| author_facet | Wojtak, Connor Gajewski, Darek Cerny, Tomas |
| contents | Microservice systems are becoming increasingly adopted due to their scalability, decentralized development, and support for continuous integration and delivery (CI/CD). However, this decentralized development by separate teams and continuous evolution can introduce miscommunication and incompatible implementations, undermining system maintainability and reliability across aspects from security policy to system architecture. We propose a novel methodology that statically reconstructs microservice source code into a formal system model. From this model, a Satisfiability Modulo Theories (SMT) constraint set can be derived, enabling formal verification. Our methodology is extensible, supporting software verification across multiple cross-cutting concerns. We focus on applying the methodology to verify the system architecture concern, presenting formal reasoning to validate the methodology's correctness and applicability for this concern. Additional concerns such as security policy implementation are considered. Future directions are established to extend and evaluate the methodology. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_02860 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems Wojtak, Connor Gajewski, Darek Cerny, Tomas Software Engineering Logic in Computer Science Microservice systems are becoming increasingly adopted due to their scalability, decentralized development, and support for continuous integration and delivery (CI/CD). However, this decentralized development by separate teams and continuous evolution can introduce miscommunication and incompatible implementations, undermining system maintainability and reliability across aspects from security policy to system architecture. We propose a novel methodology that statically reconstructs microservice source code into a formal system model. From this model, a Satisfiability Modulo Theories (SMT) constraint set can be derived, enabling formal verification. Our methodology is extensible, supporting software verification across multiple cross-cutting concerns. We focus on applying the methodology to verify the system architecture concern, presenting formal reasoning to validate the methodology's correctness and applicability for this concern. Additional concerns such as security policy implementation are considered. Future directions are established to extend and evaluate the methodology. |
| title | Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems |
| topic | Software Engineering Logic in Computer Science |
| url | https://arxiv.org/abs/2509.02860 |