An Integrated Framework for the Validation and Verification of UML Models

UML is widely adopted for modelling object-oriented software systems, including diagrams that cover the several facets of the entire development life cycle. Approaches to formal semantics of UML tend to concentrate on individual diagrams and, so far, no complete, standard, semantics is available. Here, we explore a different path and define a natural-language semantics for UML models that embody state machines and composite structure diagrams. We then integrate with the NAT2TEST strategy to provide means for an integrated framework for the validation (via simulation) and verification (via testing - QuickChick, interactive theorem proving - Rocq, and model checking - FDR) of UML models. The integration is based on a systematic process (mapping rules), and its soundness has been validated considering an independent reference formal semantics. The developed tool support uses ATL to implement the translation from UML models to natural-language requirements directly based on the proposed mapping rules. We illustrate our contributions and tool support with respect to two case studies: the classical Dijkstra's dining philosophers problem, and a distributed ring-buffer model.