John.Wiley.And.Sons.Validation.Of.Communications.Systems.With.SDL

asic_ant

Contents
Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xi
Foreword . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xiii
1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.1 Validation of Communications Systems . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 SDL, Language to Master Complex Systems Development . . . . . . . . . . . . 2
1.2.1 Overview of SDL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.2.2 Benefits provided by SDL . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3 Simulation Life Cycle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.4 Contents of the Book . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.5 Tools and Platforms Used . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2 Quick Tutorial on SDL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.1 Structure of an SDL Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.1.1 System, block and process . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.1.2 Scope of declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.1.3 Process . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.1.4 Procedure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2 Communication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2.1 Signals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2.2 Channel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2.3 Signal route . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.3 Behavior . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.3.1 Structure of a transition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.3.2 Start . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.3.3 States . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3.4 Input . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3.5 Save . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.3.6 Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.3.7 Stop . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.3.8 Task . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.3.9 Create . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.3.10 Output . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.3.11 Decision . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.3.12 Timers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.4 Data Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.4.1 Predefined data . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.4.2 Array . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.4.3 Synonym and syntype . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.4.4 Newtype . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.5 Constructs for Better Modularity and Genericity . . . . . . . . . . . . . . . . . . . 22
2.5.1 Package . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.5.2 Types, instances and gates . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.5.3 Specialization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
3 The V.76 Protocol Case Study . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.1 Presentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.2 Specification of the V.76 Protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.2.1 Abbreviations used . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.2.2 Exchange identification procedures (XID) . . . . . . . . . . . . . . . . . . 27
3.2.3 Establishment of a data link connection . . . . . . . . . . . . . . . . . . . 27
3.2.4 Information transfer modes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.2.5 Release of a DLC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.3 Analysis MSCs for the V.76 Protocol . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.4 The SDL Model of V.76 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3.4.1 The simulation configuration of V.76 . . . . . . . . . . . . . . . . . . . . . 30
3.4.2 The package V76 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3.4.3 The block dataLink . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4 Interactive Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
4.1 Principles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
4.2 Case Study with Tau SDL Suite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
4.2.1 Prepare the Simulator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
4.2.2 Validate against the main scenarios . . . . . . . . . . . . . . . . . . . . . . 44
4.2.3 Detect a bug in the SDL model . . . . . . . . . . . . . . . . . . . . . . . . . 50
4.2.4 Detect nonsimulated parts . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
4.2.5 Validate against more scenarios . . . . . . . . . . . . . . . . . . . . . . . . . 58
4.2.6 Write a script for automatic validation . . . . . . . . . . . . . . . . . . . . 62
4.2.7 Other Simulator features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
4.3 Case Study with ObjectGeode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
4.3.1 Prepare the Simulator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
4.3.2 Validate against the main scenarios . . . . . . . . . . . . . . . . . . . . . . 75
4.3.3 Detect a bug in the SDL model . . . . . . . . . . . . . . . . . . . . . . . . . 79
4.3.4 Detect nonsimulated parts . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
4.3.5 Validate against more scenarios . . . . . . . . . . . . . . . . . . . . . . . . . 88
4.3.6 Write a script for automatic validation . . . . . . . . . . . . . . . . . . . . 93
4.3.7 Other Simulator features: watch, trace, filter etc. . . . . . . . . . . . . . . 95
4.4 Errors Detectable by Interactive Simulation . . . . . . . . . . . . . . . . . . . . . . 108
4.4.1 Dynamic errors detected by Tau SDL suite Simulator . . . . . . . . . . 108
4.4.2 Dynamic errors detected by ObjectGeode SDL Simulator . . . . . . . . 109
4.4.3 Dynamic errors not checked . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
5 Automatic Observation of Simulations . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
5.1 Principles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
5.1.1 Automatic checking of model properties . . . . . . . . . . . . . . . . . . . 111
5.1.2 Specificity of observation with MSCs in Tau SDL Suite . . . . . . . . 113
5.2 Case study with Tau SDL Suite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
5.2.1 Simulate with user-defined rules . . . . . . . . . . . . . . . . . . . . . . . . 114
5.2.2 Simulate with a basic MSC . . . . . . . . . . . . . . . . . . . . . . . . . . . 117
5.2.3 Simulate with an MSC containing inline operators . . . . . . . . . . . . 119
5.2.4 Simulate with an HMSC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
5.2.5 More details on MSCs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127
5.2.6 Simulate with observer processes . . . . . . . . . . . . . . . . . . . . . . . . 132
5.2.7 More details on observer processes . . . . . . . . . . . . . . . . . . . . . . 134
5.3 Case Study with ObjectGeode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136
5.3.1 Simulate with stop conditions . . . . . . . . . . . . . . . . . . . . . . . . . . 136
5.3.2 Simulate with a basic MSC . . . . . . . . . . . . . . . . . . . . . . . . . . . 139
5.3.3 Simulate with a hierarchical MSC . . . . . . . . . . . . . . . . . . . . . . . 142
5.3.4 More details on MSCs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149
5.3.5 Simulate with GOAL observers . . . . . . . . . . . . . . . . . . . . . . . . . 159
5.3.6 More details on GOAL observers . . . . . . . . . . . . . . . . . . . . . . . 161
6 Random Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
6.1 Principles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
6.2 Case Study with Tau SDL Suite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
6.2.1 Random simulation without observers . . . . . . . . . . . . . . . . . . . . 167
6.2.2 Multiple random simulations . . . . . . . . . . . . . . . . . . . . . . . . . . 169
6.2.3 Random simulation with observers . . . . . . . . . . . . . . . . . . . . . . . 170
6.3 Case Study with ObjectGeode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172
6.3.1 Random simulation without observers . . . . . . . . . . . . . . . . . . . . 172
6.3.2 Multiple random simulations . . . . . . . . . . . . . . . . . . . . . . . . . . 174
6.3.3 Random simulation with observers . . . . . . . . . . . . . . . . . . . . . . . 175
6.3.4 Details on random simulation . . . . . . . . . . . . . . . . . . . . . . . . . . 179
6.4 Errors Detectable by Random Simulation . . . . . . . . . . . . . . . . . . . . . . . 180
7 Exhaustive Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181
7.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181
7.1.1 Exhaustive simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181
7.1.2 Bit-state simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184
7.1.3 On-the-fly validation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184
7.2 Simple Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185
7.2.1 Exhaustive simulation of the ping TCP/IP command . . . . . . . . . . . 185
7.2.2 Exhaustive simulation of counters . . . . . . . . . . . . . . . . . . . . . . . 190
7.3 Case Study with Tau SDL Suite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191
7.3.1 One second to detect missing save of v76frame . . . . . . . . . . . . . . 192
7.3.2 One second to detect missing input L ReleaseReq . . . . . . . . . . . . 197
7.3.3 One second to detect missing input L DataReq . . . . . . . . . . . . . . 199
7.3.4 Millions of states: detect output to Null . . . . . . . . . . . . . . . . . . . 202
7.3.5 Forty seconds to detect missing save of L DataReq . . . . . . . . . . . 206
7.3.6 Two minutes to detect missing input L ReleaseReq and answer DM 210
7.3.7 Three minutes, 6.7 million states, no error . . . . . . . . . . . . . . . . . . 214
7.3.8 Bit-state simulation with a user-defined rule . . . . . . . . . . . . . . . . 217
7.3.9 Verifying an MSC with bit-state simulation . . . . . . . . . . . . . . . . . 218
7.3.10 Bit-state simulation with observer processes . . . . . . . . . . . . . . . . 220
7.4 Case Study with ObjectGeode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221
7.4.1 One second to detect missing save of v76frame . . . . . . . . . . . . . . 221
7.4.2 One second to detect missing input L ReleaseReq . . . . . . . . . . . . 225
7.4.3 One second to detect missing input L DataReq . . . . . . . . . . . . . . 227
7.4.4 Seventeen seconds to explore 87174 global states . . . . . . . . . . . . . 230
7.4.5 Add faults in block dataLink : detect output to Null . . . . . . . . . . . 235
7.4.6 Twenty-two seconds to detect missing save of L DataReq . . . . . . . 240
7.4.7 Eleven minutes to detect missing input L ReleaseReq
and answer DM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243
7.4.8 Eleven minutes, 2.8 million states, no error . . . . . . . . . . . . . . . . . 248
7.4.9 Exhaustive simulation with stop conditions . . . . . . . . . . . . . . . . . 250
7.4.10 Exhaustive simulation with MSC observers . . . . . . . . . . . . . . . . . 251
7.4.11 Exhaustive simulation with GOAL observers . . . . . . . . . . . . . . . . 253
7.5 Other Simulation Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 256
7.5.1 Tau SDL Suite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 256
7.5.2 ObjectGeode: supertrace . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 256
7.5.3 ObjectGeode: liveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 257
7.6 Strategy to Master Exhaustive Simulation . . . . . . . . . . . . . . . . . . . . . . . 262
7.6.1 Which simulation modes should be used . . . . . . . . . . . . . . . . . . . 262
7.6.2 If simulation never terminates . . . . . . . . . . . . . . . . . . . . . . . . . . 263
7.7 Errors Detectable by Exhaustive Simulation . . . . . . . . . . . . . . . . . . . . . . 264
7.7.1 Errors detected by Tau SDL Suite . . . . . . . . . . . . . . . . . . . . . . . 264
7.7.2 Errors detected by ObjectGeode . . . . . . . . . . . . . . . . . . . . . . . . 265
8 Other Simulator Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 267
8.1 Tau SDL Suite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 267
8.1.1 Writing in the Simulator trace . . . . . . . . . . . . . . . . . . . . . . . . . . 267
8.1.2 Calling external C code . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 267
8.1.3 Simulating ASN.1 data types . . . . . . . . . . . . . . . . . . . . . . . . . . 270
8.1.4 Adding buttons to the Simulator . . . . . . . . . . . . . . . . . . . . . . . . 270
8.1.5 Adding buttons to the Validator . . . . . . . . . . . . . . . . . . . . . . . . . 272
8.1.6 Setting breakpoints in the Simulator . . . . . . . . . . . . . . . . . . . . . . 272
8.1.7 Running several communicating Simulators . . . . . . . . . . . . . . . . . 273
8.1.8 Real-time simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 275
8.1.9 List of Validator options . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 275
8.2 ObjectGeode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 279
8.2.1 Writing in the Simulator trace . . . . . . . . . . . . . . . . . . . . . . . . . . 279
8.2.2 Calling external C code . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 279
8.2.3 Simulating ASN.1 data types . . . . . . . . . . . . . . . . . . . . . . . . . . 281
8.2.4 Adding buttons to the Simulator . . . . . . . . . . . . . . . . . . . . . . . . 281
8.2.5 Simulation scheduling like in Tau SDL Simulator and Validator . . . 282
8.2.6 List of Simulator settings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 284
Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 289
Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 293

opqrst

I am currently looking for this kind of books. Many thanks.

secant0711

thx for sharing

hongsail

Thanks！

vikingg

谢谢分享

pusher_yxg

Thanks a lot!!

lyd964201

kankan