Towards Formal Verification of Federated Learning Orchestration Protocols on Satellites

TL;DR

This paper advances the formal verification of federated learning protocols on satellites by modeling spacecraft movement with celestial mechanics and using timed automata to verify protocol properties, addressing challenges of moving nodes.

Contribution

It introduces a novel approach combining celestial mechanics and timed automata for formal verification of FL protocols on moving satellite nodes, extending prior stationary node models.

Findings

Proved deadlock freeness and termination of the FL protocol.

Verified timing correctness and estimated termination probability.

Demonstrated applicability to satellite-based FL systems.

Abstract

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.