This paper describes formal modeling and verification of generic algorithm for
universal Time Division Multiplexing (TDM) communication, one of the
orchestration algorithms used in PTB-FLA (Python TestBed for Federated Learning
Algorithms), a light-weight framework for developing distributed applications,
developed as a part of the TaRDIS (Trustworthy and Resilient Decentralized
Intelligence For Edge Systems) project. Modeling and verification is done using
UPPAAL model checker tool. When developing a distributed application, in early
development phases a user of PTB-FLA can abstract away low-level details of
message passing and some elements of orchestration, by choosing one of the
available orchestration algorithms, therefore being able to focus on the actual
distributed algorithm at the application level. The generic algorithm for
universal TDM communication models peer data exchange between the nodes within a
discrete time-slots, a frequent case in inter-satellite links. It is an
orchestration algorithm intended to be used in satellite-swarm applications,
such as distributed ODTS (Orbit Determination and Time Synchronization). Formal
modeling and formal verification contributes significantly to increased
reliability of orchestration layer, making development of a distributed
algorithm easier by narrowing down possible sources of errors to application
level. This paper gives overview of PTB-FLA framework, provides a description of
the orchestration algorithm, shows its formal model in UPPAAL, and verifies some
important algorithm properties, namely deadlock freedom (a safety property) and
successful termination (a liveness property). This paper represents a
continuation of one of the research lines related to PTB-FLA, which is formal
verification of the framework’s generic orchestration algorithms, and other
elements.