Formal Verification of a Generic Algorithm for TDM Communication Over Inter Satellite Links
Miroslav Popovic, Marko Popovic, Pavle Vasiljevic, Miodrag Djukic
Python Testbed for Federated Learning Algorithms是一个简单的针对边缘系统的FL框架,它提供了三种通用算法:集中式联合学习,分散式联合学习以及当前时间段的通用TDM通信。 前两个在上一篇论文中使用CSP过程代数进行了正式验证,本文中,我们使用相同的方法来正式验证第三个,分两个阶段。 在第一阶段,我们构建CSP模型作为真实Python代码的忠实表示。 在第二阶段,模型检查器PAT通过证明其死锁自由度(安全属性)和成功终止(活性属性)自动证明了第三个通用算法的正确性。
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...
