Relating computer systems to sequence diagrams with underspecification, inherent nondeterminism and probabilistic choice : Part 2

Abstract

Having a sequence diagram specification and a computer system, we need to answer the question: Is the system compliant with the sequence diagram specification in the desired way? We present a procedure for answering this question for three variations of sequence diagrams. The procedure does not require access to information about the internals of the system such as program code.

The semantics of sequence diagrams is denotational and based on traces. In order to answer the initial question, the procedure starts by obtaining a basic representation of the system by e.g. testing.This representation is then transformed into the same semantic model as that used for the sequence diagram. Finally, a formal definition of compliance is applied to determine whether the system complies with the specification. Compliance is closely related to refinement, and the definitions of compliance are based on refinement definitions. Therefore refinement as well as compliance is addressed. Compliance is not identical to refinement due to the partial nature of sequence diagram specifications.

The work is split in two parts. Part 1 [RRS07] introduces the necessary definitions for using the compliance checking procedure on sequence diagrams with underspecification and sequence diagrams with inherent nondeterminism. This paper presents Part 2, in which we introduce the necessary definitions for using the compliance checking procedure on sequence diagrams with probabilistic choice. Part 1 is a necessary prerequisite for Part 2.