oop corresponds to the livelock detected in depth mode, shown in Figure 7.75. The execution can continue forever, trapped between states s12 and s121, never reaching any success state. By loading the file maze.l1.scn into the Simulator and replaying it, the MSC trace shown in Figure 7.78 has been generated: this nonsuccess loop is shown in the left part of Figure 7.79. As for the previous nonsuccess loop, the execution can continue forever between states s11 and s112, never reaching any success state. But this nonsuccess loop had not been detected in Exhaustive Simulation 261 no_succ2 inst_1_proc1 proc1(1) entry enter Figure 7.77 The second nonsuccess loop detected no_succ1 inst_1_proc1 proc1(1) entry enter Figure 7.78 The first nonsuccess loop detected ENTRY input enter input enter non-success right loop 1 non-success output exit right loop 2 Figure 7.79 The two nonsuccess loops detected 262 Validation of Communications Systems with SDL depth mode because it does not correspond to any livelock: from s11 the system can exit from the loop. Examples of applications where liveness is helpful: for a communication protocol, to prove that any data transmitted are received, or if they were not transmitted the sender has been informed (this has been done with VEDA2, a tool based on the Estelle language, in [Doldi92]); for an aircraft or a car, to prove that several on-board systems always synchronize upon power-up or that the reconfiguration mechanism after a failure always works; this is very difficult to check manually because such systems are complicated by the requirement to remain operational after one (hard or soft) failure and safe after a second failure; as such systems especially in aircraft are safety-critical, a bug in the failure detection and recovery mechanisms could provoke a crash. 7.5.3.3 Application to V.76 If you simulate in liveness mode the V.76 SDL model observed by the MSC represented in Figure 7.80 (with the MSC Simulation property set to search), the simulator detects nonsuc- cess loops. inst_dlc