Where academic tradition
meets the exciting future

Formalising UML Use Cases in the Refinement Calculus

Ralph-Johan Back, Luigia Petre, Ivan Porres, Formalising UML Use Cases in the Refinement Calculus. TUCS Technical Reports 279, Turku Centre for Computer Science, 1999.


The Unified Modeling Language (UML) consists of a set of diagrams that describe a system under development. A use case diagram specifies the required functionality of the system, showing the collaboration among a set of actors that are to perform certain tasks. We enhance use case diagrams by providing formal documents (like specifications or programs), called contracts that regulate the behaviour of the agents involved. These agents could be programs, modules, systems, users. The contract is written in a language with a precise semantics and logic for reasoning, the refinement calculus. Hence, it can be analysed for the preconditions required in order to achieve certain goals. In order to express contracts we also need to specify the problem domain of the system; using refinement calculus for this too, we specify classes and UML class diagrams. Thereby, we integrate the functional view of a system, described by the use case diagram with the object-oriented view for the same system, described by the class diagram. We demonstrate this approach by formally describing and analysing a small though nontrivial example.


Full publication in PDF-format

BibTeX entry:

  title = {Formalising UML Use Cases in the Refinement Calculus},
  author = {Back, Ralph-Johan and Petre, Luigia and Porres, Ivan},
  number = {279},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {1999},
  keywords = {UML Use Case diagrams, User Requirements, Problem Domain, Formal Contracts},
  ISBN = {952-12-0464-8},

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication