Analysing UML active classes and associated state machines - A lightweight formal approach

Abstract

We propose a precise denition of UML active classes through associated labelled transition systems using the algebraic specication language Casl. We are convinced that the first step to make UML pre- cise is to and an underlying formal model for the systems modelled by UML, and we argue that labelled transition systems are a sensible choice. This modelization will help understanding the UML constructs and will improve their use in practice. One of our aims is, in the future, to use the powerful animation and verication tools available for algebraic spec- ications with UML specications. We simplify the problem of the ap- plicability of our semantics by restricting the state machine constructs considered. This restriction does not, however, narrow the UML subset in study because the restricted constructs can be replaced by equiva- lent combinations of other constructs. Because of some ambiguities in the UML social semantics, we discuss the several options at hand and choose, for each ambiguous case, the semantics that either makes more sense or that allows to simplify the problem the most.