An Integrated Framework for Analysing, Simulating and Testing 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 a component UML model that embodies state machines and composite structure diagrams. We then integrate with the NAT2TEST strategy to provide means for analysis (via model checking and theorem proving), simulation and testing. 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 automates 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.