Download Version3.0 Manual

Table of Contents
Introduction.........................................................................................................................................................4
1 Message Sequence Charts................................................................................................................................6
1.1 Basic MSCs...............................................................................................................................................6
1.1.1 Graphical Representation ............................................................................................. 7
1.1.2 Z120 features not addressed :...................................................................................... 8
1.1.3 Basic MSc semantics: ................................................................................................ 10
1.2 High level MSCs.....................................................................................................................................12
1.2.1 Graphical Representation ........................................................................................... 13
1.2.2 High-level MSCs hierarchy ......................................................................................... 14
1.2.3 A note on MSC sequence ........................................................................................... 15
1.2.4 A note on Atoms ...................................................................................................... 17
1.2.5 High level MSCs semantics......................................................................................... 18
1.3 MSC Documents .....................................................................................................................................21
2 Properties of Message Sequence Charts ........................................................................................................23
2.1 Frequently addressed problems with MSCs............................................................................................23
2.1.1 Model checking ........................................................................................................ 23
2.1.2 Comparison of MSC descriptions ................................................................................. 25
2.1.3 Specification and implementation................................................................................ 25
2.2 General undecidable results ....................................................................................................................27
2.3 Syntactical description of MSC subclasses.............................................................................................28
2.3.1 Regular MSCs (RMSCs).............................................................................................. 28
2.3.2 Local choice MSCs (LMSCs) ........................................................................................ 30
2.3.3 Globally cooperative MSCs (GCMSCs) .......................................................................... 35
2.3.4 Simulable MSCs ....................................................................................................... 37
2.4 Bounds ....................................................................................................................................................38
2.5 Simulation ...............................................................................................................................................38
3 SOFAT ...........................................................................................................................................................40
3.1 Installation...............................................................................................................................................40
3.2 Running SOFAT V3 ...............................................................................................................................41