Formal Verification of a Generic Algorithm for TDM Communication Over Inter Satellite Links
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909990668730368 |
|---|---|
| author | Popovic, Miroslav Popovic, Marko Vasiljevic, Pavle Djukic, Miodrag |
| author_facet | Popovic, Miroslav Popovic, Marko Vasiljevic, Pavle Djukic, Miodrag |
| contents | The Python Testbed for Federated Learning Algorithms is a simple FL framework targeting edge systems, which provides the three generic algorithms: the centralized federated learning, the decentralized federated learning, and the universal TDM communication in the current time slot. The first two were formally verified in a previous paper using the CSP process algebra, and in this paper, we use the same approach to formally verify the third one, in two phases. In the first phase, we construct the CSP model as a faithful representation of the real Python code. In the second phase, the model checker PAT automatically proves correctness of the third generic algorithm by proving its deadlock freeness (safety property) and successful termination (liveness property). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_09485 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formal Verification of a Generic Algorithm for TDM Communication Over Inter Satellite Links Popovic, Miroslav Popovic, Marko Vasiljevic, Pavle Djukic, Miodrag Distributed, Parallel, and Cluster Computing The Python Testbed for Federated Learning Algorithms is a simple FL framework targeting edge systems, which provides the three generic algorithms: the centralized federated learning, the decentralized federated learning, and the universal TDM communication in the current time slot. The first two were formally verified in a previous paper using the CSP process algebra, and in this paper, we use the same approach to formally verify the third one, in two phases. In the first phase, we construct the CSP model as a faithful representation of the real Python code. In the second phase, the model checker PAT automatically proves correctness of the third generic algorithm by proving its deadlock freeness (safety property) and successful termination (liveness property). |
| title | Formal Verification of a Generic Algorithm for TDM Communication Over Inter Satellite Links |
| topic | Distributed, Parallel, and Cluster Computing |
| url | https://arxiv.org/abs/2511.09485 |