Towards Formal Verification of Federated Learning Orchestration Protocols on Satellites
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910793770991616 |
|---|---|
| author | Popovic, Miroslav Popovic, Marko Djukic, Miodrag Basicevic, Ilija |
| author_facet | Popovic, Miroslav Popovic, Marko Djukic, Miodrag Basicevic, Ilija |
| contents | Python Testbed for Federated Learning Algorithms (PTB-FLA) is a simple FL framework targeting smart Internet of Things in edge systems that provides both generic centralized and decentralized FL algorithms, which implement the corresponding FL orchestration protocols that were formally verified using the process algebra CSP. This approach is appropriate for systems with stationary nodes but cannot be applied to systems with moving nodes. In this paper, we use celestial mechanics to model spacecraft movement, and timed automata (TA) to formalize and verify the centralized FL orchestration protocol, in two phases. In the first phase, we created a conventional TA model to prove traditional properties, namely deadlock freeness and termination. In the second phase, we created a stochastic TA model to prove timing correctness and to estimate termination probability. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_13429 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Towards Formal Verification of Federated Learning Orchestration Protocols on Satellites Popovic, Miroslav Popovic, Marko Djukic, Miodrag Basicevic, Ilija Distributed, Parallel, and Cluster Computing Python Testbed for Federated Learning Algorithms (PTB-FLA) is a simple FL framework targeting smart Internet of Things in edge systems that provides both generic centralized and decentralized FL algorithms, which implement the corresponding FL orchestration protocols that were formally verified using the process algebra CSP. This approach is appropriate for systems with stationary nodes but cannot be applied to systems with moving nodes. In this paper, we use celestial mechanics to model spacecraft movement, and timed automata (TA) to formalize and verify the centralized FL orchestration protocol, in two phases. In the first phase, we created a conventional TA model to prove traditional properties, namely deadlock freeness and termination. In the second phase, we created a stochastic TA model to prove timing correctness and to estimate termination probability. |
| title | Towards Formal Verification of Federated Learning Orchestration Protocols on Satellites |
| topic | Distributed, Parallel, and Cluster Computing |
| url | https://arxiv.org/abs/2410.13429 |