Validation of Communications Systems with SDL provides a clear practical guide to validating, by simulation, a telecom system modelled in SDL. SDL, the Specification and Description Language standardised by the International Telecommunication Union (ITU-T), is used to specify and develop complex systems such as GSM, GPRS, UMTS, IEEE 802.11 or Hiperlan. Since the downturn in the telecom industry, validating a system before its implementation has become mandatory to reduce costs. This volume guides you step by step through the validation of a simplified protocol layer, from interactive simulation to proof of properties using reachability analysis combined with observers. Every step is explained, using the two main SDL tools commercially available: ObjectGeode™ and Tau SDL™ Suite, both from Telelogic. Contents: Short tutorial on SDL Presentation of the protocol layer case study Interactive simulation, MSC generation Scripting, automatic non-regression Auto matic validation against MSC, HMSC, etc. Random simulation Exhaustive and bit-state simulation Errors detected and not detected by simulation Other simulator features This book offers you the opportunity to: Learn expert validation techniques and tips Master advanced simulation features of Telelogic ObjectGeode™ and Tau SDL Suite™ Practice 156 hands-on exercises with solutions. The SDL models and scripts used in the exercises can be downloaded from the Web.

Table of 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 MSC117 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