ITU-T Rec. Z.120 Annex B (04/1998) Message Sequence Chart Annex B: Formal semantics of Message Summary Source FOREWORD CONTENTS B.1 Introduction B.2 Message Sequence Charts B.2.1 Introduction B.2.2 Basic Message Sequence Charts B.2.3 Additional Basic Concepts B.2.4 Ordering facilities B.2.5 Combining MSCs with composition constructs B.3 Message Sequence Charts with Gates B.3.1 Gates B.3.2 MSC reference expressions and gates B.3.3 Inline expressions and gates B.4 Process theory for Message Sequence Charts B.4.1 Introduction B.4.2 Operational semantics B.4.3 Equivalence of processes B.4.4 Deadlock, empty process and atomic actions B.4.5 Delayed choice B.4.6 Delayed parallel composition B.4.7 Weak sequential composition B.4.8 Generalization of the composition operators B.4.9 Renaming operator B.4.10 Repetitive behaviour B.5 Textual syntax of MSC for the semantics B.5.1 Changes to the textual syntax B.5.2 Textual syntax for semantics definition B.6 Semantics of Message Sequence Charts B.6.1 Introduction B.6.2 The approach B.6.3 Semantics of an MSC document B.6.4 Semantics of events B.6.5 Semantics of causally ordered events B.6.6 Vertical and horizontal composition of MSC fragments B.6.7 Semantics of coregions B.6.8 Semantics of MSC bodies B.6.9 Semantics of MSC reference expressions B.6.10 Semantics of inline expressions B.6.11 Semantics of High-level Message Sequence Charts References