Towards Formal Verification of Federated Learning Orchestration Protocols on Satellites

Python Testbed for Federated Learning Algorithms (PTB-FLA) is a simple FL framework targeting edge systems that implements both centralized and decentralized FL orchestration protocols, which were formally verified in a previous paper 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.