tems with SDL the simulation will prove that this property cannot be satisfied. More details are provided in Chapter 7. Table 5.1 shows the observation formalisms that can be used in our two SDL tools. In this book, we call all these formalisms 'observers', but in fact, the name observer, in the tools documentation, is only used for the MSCs or GOAL¹ observers in ObjectGeode and the observer processes in Tau SDL Suite. Table 5.1 Observation formalisms available in the two SDL tools Kind of property Formalization ObjectGeode Simulator Tau SDL Validator* Expression on current stop conditions rules model state Linear signal sequencing basic MSCs basic MSCs Complex signal sequencing medium hierarchical MSCs MSCs with inline (i.e. with operators) operators HMSCs (High-Level MSCs) All the above plus medium GOAL observers observer processes memorization and more *The Simulator can also be used to observe an SDL model with an MSC, using the Organizer command Simulator Test > New Simulator. Examples of observers: stop condition (ObjectGeode): detects that instance 1 of process DLC in blocks DLCa and DLCb are in state connected; stop if (DLCa!DLC (1) !state = connected) and \ (DLCb!DLC (1) state = connected) MSC (Tau and ObjectGeode), shown in Figure 5.2: checks that in the simulated SDL model, an input of signal L_EstabReq(0) by block DLCa is followed by the output of signal L_EstabConf(0) from the same block. Note that in Tau, exchanges of other signals are considered as a violation, as opposed to that in ObjectGeode. There is no way to memorize the parameter value, thus there must be one MSC per value of parameters (one for 0, one for 1 etc.), or the parameter values must be ignored. MSC obs_ex1 env_0 inst_dlca lestabreq( 0) I_estabconf( 0) Figure 5.2 Example of observer MSC 1 Geode Observation Automata Language. Automatic Observation of Simulations 113 GOAL observer (ObjectGeode), shown in Figure 5.3, or observer process (Tau): behavior similar to the observer MSC in Figure 5.2, plus memorization of the value of the pa