On testing and conformance relations for UML statechart diagrams behaviours

In this paper we study the formal relationship between testing preorder/equivalences for a behavioural subset of UML Statechart Diagrams and a conformance relation for implementations with respect to specifications given using such diagrams. We study the impact of stuttering on the above mentioned relationship. In the context of UMLSDs, stuttering occurs when no transition of the UMLSD is enabled by the current event in the current (global) state of the underlying state-machine. We consider both the case in which the semantics underlying the testing relations does not model stuttering explicitly - we call it the non-stuttering semantics - and the case in which it does it - i.e. the stuttering semantics. We show that in the first case the conformance relation is stronger than the reverse of the MUST preorder and, consequently, stronger than the MAY preorder. Much more interesting results can be proven in the second case, possibly under proper conditions on the sets of events under consideration. In fact the conformance relation is shown to coincide with the MAY preorder, and thus be implied by the reverse MUST preorder. Finally, we show important substitutivity properties which hold in the case of stuttering semantics.