Scalable Formal Verification of UML Models

UML (Unified Modeling Language) has been used for years in diverse domains. Its notations usually come with a reasonably well-defined syntax, but its semantics is left under-specified and open to different interpretations. This freedom hampers the formal verification of produced specifications and calls for more rigor and precision. This work 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 work also proposes a bit-vector-based encoding of LTL formulae. The first 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 formulae.