Logic-based verification of multi-diagram UML models for timed systems

The Unified Modeling Language (UML) has gone from a relatively basic descriptive tool (i.e., a tool that serves to document software systems) to a sophisticated prescriptive one, that is, a tool that can be used to specify, analyze and implement complex software systems. Despite some good results in this field some fundamental problems hamper the actual adoption of UML models for the analysis of the systems in a real production environment. First, a unified and coherent semantics of UML must be developed. In the last ten years researchers have been trying to ascribe UML with many different semantics, but all these attempts have been partial. While there seems to be a general consensus on the semantics of some individual diagrams, the composite semantics of the different views is still an open problem. The wide spectrum of the notation and the heterogeneity and overlapping of the different modeling elements have played against its complete formalization; as a matter of fact most of the existing approaches only focus on a limited number of diagrams (oftentimes they only consider a single type) and neglect the interdependencies with the other views of the system. However multiple views mean better quality since different UML diagrams emphasize different aspects of the system. Second, to spread the use of UML model verification at large scale the inherent complexity of formal methods in terms of usability must be decreased. For example in the classical approach to formal analysis the user is required to manually construct the formal model of the system in the language that is accepted by the verification tool. The construction of such model typically requires good knowledge of both the application domain and of the verification technology. In turn this activity requires mastering techniques like abstraction and refinement, model checking, or theorem proving that require a dedicated background. To avoid the manual construction of the formal model different tools have been developed to transform the UML models to a variety of formal notations, but the vast majority of them neglet the difficulty of hiding the underlying formal notations and tools to the UML user. Without a dedicated expertise in this field the user is not able neither to enact the verification phase, or to understand the verification results. Oftentimes a formal verification expert is required, making the UML formal verification a niche activity. This thesis presents a significant step towards solving these problems by means of an advanced verification framework made of the following elements: - A significant and consistent subset of UML, called MADES UML, where timed-related properties can be modeled carefully. MADES UML supports different behavioral views connected by means of a shared set of events. - A formal semantics based on metric temporal logic which offers the flexibility and scalability we need to formalize a wide and rich notation like MADES UML. The formal semantics is used to feed a bounded model/satisfiability checker to allow users to verify their systems, even from the initial phases of the design. - An advanced prototype verification tool called "Corretto". Using "Corretto" UML engineers can exploit both a well-known modeling notation and advanced verification capabilities seamlessly. Properties are expressed using a high-level notation, and verification results produced by the underlying verification tool are linked back to the corresponding UML elements in the model.

Il linguaggio di modellazione UML (Unified Modeling Language) è in assoluto lo strumento più diffuso per la documentazione e la diffusione del design del software. Negli ultimi anni da semplice mezzo comunicativo si è evoluto sempre di più 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 è ancora frenata da delle importanti difficoltà. In primo luogo è necessario sviluppare una semantica unificata e coerente del linguaggio. Negli ultimi dieci anni gli sforzi della comunità 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, è ancora oggetto di dibattito. La dimensione del linguaggio insieme alla sovrapposizione di diversi elementi sintattici ha fortemente ostacolato la sua completa formalizzazione; UML è 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 più 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 semplicità di utilizzo dei metodi formali adibiti all'analisi va rivista e migliorata. Nell'approccio classico alla verifica formale è 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 è un attività 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 è in grado né di avviare la fase di verifica, né di comprendere i risultati della stessa. Questo compito viene conseguentemente affidato a un esperto di verifica formale, rendendo l'analisi dei modelli UML un attività confinata alla comunità 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 è 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 flessibilità e la scalabilità 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 proprietà 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 può utilizzare una notazione ricca e diffusa come UML, senza però dover rinunciare ai vantaggi di un ambiente di verifica avanzato. Le proprietà 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.