or automatic validation 4.3.7 Other Simulator features: watch, trace, filter etc Errors Detectable by Interactive Simulation 4.4.1 Dynamic errors detected by Tau SDL suite Simulator 4.4.2 Dynamic errors detected by ObjectGeode SDL Simulator 4.4.3 Dynamic errors not checked 5 Automatic Observation of Simulations 5.1 Principles Contents ix 5.1.1 Automatic checking of model properties 5.1.2 Specificity of observation with MSCs in Tau SDL Suite 5.2 Case study with Tau SDL Suite 5.2.1 Simulate with user-defined rules 5.2.2 Simulate with a basic MSC 5.2.3 Simulate with an MSC containing inline operators 5.2.4 Simulate with an HMSC 5.2.5 More details on MSCs 5.2.6 Simulate with observer processes 5.2.7 More details on observer processes 5.3 Case Study with ObjectGeode 5.3.1 Simulate with stop conditions 5.3.2 Simulate with a basic MSC 5.3.3 Simulate with a hierarchical MSC 5.3.4 More details on MSCs 5.3.5 Simulate with GOAL observers 5.3.6 More details on GOAL observers 6 Random Simulation 6.1 Principles 6.2 Case Study with Tau SDL Suite 6.2.1 Random simulation without observers 6.2.2 Multiple random simulations 6.2.3 Random simulation with observers 6.3 Case Study with ObjectGeode 6.3.1 Random simulation without observers 6.3.2 Multiple random simulations 6.3.3 Random simulation with observers 6.3.4 Details on random simulation 6.4 Errors Detectable by Random Simulation 7 Exhaustive Simulation 7.1 Introduction 7.1.1 Exhaustive simulation 7.1.2 Bit-state simulation 7.1.3 On-the-fly validation 7.2 Simple Examples 7.2.1 Exhaustive simulation of the ping TCP/IP command 7.2.2 Exhaustive simulation of counters 7.3 Case Study with Tau SDL Suite 7.3.1 One second to detect missing save of v76frame 7.3.2 One second to detect missing input L_ReleaseReq 7.3.3 One second to detect missing input _DataReq 7.3.4 Millions of states: detect output to Null 7.3.5 Forty seconds to detect missing save of L_DataReq 7.3.6 Two minutes to detect missing input L_ReleaseReq and answer DM 7.3.7 Three minutes, 6.7 million states, no error 7.3.8 Bit