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).

翻译：Python联邦学习算法测试平台是一个面向边缘系统的简易FL框架，提供了三种通用算法：集中式联邦学习、分布式联邦学习以及当前时隙的通用TDM通信。前两种算法已在先前论文中通过CSP进程代数完成形式化验证。本文采用相同方法，分两个阶段对第三种算法进行形式化验证。第一阶段构建CSP模型，使其精确对应实际Python代码。第二阶段通过模型检测工具PAT自动验证第三种通用算法的正确性，具体证明其无死锁性（安全性）与成功终止性（活性）。