Validation of Communications Systems with SDL: The Art of SDL Simulation and Reachability Analysis

TeamLiB......Page 1
Cover......Page 2
Contents......Page 9
Preface......Page 13
Foreword......Page 15
1.1 Validation of Communications Systems......Page 17
1.2.1 Overview of SDL......Page 18
1.2.2 Bene.ts provided by SDL......Page 19
1.3 Simulation Life Cycle......Page 20
1.4 Contents of the Book......Page 22
1.5 Tools and Platforms Used......Page 23
2.1.1 System, block and process......Page 25
2.1.3 Process......Page 26
2.2.1 Signals......Page 27
2.3.1 Structure of a transition......Page 29
2.3.2 Start......Page 30
2.3.4 Input......Page 31
2.3.5 Save......Page 32
2.3.8 Task......Page 33
2.3.10 Output......Page 34
2.3.12 Timers......Page 35
2.4.1 Prede.ned data......Page 36
2.4.4 Newtype......Page 37
2.5.2 Types, instances and gates......Page 38
2.5.3 Specialization......Page 40
3.1 Presentation......Page 41
3.2.1 Abbreviations used......Page 42
3.2.3 Establishment of a data link connection......Page 43
3.3 Analysis MSCs for the V.76 Protocol......Page 44
3.4.2 The package V76......Page 46
3.4.3 The block dataLink......Page 51
4.1 Principles......Page 55
4.2.1 Prepare the Simulator......Page 56
4.2.2 Validate against the main scenarios......Page 60
4.2.3 Detect a bug in the SDL model......Page 66
4.2.4 Detect nonsimulated parts......Page 71
4.2.5 Validate against more scenarios......Page 74
4.2.6 Write a script for automatic validation......Page 78
4.2.7 Other Simulator features......Page 79
4.3 Case Study with ObjectGeode......Page 84
4.3.1 Prepare the Simulator......Page 85
4.3.2 Validate against the main scenarios......Page 91
4.3.3 Detect a bug in the SDL model......Page 95
4.3.4 Detect nonsimulated parts......Page 102
4.3.5 Validate against more scenarios......Page 104
4.3.6 Write a script for automatic validation......Page 109
4.3.7 Other Simulator features: watch, trace,.lter etc......Page 111
4.4.1 Dynamic errors detected by Tau SDL suite Simulator......Page 124
4.4.2 Dynamic errors detected by ObjectGeode SDL Simulator......Page 125
4.4.3 Dynamic errors not checked......Page 126
5.1.1 Automatic checking of model properties......Page 127
5.1.2 Speci.city of observation with MSCs in Tau SDL Suite......Page 129
5.2.1 Simulate with user-de.ned rules......Page 130
5.2.2 Simulate with a basic MSC......Page 133
5.2.3 Simulate with an MSC containing inline operators......Page 135
5.2.4 Simulate with an HMSC......Page 137
5.2.5 More details on MSCs......Page 143
5.2.6 Simulate with observer processes......Page 148
5.2.7 More details on observer processes......Page 150
5.3.1 Simulate with stop conditions......Page 152
5.3.2 Simulate with a basic MSC......Page 155
5.3.3 Simulate with a hierarchical MSC......Page 158
5.3.4 More details on MSCs......Page 165
5.3.5 Simulate with GOAL observers......Page 175
5.3.6 More details on GOAL observers......Page 177
6.2.1 Random simulation without observers......Page 183
6.2.2 Multiple random simulations......Page 185
6.2.3 Random simulation with observers......Page 186
6.3.1 Random simulation without observers......Page 188
6.3.2 Multiple random simulations......Page 190
6.3.3 Random simulation with observers......Page 191
6.3.4 Details on random simulation......Page 195
6.4 Errors Detectable by Random Simulation......Page 196
7.1.1 Exhaustive simulation......Page 197
7.1.3 On-the-.y validation......Page 200
7.2.1 Exhaustive simulation of the ping TCP/IP command......Page 201
7.2.2 Exhaustive simulation of counters......Page 206
7.3 Case Study with Tau SDL Suite......Page 207
7.3.1 One second to detect missing save of v76frame......Page 208
7.3.2 One second to detect missing input L ReleaseReq......Page 213
7.3.3 One second to detect missing input L DataReq......Page 215
7.3.4 Millions of states: detect output to Null......Page 218
7.3.5 Forty seconds to detect missing save of L DataReq......Page 222
7.3.6 Two minutes to detect missing input L ReleaseReq and answer DM......Page 226
7.3.7 Three minutes, 6.7 million states, no error......Page 230
7.3.8 Bit-state simulation with a user-de.ned rule......Page 233
7.3.9 Verifying an MSC with bit-state simulation......Page 234
7.3.10 Bit-state simulation with observer processes......Page 236
7.4.1 One second to detect missing save of v76frame......Page 237
7.4.2 One second to detect missing input L ReleaseReq......Page 241
7.4.3 One second to detect missing input L DataReq......Page 243
7.4.4 Seventeen seconds to explore 87174 global states......Page 246
7.4.5 Add faults in block dataLink : detect output to Null......Page 251
7.4.6 Twenty-two seconds to detect missing save of L DataReq......Page 256
7.4.7 Eleven minutes to detect missing input L ReleaseReq and answer DM......Page 259
7.4.8 Eleven minutes, 2.8 million states, no error......Page 264
7.4.9 Exhaustive simulation with stop conditions......Page 266
7.4.10 Exhaustive simulation with MSC observers......Page 267
7.4.11 Exhaustive simulation with GOAL observers......Page 269
7.5.2 ObjectGeode: supertrace......Page 272
7.5.3 ObjectGeode: liveness......Page 273
7.6.1 Which simulation modes should be used......Page 278
7.6.2 If simulation never terminates......Page 279
7.7.1 Errors detected by Tau SDL Suite......Page 280
7.7.2 Errors detected by ObjectGeode......Page 281
8.1.2 Calling external C code......Page 283
8.1.4 Adding buttons to the Simulator......Page 286
8.1.6 Setting breakpoints in the Simulator......Page 288
8.1.7 Running several communicating Simulators......Page 289
8.1.9 List of Validator options......Page 291
8.2.2 Calling external C code......Page 295
8.2.4 Adding buttons to the Simulator......Page 297
8.2.5 Simulation scheduling like in Tau SDL Simulator and Validator......Page 298
8.2.6 List of Simulator settings......Page 300
Bibliography......Page 305
Index......Page 309