On state-oriented vs. event-oriented thinking in formal behavioural specifications

Bolognesi T.

Formal methods  Process algebra  ASM  CCS  CSP  High-level Petri nets  LOTOS  TLA 

In this paper an extension of a behavioural subset of UML Statecharts for modeling mobility issues is proposed. The extension builds on the notion of Multicharts, as proposed by the authors in previous work. A Multichart is a collection of Statecharts, where each Statechart is associated with a unique input queue. In a Multichart each Statechart can address its output events directly to each (other) Statechart of the Multichart by explicitly mentioning the name of (the unique queue of) such Statechart in its output actions. The extension we present consists in relaxing the unique association between each Statechart and its input-queue and in allowing the the use of (queue) name variables in communication actions. The resulting communication paradigm is much more flexible than the standard asymmetric one and is well suited for the modelling of mobility-oriented as well as fault tolerant systems.

Source: ISTI Technical reports, 2003