 all the reachable states of the SDL model have been explored, the simulation is fin- ished: the SDL model correctness has been formally proved (according to the configura- tion used). Otherwise, because the large number of global states prevents exploring them, the model configuration must be reduced, for example, by allowing one or two signals only per pro- cess input queue, limiting the exploration depth and SO on. If the configuration cannot be reduced, the simulation is finished, and the validation is partial because some global states remain unexplored. The simulator also detects SDL symbols never simulated: they indicate SDL transitions or branches that could be removed, or reveal missing test signals or test values to be transmitted to the SDL model by the simulator. All these steps are detailed in the book, illustrated by numerous hands-on exercises. 1.4 CONTENTS OF THE BOOK This book is divided into eight chapters. Chapter 1 is the present introduction. Chapter 2 is a quick tutorial on SDL-92, the language used for the exercises in the rest of the book. Chapter 3 contains the simplified version of the V.76 protocol specification, some analysis MSCs and the corresponding SDL model used during the simulation exercises. Chapter 4 explains how to validate the V.76 SDL model using interactive simulation. Chapter 5 introduces observers, what they can detect, how to build them and how to use them during interactive simulation. Chapter 6 describes random simulation. Chapter 7 presents exhaustive simulation, how to use it with observers and other simulation algorithms such as bit-state or liveness. Chapter 8 illustrates other simulator features such as calling external C code or adding buttons to the simulators. Introduction 7 Each chapter contains hands-on exercises with solutions for the two main SDL tools com- mercially available: ObjectGeode and Tau SDL Suite, both from Telelogic. 1.5 TOOLS AND PLATFORMS USED The exercises of the book have been developed using the following commercial off-the-shelf tools, bo