Enriching OCL Using Observational Mu-Calculus

Research output: Chapter in Book/Report/Conference proceedingConference contribution


The Object Constraint Language is a textual specification language which forms part of the Unified Modelling Language[ 8 ]. Its principal uses are specifying constraints such as well-formedness conditions (e.g. in the definition of UML itself) and specifying contracts between parts of a system being modelled in UML. Focusing on the latter, we propose a systematic way to extend OCL with temporal constructs in order to express richer contracts. Our approach is based on observational mu-calculus, a two-level temporal logic in which temporal features at the higher level interact cleanly with a domain specific logic at the lower level. Using OCL as the lower level logic, we achieve much improved expressiveness in a modular way. We present a unified view of invariants and pre/post conditions, and we show how the framework can be used to permit the specification of liveness properties.
Original languageEnglish
Title of host publicationFundamental Approaches to Software Engineering
Subtitle of host publication5th International Conference, FASE 2002 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8–12, 2002 Proceedings
EditorsRalf-Detlef Kutsche, Herbert Weber
PublisherSpringer-Verlag GmbH
Number of pages27
ISBN (Print)978-3-540-43353-8
Publication statusPublished - 2002

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint Dive into the research topics of 'Enriching OCL Using Observational Mu-Calculus'. Together they form a unique fingerprint.

Cite this