Concurrency and Refinement in the Unified Modeling Language by Davies, J, Crichton, C

“…This paper shows how a formal notion of refinement may be defined for models, and model components, expressed in the Unified Modeling Language (UML). A formal, behavioural semantics is given to combinations of class, object, and state diagrams, using the notation of Communicating Sequential Processes (CSP); this semantics is adequate for the analysis of concurrent, communicating behaviour, and induces a notion of refinement for UML based upon existing notions of traces and failures refinement for CSP.…”

Concurrency and Refinement in the Unified Modeling Language by Davies, J, Crichton, C

“…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). …”

A Method for the Automatic Generation of Test Suites from Object Models by Davies, J, Crichton, C, Cavarra, A

“…This paper explains how object models written in the Unified Modeling Language (UML) can be translated into formal, behavioural descriptions and used as a basis for automatic test generation. …”

A Method for the Automatic Generation of Test Suites from Object Models by Cavarra, A, Crichton, C, Davies, J

“…This paper shows how object-oriented specifications, written in the Unified Modeling Language (UML) can be translated into formal, behavioural descriptions and used as a basis for automatic test generation. …”

Using State Diagrams to Describe Concurrent Behaviour by Davies, J, Crichton, C

“…The state diagram notation, a derivative of Harel's StateCharts, is an important component of the Unified Modeling Language (UML). It is the primary means of describing object behaviour: by associating a state diagram with a particular class, a designer may specify how objects of that class should perform sequences of actions in response to incoming events. …”