Skip to main content
Top

2024 | OriginalPaper | Chapter

Correct Orchestration of Federated Learning Generic Algorithms: Formalisation and Verification in CSP

Authors : Ivan Prokić, Silvia Ghilezan, Simona Kašterović, Miroslav Popovic, Marko Popovic, Ivan Kaštelan

Published in: Engineering of Computer-Based Systems

Publisher: Springer Nature Switzerland

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
4.
go back to reference 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., 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
6.
go back to reference 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 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
7.
go back to reference Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985) Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
8.
go back to reference 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 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
9.
go back to reference Kholod, I., et al.: Open-source federated learning frameworks for IoT: A comparative review and analysis. Sensors 21(1), 167 (2021)CrossRef Kholod, I., et al.: Open-source federated learning frameworks for IoT: A comparative review and analysis. Sensors 21(1), 167 (2021)CrossRef
11.
go back to reference 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 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
13.
go back to reference 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 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
14.
go back to reference Mittone, G., et al.: Experimenting with emerging RISC-V systems for decentralised machine learning (2023) Mittone, G., et al.: Experimenting with emerging RISC-V systems for decentralised machine learning (2023)
24.
go back to reference 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., Chen, Y., Hu, H., Pan, P., Yin, W.: Exponential graph is provably efficient for decentralized deep training (2021)
26.
go back to reference 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 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
Metadata
Title
Correct Orchestration of Federated Learning Generic Algorithms: Formalisation and Verification in CSP
Authors
Ivan Prokić
Silvia Ghilezan
Simona Kašterović
Miroslav Popovic
Marko Popovic
Ivan Kaštelan
Copyright Year
2024
DOI
https://doi.org/10.1007/978-3-031-49252-5_25

Premium Partner