| A good design is crucial to the development of quality software. Despite this, behavior correctness is validated on partially or fully implemented software. Yet, it is estimated that correcting an error is 50--200 times more costly during implementation than during design [BP88]. Hence the need for design validation techniques.; We propose one such technique for the Unified Modeling Language ( UML) notation, which is the de facto industrial design language. It consists of a model-checking framework for the Object Constraint Language (OCL), which is a integral part of the UML standard. Model-checking is a highly automated formal method that has found industrial applications [Cim01]. This thesis also aims at designing tool support for the described model-checking framework. The tool implements the automatic extraction and compilation of a UML model, the computation of the model's execution graph and the model-checking of OCL constraints.; The OCL language is divided into expressions and constraints. OCL expressions are integrated into the UML semantics in guards, method calls and assignation actions. Their semantics is developed as a recursive function over the formal representation of a UML model configuration. Given a configuration and a variable environment (containing at least a value for the special variable self), the function returns the value of the evaluated expression by recursively evaluating subexpressions. (Abstract shortened by UMI.)... |
