-state simulation with a user-defined rule X Contents 7.3.9 Verifying an MSC with bit-state simulation 7.3.10 Bit-state simulation with observer processes 7.4 Case Study with ObjectGeode 7.4.1 One second to detect missing save of v76frame 7.4.2 One second to detect missing input :L_ReleaseReq 7.4.3 One second to detect missing input L_DataReq 7.4.4 Seventeen seconds to explore 87174 global states 7.4.5 Add faults in block dataLink : detect output to Null 7.4.6 Twenty-two seconds to detect missing save of L_DataReq 7.4.7 Eleven minutes to detect missing input L _ReleaseReq and answer DM 7.4.8 Eleven minutes, 2.8 million states, no error 7.4.9 Exhaustive simulation with stop conditions 7.4.10 Exhaustive simulation with MSC observers 7.4.11 Exhaustive simulation with GOAL observers 7.5 Other Simulation Algorithms 7.5.1 Tau SDL Suite 7.5.2 ObjectGeode: supertrace 7.5.3 ObjectGeode: liveness 7.6 Strategy to Master Exhaustive Simulation 7.6.1 Which simulation modes should be used 7.6.2 If simulation never terminates 7.7 Errors Detectable by Exhaustive Simulation 7.7.1 Errors detected by Tau SDL Suite 7.7.2 Errors detected by ObjectGeode 8 Other Simulator Features 8.1 Tau SDL Suite 8.1.1 Writing in the Simulator trace 8.1.2 Calling external C code 8.1.3 Simulating ASN.1 data types 8.1.4 Adding buttons to the Simulator 8.1.5 Adding buttons to the Validator 8.1.6 Setting breakpoints in the Simulator 8.1.7 Running several communicating Simulators 8.1.8 Real-time simulation 8.1.9 List of Validator options 8.2 ObjectGeode 8.2.1 Writing in the Simulator trace 8.2.2 Calling external C code 8.2.3 Simulating ASN.1 data types 8.2.4 Adding buttons to the Simulator 8.2.5 Simulation scheduling like in Tau SDL Simulator and Validator 8.2.6 List of Simulator settings Bibliography Index Preface This book is the second in a series; after a first book explaining SDL (Specification and Description Language) and about how to build an SDL model [Doldi01], this book explains how to validate the model by simulation. The two books share the sa