I ricercatori della Fondazione Bruno Kessler (FBK) di Trento hanno realizzato uno studio scientifico congiunto con la Boeing dedicato all’analisi di sicurezza basata su modelli formali matematici che verrà presentato alla più importante conferenza mondiale nel settore della verifica formale, CAV 2015, in programma dal 18 al 24 luglio a San Francisco.

L’importante collaborazione del centro di ricerca trentino con il colosso internazionale dell’aerospazio è nata grazie alla pluriennale esperienza di settore dell’Unità Embedded Systems guidata da Alessandro Cimatti e appartenente al Centro ICT della FBK, diretto da Paolo Traverso.  

Lo studio è stato realizzato nell’ambito dell’analisi di sicurezza basata su modelli formali (model-based safety assessment – MBSA) che ha permesso di partecipare tra l’altro a progetti dell’Agenzia Spaziale Europea e che ha aperto la strada ad applicazioni pionieristiche in ambito industriale. Proprio con la Boeing la FBK ha firmato nel 2014 un accordo strategico di collaborazione, di durata quinquennale, e, nel contesto di questo accordo, Boeing ha finanziato un progetto di ricerca e sviluppo congiunto.

Lo scopo è investigare l’applicazione di tecniche per l’analisi di sicurezza, basate su modelli formali, al processo di Boeing, con l’obiettivo di dimostrarne l’utilità e l’adeguatezza per migliorare lo sviluppo complessivo e per supportare la certificazione dei sistemi. Il primo studio scientifico che sarà presentato a San Francisco riguarderà in particolare i sistemi di frenatura degli aerei in fase di atterraggio. «Si tratta - spiega il ricercatore FBK Marco Bozzano che ha realizzato lo studio con Alessandro Cimatti, Anthony Fernandes Pires e Stefano Tonetta e, per parte di Boeing, con David Jones, Greg Kimberly, Tyler Petri e Richard Robinson - di analizzare con dei modelli matematici tutti i possibili scenari in fase di progettazione e di procedere alla loro verifica, sempre utilizzando software automatici di risoluzione. In questo modo si affianca il tradizionale lavoro ingegneristico offrendo ulteriori garanzie relative al buon funzionamento dei sistemi coinvolti in tutti gli scenari di interesse».

In questo campo la FBK ha sviluppato e detiene la proprietà intellettuale di numerose tecnologie e strumenti, inclusi il sistema per l’analisi di affidabilità denominato xSAP e il sistema per l’analisi di correttezza denominato nuXmv.