@proceedings {BaruzzoC06a, title = {Static Verification of UML Model Consistency}, journal = {MoDeV{$^2$}a: Model Development, Validation and Verification}, year = {2006}, month = {October}, pages = {111{\textendash}126}, publisher = {University of Queensland}, abstract = {UML is nowadays a de-facto standard for design and development of (object-oriented) software. With version 2.0 UML has achieved a more precise formal semantics. The same happened to OCL, a specification language which is an integral part of UML that allows to embed software contracts in the model. In a UML model, different aspects of a system are covered by different types of diagrams and this bears the risk that an overall system specification becomes inconsistent or incomplete. Hence, it is important to provide means to check the consistency and completeness of a UML model. In this work we propose an approach for a static verification of consistency of UML models which relies on OCL constraints. Many approaches for model validation and verification rely on generation of suitable code which dynamically (i.e., at run-time) checks the validity of OCL constraints. This approach has several drawbacks. For example, it cannot generally guarantee that a constraint will never be violated, unless an infinite number of tests is performed. Also the generation of just a significative finite subset is not so feasible because, on one hand, a considerable manual effort is needed even to produce a single test scenario and, on the other hand, test-case generation is well-known to be a hard problem. On the other hand, static approaches based on model checking suffer of the state explosion problem and thus cannot scale to most system sizes. In this paper we propose a static verification technique that, by using OCL constraints together with Class Diagrams, certifies that the dy- namic part of the model is satisfied. This encompasses the weaknesses of the other mentioned methods as it does not require users to build test scenarios and also performs the verification of all system properties at the same time.}, keywords = {OCL, UML diagrams, UML models, Validation, Verification}, url = {http://modeva.itee.uq.edu.au}, author = {Andrea Baruzzo and Marco Comini}, editor = {Hearnden, D. and S{\"u}{\ss}, J. G. and Benoit Baudry and Rapin, N.} }