Abstract
Federated learning (FL) is a machine learning setting where clients keep the training data decentralised and collaboratively train a model either under the coordination of a central server (centralised FL) or in a peer-to-peer network (decentralised FL). Correct orchestration is one of the main challenges. In this paper, we formally verify the correctness of two generic FL algorithms, a centralised and a decentralised one, using the Communicating Sequential Processes calculus (CSP) 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 freeness (safety property) and successful termination (liveness property). The CSP models are constructed bottom-up by hand as a faithful representation of the real Python code and is automatically checked top-down by PAT.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
A world where every good question is answered. https://www.openmined.org. Accessed 15 Mar 2023
An industrial grade federated learning framework. https://fate.fedai.org/. Accessed 15 Mar 2023
An open-source deep learning platform originated from industrial practice. https://www.paddlepaddle.org.cn/en. Accessed 15 Mar 2023
Bonawitz, K.A., et al.: Practical secure aggregation for privacy-preserving machine learning. In: Thuraisingham, B., Evans, D., Malkin, T., Xu, D. (eds.) Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, 30 October–3 November 2017, pp. 1175–1191. ACM (2017). https://doi.org/10.1145/3133956.3133982
Bonawitz, K.A., Kairouz, P., McMahan, B., Ramage, D.: Federated learning and privacy. Commun. ACM 65(4), 90–97 (2022). https://doi.org/10.1145/3500240
Feraudo, A., et al.: CoLearn: Enabling federated learning in MUD-compliant IoT edge networks. In: Proceedings of the Third ACM International Workshop on Edge Systems, Analytics and Networking, pp. 25–30. EdgeSys 2020. Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3378679.3394528
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Hu, R., Yoshida, N.: Explicit connection actions in multiparty session types. In: Huisman, M., Rubin, J. (eds.) Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, 22–29 April 2017, Proceedings. LNCS, vol. 10202, pp. 116–133. Springer, Cham (2017). https://doi.org/10.1007/978-3-662-54494-5_7
Kholod, I., et al.: Open-source federated learning frameworks for IoT: A comparative review and analysis. Sensors 21(1), 167 (2021)
Konečný, J., McMahan, H.B., Yu, F.X., Richtárik, P., Suresh, A.T., Bacon, D.: Federated learning: Strategies for improving communication efficiency (2017). http://arxiv.org/abs/1610.05492
Kuhn, R., Melgratti, H.C., Tuosto, E.: Behavioural types for local-first software. In: Ali, K., Salvaneschi, G. (eds.) 37th European Conference on Object-Oriented Programming, ECOOP 2023, 17–21 July 2023, Seattle, Washington, United States. LIPIcs, vol. 263, pp. 15:1–15:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023). https://doi.org/10.4230/LIPIcs.ECOOP.2023.15
McMahan, B.: “Federated learning from research to practice”, a presentation hosted by Carnegie Mellon University seminar series. https://www.pdl.cmu.edu/SDI/2019/slides/2019-09-05Federated. Accessed 15 Mar 2023
McMahan, B., Moore, E., Ramage, D., Hampson, S., y Arcas, B.A.: Communication-efficient learning of deep networks from decentralized data. In: Singh, A., Zhu, X.J. (eds.) Proceedings of the 20th International Conference on Artificial Intelligence and Statistics, AISTATS 2017, 20–22 April 2017, Fort Lauderdale, FL, USA. Proceedings of Machine Learning Research, vol. 54, pp. 1273–1282. PMLR (2017). http://proceedings.mlr.press/v54/mcmahan17a.html
Mittone, G., et al.: Experimenting with emerging RISC-V systems for decentralised machine learning (2023)
Perino, D., Katevas, K., Lutu, A., Marin, E., Kourtellis, N.: Privacy-preserving AI for future networks. Commun. ACM 65(4), 52–53 (2022). https://doi.org/10.1145/3512343
Popovic, M., Popovic, M., Kastelan, I., Djukic, M., Ghilezan, S.: A simple Python testbed for federated learning algorithms. CoRR abs/2305.20027 (2023). https://doi.org/10.48550/ar**v.2305.20027
Popovic, M., Popovic, M., Kastelan, I., Djukic, M., Ghilezan, S.: A simple Python testbed for federated learning algorithms. In: 2023 Zooming Innovation in Consumer Technologies Conference (ZINC), pp. 148–153 (2023). https://doi.org/10.1109/ZINC58345.2023.10173859
Privacy-preserving artificial intelligence to advance humanity. https://sherpa.ai. Accessed 15 Mar 2023
Shen, C., Xue, W.: An experiment study on federated learning testbed. In: Zhang, Y.-D., Senjyu, T., So-In, C., Joshi, A. (eds.) Smart Trends in Computing and Communications. LNNS, vol. 286, pp. 209–217. Springer, Singapore (2022). https://doi.org/10.1007/978-981-16-4016-2_20
Simic, M., Prokic, I., Dedeic, J., Sladic, G., Milosavljevic, B.: Towards edge computing as a service: Dynamic formation of the micro data-centers. IEEE Access 9, 114468–114484 (2021). https://doi.org/10.1109/ACCESS.2021.3104475
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_59
TaRDIS: Trustworthy and resilient decentralised intelligence for edge systems. https://www.project-tardis.eu/
TensorFlow Federated: Machine learning on decentralized data. https://www.tensorflow.org/federated. Accessed 15 Mar 2023
Ying, B., Yuan, K., Chen, Y., Hu, H., Pan, P., Yin, W.: Exponential graph is provably efficient for decentralized deep training (2021)
Ying, B., Yuan, K., Hu, H., Chen, Y., Yin, W.: BlueFog: Make decentralized algorithms practical for optimization and deep learning. CoRR abs/2111.04287 (2021). https://arxiv.org/abs/2111.04287
Zhang, T., He, C., Ma, T., Gao, L., Ma, M., Avestimehr, S.: Federated learning for Internet of Things. In: Proceedings of the 19th ACM Conference on Embedded Networked Sensor Systems, SenSys 2021, pp. 413–419. Association for Computing Machinery, New York, NY, USA (2021). https://doi.org/10.1145/3485730.3493444
Acknowledgements
Funded by the European Union (TaRDIS, 101093006). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union. Neither the European Union nor the granting authority can be held responsible for them.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Prokić, I., Ghilezan, S., Kašterović, S., Popovic, M., Popovic, M., Kaštelan, I. (2024). Correct Orchestration of Federated Learning Generic Algorithms: Formalisation and Verification in CSP. In: Kofroň, J., Margaria, T., Seceleanu, C. (eds) Engineering of Computer-Based Systems. ECBS 2023. Lecture Notes in Computer Science, vol 14390. Springer, Cham. https://doi.org/10.1007/978-3-031-49252-5_25
Download citation
DOI: https://doi.org/10.1007/978-3-031-49252-5_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-49251-8
Online ISBN: 978-3-031-49252-5
eBook Packages: Computer ScienceComputer Science (R0)