Skip to main content

Concurrency and Refinement in the Unified Modeling Language

Jim Davies and Charles Crichton

Abstract

This paper defines a formal semantics for a subset of the Unified Modeling Language (UML). It shows how suitable combinations of class, object, state, and sequence diagrams can be associated with patterns of interaction, expressed in the event notation of Communicating Sequential Processes (CSP). The diagram semantics is then extended to give a meaning to complete models - suitable combinations of diagrams - and thus a concurrency semantics for object models written in UML. This model semantics is in turn used to define a theory of refinement, based upon existing notions of data and process refinement.

Journal
Formal Aspects of Computing
Number
2−3
Pages
118−145
Publisher
Springer London
Volume
15
Year
2003