@proceedings {BaruzzoC06,
	title = {Checking UML Model Consistency},
	journal = {Proceedings of CILC 2006 - Convegno Italiano di Logica Computazionale},
	year = {2006},
	pages = {1{\textendash}15},
	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 this work we propose an approach for a static verification of consis- tency 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 real system sizes. In this paper we propose a static verification technique that, by using OCL constraints together with class diagrams, certifies that the dynamic part of the model is satisfied. This encompasses the weaknesses of the other mentioned methods as it does not require users to build test sce- narios and also performs the verification of all system properties at the same time.},
	author = {Andrea Baruzzo and Marco Comini}
}
