L'Association for Computing Machinery (ACM, https://www.acm.org/) pubblica da oltre cinque decenni le linee guida per i programmi universitari di Informatica (Computer Science, CS). Poiché il campo dell'Informatica si evolve rapidamente, l'ACM rivede una volta ogni decennio le sue linee guida. L'ultima revisione, la CS2023, pubblicata di recente, contiene 17 aree di conoscenza fondamentali ritenute essenziali per l'Informatica, ciascuna delle quali è ulteriormente suddivisa in unità di conoscenza costituite da sotto-argomenti: alcuni obbligatori da insegnare e altri elettivi.
Il ruolo dei Metodi Formali nella Formazione in Informatica è evidenziato in un recente articolo che riassume le discussioni e le prove presentate in tre white paper, scritti complessivamente da 35 informatici e professionisti di tutto il mondo con una vasta esperienza nell'insegnamento dei Metodi Formali in ambito accademico o nell'industria. Questo ruolo chiave dei Metodi Formali deve necessariamente riflettersi nei curricula di Informatica come un'area di conoscenza fondamentale piuttosto che come argomenti elettivi in aree di conoscenza distinte. Ciò è confermato da un'ampia rassegna dell'uso crescente dei Metodi Formali nell'Industria, non limitata alle ben note storie di successo del settore safety-critical, ma che include casi d'uso nella produzione litografica e nella sicurezza del cloud nel commercio elettronico, nonché l'ampio uso nelle industrie in Europa, Asia, e Nord e Sud America. Sia l'articolo che la rassegna sono stati coordinati dal responsabile del laboratorio Formal Methods and Tools (FMT) dell'Istituto di Scienze e Tecnologie dell'Informazione (ISTI) del CNR, e sono stati pubblicati nelle principali riviste di Informatica dell'ACM. I Metodi Formali sono linguaggi e tecniche (e strumenti software) basati su rigorosi fondamenti matematici per la specifica, lo sviluppo, l'analisi e la verifica (manuale o automatizzata) di sistemi software e hardware. FMT è un gruppo di ricerca di fama internazionale nel settore, con decenni di esperienza nello sviluppo e nell'applicazione di Metodi Formali e strumenti, in particolare nell'industria ferroviaria.
L'articolo sostiene dunque la necessità di introdurre i Metodi Formali come area di conoscenza fondamentale distinta nelle linee guida ACM/IEEE/AAAI per i curricula in Informatica (https://csed.acm.org/), laddove attualmente i Metodi Formali sono inseriti solo come argomenti elettivi in alcune unità di conoscenza all'interno delle aree di conoscenza Foundations of Programming Languages e Software Engineering. Le prove presentate suggeriscono che la mancata indicazione dei Metodi Formali come area di conoscenza centrale nelle linee guida CS2023 è ingiustificata, probabilmente similmente al fatto che solo 10 anni fa l'Intelligenza Artificiale non fosse inclusa nelle linee guida CS2013. Nello specifico, viene sottolineata l'importanza della riflessione sui Metodi Formali nella Formazione Informatica, in quanto essa fornisce il rigore necessario per ragionare sul software, sulle sue specifiche, sulla sua verifica, e sulla sua correttezza: tutte competenze fondamentali per i futuri sviluppatori di software. Viene poi sottolineata l'importanza della conoscenza dei Metodi Formali per tutti gli informatici, poiché le competenze e le conoscenze acquisite in questo modo forniscono l'indispensabile base solida che costituisce l'ossatura della pratica dell'Informatica. Infine, viene sottolineata che l'insegnamento dei Metodi Formali non deve necessariamente avvenire in luogo di altri aspetti ingegneristici dell'Informatica che sono già ampiamente accettati come essenziali. Al contrario, viene evidenziata come i Metodi Formali abbiano il potenziale per sostenere e rafforzare la presentazione e la conoscenza in 8 delle 17 aree di conoscenza di CS2023; oltre alle aree di conoscenza sopra citate, si tratta di Algorithmic Foundations, Architecture and Organization, Artificial Intelligence, Parallel and Distributed Computing, Security, e Software Development Fundamentals. L'articolo fornisce suggerimenti concreti per gli educatori su come incorporare i Metodi Formali nella Formazione Informatica, ad esempio attraverso Formal Methods Europe (FME, https://fmeurope.org/) e il suo Teaching Committee's Education Course Database (https://fme-teaching.github.io/courses/).
References:
M. ter Beek, M. Broy, and B. Dongol, The Role of Formal Methods in Computer Science Education. ACM Inroads 15, 4 (2024), 58-66. DOI: https://doi.org/10.1145/3702231
M.H. ter Beek, R. Chapman, R. Cleaveland, H. Garavel, R. Gu, I. ter Horst, J.J.A. Keiren, T. Lecomte, M. Leuschel, K.Y. Rozier, A. Sampaio, C. Seceleanu, M. Thomas, T.A.C. Willemse, and L. Zhang, Formal Methods in Industry. Formal Aspects of Computing: Applicable Formal Methods (2024). DOI: https://doi.org/10.1145/3689374
Focus