A generic algorithm for universal TDM communication over inter-satellite links: Foundations, verification, and practice

The emergence of new swarm architectures and next-generation distributed algorithms utilizing them presents a substantial challenge for ensuring correctness, robustness, and scalability. The Python Testbed for Federated Learning Algorithms (PTB-FLA), developed within the TaRDIS project, is a lightweight framework offering generic algorithms for federated learning and pairwise TDM communication. Although PTB-FLA was originally conceived for federated learning algorithms development, it has since evolved to accommodate decentralized swarm systems that require trustworthy, formally verified communication mechanisms. This paper presents a unified and extended study of the generic algorithm for universal TDM communication, within PTB-FLA. The algorithm generalizes pairwise exchanges into synchronous multi-peer communication within a single timeslot, enabling flexible, topology-independent simulation of decentralized swarm systems such as satellite constellations. This work outlines the algorithm’s foundations, implementation, CSP formal modeling, and extends verification from a static clique worst-case scenario to dynamic configurations, featuring link failures, recoveries, and evolving inter-satellite link topologies. Verification results demonstrate both safety and liveness over many rounds, establishing the algorithm as a trustworthy and robust communication primitive. A case study of the algorithm’s usage within the TaRDIS satellite swarm use case highlights its practical impact, showing how the algorithm can be utilized within a simulation of a large, dynamically reconfiguring constellation. This capability is essential for development of novel orbit determination and time synchronization algorithms that are the main goal of the use case, reinforcing PTB-FLA’s growing role as a framework for the development of trustworthy, correct-by-construction systems.