Una metodologia per la modellazione formale di sistemi critici basata su metodi e tecniche di model driven engineering

I sistemi basati su calcolatore sono ormai presenti nella nostra vita di ogni giorno e ne influenzano molti aspetti, a volte senza che di ciò si abbia neanche precisa cognizione. I sistemi che forniscono supporto indispensabile alle attività economiche, ai trasporti e alle comunicazioni, per non tacere dei sistemi che vengono utilizzati in campo biomedico o nell’automazione industriale e di altri sistemi a cui sono demandati servizi critici in termini di sicurezza fisica di persone e beni, hanno ormai raggiunto livelli di complessità che ne rendono estremamente difficile la progettazione, lo sviluppo e - una volta operativi – la necessaria manutenzione al fine di garantire che i requisiti di affidabilità e sicurezza continuino ad essere soddisfatti durante l’esercizio. Tali sistemi presentano in genere un’architettura distribuita di grandi dimensioni in cui la complessità è dovuta anche alla forte eterogeneità dei componenti, sia a livello hardware che software. Essi devono rispondere a diversi requisiti, dettati nel caso di sistemi critici anche da standard internazionali, il cui soddisfacimento deve essere dimostrato, anche ai fini della necessaria certificazione. Pertanto è indispensabile che il processo di sviluppo (esteso anche agli aspetti legati all’esercizio ed alla manutenzione) sia tale da rendere possibile l’evidenza formale del rispetto dei requisiti. A tale scopo sono stati investigati nel passato e quindi applicati allo sviluppo dei sistemi approcci di modellazione formale che, costruendo un modello del sistema ne consentono l’analisi e quindi sia la validazione che la verifica di proprietà. E’ ben noto però che l’applicazione di metodi formali in ambito industriale – sebbene fortemente consigliato quando non obbligatorio – è rallentato dalle difficoltà dettate da un lato dalla complessità dei modelli (che rispecchia la complessità dei sistemi), e dall’altro dalla necessità di avere personale formato nell’uso dei linguaggi formali e nello sviluppo di modelli. In altre parole, si ravvisa la necessità di metodologie di sviluppo e di strumenti di supporto alla modellazione. Così come nel tempo si è affermata come disciplina l’ ingegneria del software, così attualmente si sente la necessità di una ingegneria dei modelli che definisca le opportune metodologie e i processi necessari a ingegnerizzare le attività di sviluppo di modelli complessi e a migliorare il rapporto qualità/costo anche nell’ambito della modellazione formale. Allo stato attuale in letteratura sono presenti diversi approcci, che possono essere ricondotti a due linee fondamentali: a) metodologie e strumenti per la composizionalità ed il multiformalismo, e relative tecniche di soluzione; b) derivazione (possibilmente automatica) di modelli formali da modelli di alto livello del sistema utilizzati nella specifica e nella progettazione. La presente tesi si pone in questo contesto l’obiettivo di definire una metodologia di sviluppo che consenta di integrare queste due linee e di trarre vantaggio quindi sia dalla possibilità di uno sviluppo di modelli “per componenti”, sia dalla possibilità di derivare automaticamente modelli formali da modelli di alto livello del sistema e dei relativi requisiti grazie alla attuale disponibilità di framework attualmente utilizzati nello sviluppo di sistemi software in ambito di Model Driven Engineering (MDE). Il contributo originale della tesi è nella definizione della metodologia e delle sue fasi, nella definizione e nello sviluppo di alcune tecniche a supporto e nel particolare focus applicativo orientato alla manutenibilità dei sistemi critici, aspetto questo non sufficientemente trattato in letteratura e di particolare importanza per i sistemi critici