Bergamo – Dal 25 al 28 giugno 2024, presso la sede di Sant’Agostino, l’Università degli studi di Bergamo ospita la decima edizione della conferenza internazionale sui metodi formali: ABZ 2024 – 10th International Conference on Rigorous State Based Methods. Ricercatori di informatica provenienti da tutto il mondo si trovano per discutere l’uso dei metodi formali per la progettazione, lo sviluppo e la verifica di sistemi, sia software che hardware. Oggigiorno, è ampiamente riconosciuto che l’uso di metodi formali è utile per la realizzazione di sistemi ritenuti critici, come ad esempio software medici o software per veicoli a guida autonoma, cioè sistemi in cui un malfunzionamento può avere conseguenze assai disastrose con possibile perdita di vite umane. Come dimostrato in letteratura, l’uso di metodi formali avrebbe potuto evitare significativi danni in vari casi, come ad esempio le morti causate dal dispositivo medico per radioterapia Therac-25 tra il 1985 e il 1987, il fallimento del lancio del razzo Ariane 5 nel 1996, l’incidente mortale che ha coinvolto l’Airbus A400M nel 2015 in Spagna a causa di un difetto nel software di controllo del velivolo, o ancora il problema connesso allo spegnimento dei sistemi ibridi gas-elettrici dei veicoli Prius Toyota nel 2014 a causa di un errore di programmazione, per non dimenticare l’incidente mortale del 2016 che ha coinvolto una Tesla Model S con pilota automatico e che ha costretto la compagnia a richiamare oltre 54 mila automobili perché il software di guida autonoma consentiva di superare i segnali di stop. Questi sono solo alcuni esempi di cattiva progettazione e implementazione del software di controllo, che si sarebbero potuti evitare con l’impiego di processi di sviluppo rigorosi basati su metodi formali. Ogni anno alla conferenza viene proposto un caso di studio da risolvere applicando diverse tecniche nell’ambito dei metodi formali. Quest’anno, il caso di studio riguarda un ventilatore meccanico polmonare (Mechanical Lung Ventilator) per controllare/supportare i pazienti che necessitano di ventilazione meccanica. All’evento è principalmente coinvolto il gruppo di docenti e ricercatori del FOSELAB (Formal Methods & Software Engineering Laboratory) del Dipartimento di Ingegneria Gestionale, della Produzione e dell’Informazione dell’Università di Bergamo: il prof. Angelo Gargantini, la prof.ssa Patrizia Scandurra, il dott. Claudio Menghi, la dott.ssa Silvia Bonfanti e il dott. Andrea Bombarda. L’evento vede anche la compartecipazione del Dipartimento di Informatica dell’Università degli Studi di Milano, con la prof.ssa Elvinia Riccobene nel ruolo di program chair della conferenza insieme al prof. Michael Leuschel dell’Università di Düsseldorf (Germania).
