Towards Formal Verification of Federated Learning Orchestration Protocols on Satellites
Miroslav V. Popovic, Marko Popović, Miodrag M. Djukic, Ilija V. Basicevic · 2024
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.