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通过证明该通用算法无死锁（安全性）与可成功终止（活性），自动验证了第三种算法的正确性。