Scalable formal verification of UML models

The Unified Modeling Language (UML) is a general-purpose platform-independent modeling language, created and managed by the Object Management Group (OMG). During recent years, UML has transformed from a relatively basic descriptive tool to a sophisticated prescriptive one that can be used to specify, analyze and implement complex software systems. It offers a heterogeneous set of diagrams to describe the different views of a software system during the Model-Driven Development (MDD) process. Model defects are a significant concern in the MDD paradigm, as model transformations and code generation may propagate errors to other notations where they are harder to detect and trace. To avoid this problem, formal verification techniques are used, that can check the correctness of models and verification results often reveal unexpected behaviors in the models, which if left unresolved, may lead to a tremendous cost in the later stages of the development. UML notations usually come with a reasonably well-defined syntax, but their semantics are left underspecified and open to different interpretations. This freedom hampers the formal verification of produced specifications and calls for more rigor and precision. This thesis aims to bridge this gap and proposes a flexible and modular formalization approach based on temporal logic. We studied the different interpretations for some of its constructs, and our framework allows one to assemble the semantics of interest by composing the selected formalizations for the different pieces. However, the formalization per se is not enough. The verification process, in general, becomes slow and impossible --as the model grows in size. To tackle the scalability problem, this thesis also proposes an efficient bit-vector-based encoding of LTL/CLTL formulae. The experimental results witness a significant increase in the size of analyzable models, not only for our formalization of UML models, but also for numerous other models that can be reduced to bounded satisfiability checking of LTL/CLTL formulae. This thesis contributes towards formal specification of UML/eFT-UML (extensible Formal, Timed UML) models by flexible modular semantics implemented in Corretto, our verification tool, that covers a significant number of diagram types in a single coherent framework. Moreover, the proposed bit-vector-based encodings are implemented as plugins in Zot Bounded Model/Satisfiability Checker to tackle the scalability problem of Corretto.

UML (Unified Modeling Language) è un linguaggio di modellazione ``generico’’ per sistemi ad oggetti creato e gestito da Object Management Group (OMG). Negli ultimi anni, UML si è trasformato da uno strumento descrittivo relativamente semplice ad una notazione sofisticata e prescrittiva che può essere utilizzata per specificare, analizzare e gestire sistemi software complessi. Il linguaggio offre un insieme eterogeneo di diagrammi per descrivere i diversi punti di vista di un sistema software durante il processo di sviluppo Model-Driven (MDD). Gli eventuali errori o difetti nei modelli rappresentano un problema fondamentale nel paradigma MDD: le trasformazioni tra modelli e la generazione di codice potrebbero propagare errori e renderli più difficili da individuare e tracciare. Per evitare questo problema, qualcuno ha iniziato a utilizzare tecniche di verifica formale, in grado di controllare la correttezza dei modelli e i risultati della verifica spesso rivelano errori e comportamenti non previsti, che, se non gestiti, possono portare ad un costo enorme nelle fasi successive dello sviluppo. UML solitamente ha una sintassi abbastanza ben definita, ma la semantica non è completamente specificata e lascia spazio a diverse interpretazioni. Questa libertà ostacola la verifica formale delle specifiche prodotte e chiede più rigore e precisione. Questa tesi si propone di colmare questa lacuna e propone un approccio flessibile e modulare per la formalizzazione di UML utilizzando la logica temporale come notazione di riferimento. Abbiamo studiato le diverse interpretazioni per alcuni dei costrutti principali di UML, e la nostra proposta consente di ottenere la semantica di interesse componendo le formalizzazioni selezionate per i diversi elementi. Tuttavia, la formalizzazione di per sé non è sufficiente. Il processo di verifica, in generale, diventa lento e, magari, impossibile al crescere delle dimensioni del modello da analizzare. Per affrontare il problema della scalabilità, questa tesi, quindi, propone anche una codifica di formule LTL/CLTL basata su logica bit-vector particolarmente efficiente. I risultati sperimentali testimoniano un significativo aumento della dimensione dei modelli analizzabili, non solo per la formalizzazione di modelli UML, ma anche per numerosi altri problemi che possono essere ricondotti alla verifica ``bounded’’ di formule LTL/CLTL. In particolare, questa tesi propone la specifica formale di modelli UML/EFT-UML (Extensible, Formal, Timed UML) attraverso moduli semantici flessibili realizzati in Corretto, il nostro strumento di verifica. Questo copre un numero significativo di tipi di diagrammi UML in un unico contesto di riferimento. Inoltre, la codifica basata su logica bit-vector è stata implementata come plugin di Zot (il nostro bounded model/satisfiability checker) per gestire il problema della scalabilità in Corretto.