Logic-based verification of multi-diagram UML models for timed systems
Alfredo Motta · 2013
Il linguaggio di modellazione UML (Unified Modeling Language) e in assoluto lo strumento piu diffuso per la documentazione e la diffusione del design del software. Negli ultimi anni da semplice mezzo comunicativo si e evoluto sempre di piu verso uno strumento avanzato per la specifica, l'analisi e l'implementazione di sistemi software complessi. Tuttavia nonostante alcuni buoni risultati preliminari la diffusione dei modelli UML per l'analisi dei sistemi software in ambito aziendale e ancora frenata da delle importanti difficolta. In primo luogo e necessario sviluppare una semantica unificata e coerente del linguaggio. Negli ultimi dieci anni gli sforzi della comunita scientifica hanno portato allo sviluppo di diverse semantiche , ma i risultati finali sono sempre stati poco soddisfacenti. Nonostante l'ampio consenso attribuito alla semantica di alcuni diagrammi UML, la semantica unificata delle sue diverse viste , specialmente quelle comportamentali, e ancora oggetto di dibattito. La dimensione del linguaggio insieme alla sovrapposizione di diversi elementi sintattici ha fortemente ostacolato la sua completa formalizzazione; UML e infatti composto da 9 tipi di diagrammi ognuno dei quali possiede un numero non indifferente di costrutti sintattici. Gli approcci in letteratura hanno potuto focalizzarsi solo sull'analisi di un numero limitato di viste (il piu delle volte una sola), tralasciando le interdipendenze con gli altri diagrammi. In secondo luogo, per diffondere l'utilizzo di UML per la verifica dei modelli in ambito aziendale, la semplicita di utilizzo dei metodi formali adibiti all'analisi va rivista e migliorata. Nell'approccio classico alla verifica formale e necessaria la costruzione manuale di un modello del sistema che lo rappresenti fedelmente e che sia espresso nel linguaggio accettato dallo strumento di verifica. La costruzione di tale modello richiede tipicamente un'ottima conoscenza sia del dominio applicativo, sia della tecnologia utilizzata per la verifica. A sua volta questo richiede la padronanza di tecniche come l'abstraction and refinement, il model checking, o il theorem proving che richiedono una formazione dedicata. La costruzione manuale del modello formale e un attivita molto dispendiosa in termini di tempo e facilmente soggetta ad errori, di conseguenza sono stati sviluppati diversi strumenti per trasformare i modelli UML nelle loro corrispondenti rappresentazioni formali. Tuttavia la maggior parte di questi non si cura di mascherare opportunamente i dettagli della notazione formale e gli strumenti sottostanti all'utilizzatore di UML, il quale solitamente non e in grado ne di avviare la fase di verifica, ne di comprendere i risultati della stessa. Questo compito viene conseguentemente affidato a un esperto di verifica formale, rendendo l'analisi dei modelli UML un attivita confinata alla comunita scientifica. Questa tesi rappresenta un importante passo verso la soluzione dei problemi di cui sopra mediante un avanzato sistema di verifica composto dai seguenti elementi: - Un significativo sottoinsieme di UML, chiamato MADES UML. MADES UML e composto da un insieme eterogeneo di viste comportamentali messe in comunicazione da un insieme di eventi condivisi. I costrutti del linguaggio sono stati accuratamente selezionati per permettere di modellare e verificare efficacemente gli aspetti temporali del sistema sotto analisi. - Una semantica formale basata su una logica temporale del prim'ordine, con una nozione metrica di tempo. L'approccio logico offre la flessibilita e la scalabilita necessaria per la formalizzazione di un linguaggio ricco come MADES UML. La semantica attribuita ai modelli viene poi utilizzata per la verifica mediante un bounded model/satisfiability checker per permettere agli utenti di verificare le proprieta del loro sistema sin dalle prima fasi del design. - Un prototipo di sistema di verifica integrato, chiamato Corretto. Usando Corretto per il design e l'analisi del proprio design l'utente puo utilizzare una notazione ricca e diffusa come UML, senza pero dover rinunciare ai vantaggi di un ambiente di verifica avanzato. Le proprieta da verificare per il sistema sono espresse mediante l'utilizzo di una notazione di alto livello, e i risultati della verifica sono associati ai corrispondenti elementi del modello UML permettendo quindi una interpretazione semplificata degli stessi.