Formal Verification of a Generic Algorithm for TDM Communication Over Inter Satellite Links

TL;DR

This paper formally verifies a generic Time Division Multiplexing (TDM) communication algorithm for inter-satellite links using CSP process algebra, ensuring its safety and liveness properties through model checking.

Contribution

It extends formal verification to a TDM communication algorithm in satellite networks, demonstrating deadlock freedom and termination using the CSP and PAT tools.

Findings

The TDM algorithm is deadlock-free.

The algorithm guarantees successful termination.

Formal verification confirms safety and liveness properties.

Abstract

The Python Testbed for Federated Learning Algorithms is a simple FL framework targeting edge systems, which provides the three generic algorithms: the centralized federated learning, the decentralized federated learning, and the universal TDM communication in the current time slot. The first two were formally verified in a previous paper using the CSP process algebra, and in this paper, we use the same approach to formally verify the third one, in two phases. In the first phase, we construct the CSP model as a faithful representation of the real Python code. In the second phase, the model checker PAT automatically proves correctness of the third generic algorithm by proving its deadlock freeness (safety property) and successful termination (liveness property).