Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2509.11566 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866912586400792576 |
|---|---|
| author | Guo, Hua Ji, Yunhong Zhou, Xuan |
| author_facet | Guo, Hua Ji, Yunhong Zhou, Xuan |
| contents | Developing distributed systems presents significant challenges, primarily due to the complexity introduced by non-deterministic concurrency and faults. To address these, we propose a specification-driven development framework. Our method encompasses three key stages. The first stage defines system specifications and invariants using TLA${^+}$. It allows us to perform model checking on the algorithm's correctness and generate test cases for subsequent development phases. In the second stage, based on the established specifications, we write code to ensure consistency and accuracy in the implementation. Finally, after completing the coding process, we rigorously test the system using the test cases generated in the initial stage. This process ensures system quality by maintaining a strong connection between the abstract design and the concrete implementation through continuous verification. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_11566 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Sedeve-Kit, a Specification-Driven Development Framework for Building Distributed Systems Guo, Hua Ji, Yunhong Zhou, Xuan Software Engineering Developing distributed systems presents significant challenges, primarily due to the complexity introduced by non-deterministic concurrency and faults. To address these, we propose a specification-driven development framework. Our method encompasses three key stages. The first stage defines system specifications and invariants using TLA${^+}$. It allows us to perform model checking on the algorithm's correctness and generate test cases for subsequent development phases. In the second stage, based on the established specifications, we write code to ensure consistency and accuracy in the implementation. Finally, after completing the coding process, we rigorously test the system using the test cases generated in the initial stage. This process ensures system quality by maintaining a strong connection between the abstract design and the concrete implementation through continuous verification. |
| title | Sedeve-Kit, a Specification-Driven Development Framework for Building Distributed Systems |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2509.11566 |