Al Centro internazionale di scienze meccaniche si sono riuniti una settantina di ricercatori da tutto il mondo per approfondire le potenzialità dei “metodi formali” che testano sistemi per il controllo del traffico aereo o per veicoli a guida autonoma prima ancora che vengano realizzati. L'informatica ha diverse frontiere, oltre l’intelligenza artificiale e il machine learning, su cui gli scienziati sono impegnati. Una di queste riguarda i “metodi formali” che consentono di verificare l’efficacia di sistemi, come circuiti elettronici o programmi software, prima ancora della loro realizzazione.

La ricerca

“La verifica dei sistemi è fondamentale per quelli molto critici, come sono quelli per veicoli a guida autonoma, i sistemi di controllo del traffico aereo o ferroviario e gli impianti di produzione di energia”, spiega il professor Angelo Montanari, dell’Università di Udine. È stato proprio lui, assieme al collega di ateneo Gabriele Puppis e a Tiziano Villa dell'Università di Verona, ad aver coordinato la scuola estiva che per l’intera settimana ha impegnato nel Cism di Udine una settantina di ricercatori (due terzi in presenza e un terzo da remoto) provenienti da diverse nazioni: Italia, Germania, Belgio, Olanda, Regno Unito, Polonia, Austria, Francia, Islanda, Romania, Cina, India, Russia, Ungheria, Danimarca, Malta e Israele. “I metodi formali – continua Montanari - costruiscono dei modelli dei sistemi e consentono di verificare in modo rigoroso, ovvero matematico, se essi soddisfano o meno un certo insieme di proprietà desiderate prima di costruire effettivamente il sistema. Numerosi strumenti software, basati sui metodi formali studiati dai ricercatori, sono stati sviluppati e vengono correntemente utilizzati per eseguire in modo automatico tali verifiche”.

A Udine

Il lavoro fatto a Udine ha cercato di affrontare questioni poste già negli anni ’50 da Alonzo Church, uno dei padri riconosciuti dell'informatica, tra cui quella di poter produrre sistemi-programmi corretti per costruzione. Questo è possibile, ad esempio, nella sintesi di controllori di piano e di strumenti che consentono di monitorare il comportamento di un sistema, riconoscendo per tempo l'insorgenza di situazioni che, in assenza di interventi appropriati, causerebbero malfunzionamenti o guasti del sistema stesso. Udine si conferma così un punto di riferimento internazionale in questo settore dell’informatica al pari dei più celebri e blasonati atenei. Già nel 1978 il Cism aveva ospitato la quinta edizione di una delle conferenze internazionali più importanti di informatica teorica (International Colloquium on Automata, Languages and Programming), organizzata dall'Associazione europea di informatica teorica, e nel 2018 l’ateneo friulano ha organizzato il convegno annuale europeo dell'Associazione di logica simbolica (Logic Colloquium).