Correct orchestration of federated learning generic algorithms: Python translation to CSP and verification by PAT

Abstract

Federated learning (FL) is a machine learning setting where clients keep the training data decentralized and collaboratively train a model either under the coordination of a central server (centralized FL) or in a peer-to-peer network (decentralized FL). Correct orchestration is one of the main challenges. In this paper, we formally verify the correctness of two generic FL algorithms, a centralized and a decentralized one, using the Communicating Sequential Processes (CSP) calculus and the Process Analysis Toolkit (PAT) model checker. The CSP models consist of CSP processes corresponding to generic FL algorithm instances. PAT automatically proves the correctness of the two generic FL algorithms by proving their deadlock freedom (safety property) and successful termination (reachability and liveness property). The CSP models are constructed as a faithful representation of the real Python code and are expressed directly in CSP# language that PAT uses. Then they are automatically checked top-down by PAT. The Python code follows a restricted actor-based programming model, and the construction of CSP# code from such Python code is performed systematically. The process is described in detail, ensuring that the models correspond to the actual code. It represents a basis for developing tools for automatic translation of certain classes of Python code to CSP models, expressed in CSP#.