n the previous chapters, we have seen that the detection of SDL errors such as missing input (signal discarded) is automatically performed by the Simulators. However, we had to watch the simulation traces to check that the SDL model behaves as we expect. The present chapter shows how to formalize the expected behavior in order to automatically monitor the simulation to detect if the SDL model behaves correctly or not. The idea of automatic observation is not new; before being implemented in SDL tools, it was used in tools based on the Estelle language: VEDA [Jard88] and VESAR [Alga91]. As illustrated in Figure 5.1, the expected property of the system coming from its requirements is formalized into an observer. Then the SDL Simulator permanently monitors the simulation: when the behavior of the SDL model does not comply with the observer, the Simulator signals a violation of the property. If the simulated behavior complies with the observer, the Simulator signals that the property is satisfied. expected formalization observer property the property simulation is satisfied e. g. L_EstabConf or violated happens after SDL model L_EstabReq Figure 5.1 Automatic observation of simulations The observer is executed in parallel with the SDL model: one transition is executed in the SDL model, then the observer is executed, one SDL transition is executed, the observer is executed again and SO on. This is called on-the-fly verification, as there is no need to finish the computation, for example, of some reachable states graph to start running the verification. Figure 5.1 refers to an expected property: in such case, we hope that the simulation will prove that the property is satisfied. However, an observer can also represent an unwanted property (example: traffic lights are green at the same time in a crossroad), and we hope that Validation of Communications Systems with SDL: The Art of SDL Simulation and Reachability Analysis. Laurent Doldi © 2003 John Wiley & Sons, Ltd ISBN: 0-470-85286-0 112 Validation of Communications Sys