Verifying UML/OCL Operation Contracts

Download Now Free registration required

Executive Summary

In current model-driven development approaches, software models are the primary artifacts of the development process. Therefore, assessment of their correctness is a key issue to ensure the quality of the final application. Research on model consistency has focused mostly on the models' static aspects. Instead, this paper addresses the verification of their dynamic aspects, expressed as a set of operations defined by means of pre/post-condition contracts. This paper presents an automatic method based on Constraint Programming to verify UML models extended with OCL constraints and operation contracts. In the authors' approach, both static and dynamic aspects are translated into a Constraint Satisfaction Problem.

  • Format: PDF
  • Size: 698.4 KB