![]() |
![]() |
![]() |
![]() |
![]() |
Using Observer Processes
The purpose of an observer process is to make it possible to check more complex requirements on the SDL system than can be expressed using MSCs. The basic idea is to use SDL processes (called observer processes) to describe the requirements that is to be tested and then include these processes in the SDL system. Typical application areas include feature interaction analysis and safety-critical systems.
To be useful, the observer processes must be able to inspect the SDL system without interfering with it and also generate reports that convey the success or failure of whatever they are checking.
To accomplish this, three features are included in the Explorer:
- The observer process mechanism.
- The assert mechanism.
- The assert mechanism enables the observer processes to generate reports during state space exploration. These reports will show up in the list of generated reports in the Report Viewer. The details of the assertion mechanism is discussed in Using Assertions.
- The Access abstract data type.
- The purpose of the Access abstract data type is to give the observer processes a possibility to examine the internal states of the other processes in the system. Using the Access ADT it is possible to check variable values, contents of queues, etc., without any need to modify the observed processes. See The Access Abstract Data Type for more details.
A simple observer process is illustrated in Figure 490.
This process will check if the variable Counter in the Initiator process ever becomes equal to 2.
Two characteristics for the observer processes are:
- the use of continuous signals with tests that use Access operator to check the internal state of other processes, and
- the use of assertions to report the result.
- Create the observer processes in the SDL Editor. You should place the observer processes in a special block that you include in the diagram structure of the SDL system. In this block, you also need to specify an INCLUDE directive for the Access ADT:
/*#INCLUDE `access.pr' */- In the generated explorer, define each observer process by using the command Define-Observer, followed by the name of the process type. All instances of the process type will now become observer processes.
- Perform a state space exploration. If an assertion defined in an observer process is satisfied, an "Assertion" report is generated. To simplify the observer processes, an "Observer" report will also be generated whenever there is an observer process that cannot execute.
In some cases the Observer reports are not convenient and they can then be turned off with the Define-Report-Continue (that will cause the exploration to continue past a reported situation) and the Define-Report-Log command (that can be used to turn off the logging a s specific report type, e.g. Observer reports)
The Access Abstract Data Type
The Access abstract data type is an ADT intended to be used together with observer processes to make it possible to access the internal state of other processes from an observer process. The ADT is defined in the file access.pr that resides in the ADT directory together with the rest of the ADTs supplied together with the SDL Suite. Unlike the rest of the ADTs the Access ADT is a special purpose ADT that only works with the Explorer kernel.
The Access ADT defines a number of SDL operators. The signatures of these operators are defined as follows:
GetPID : CharString, integer -> PId;/* Returns the PId value of a process instancepar 1: the name of the process typepar 2: instance number of the process instance*/ActivePID : integer -> PId;/* Return the PId of the process that executes.Returns NULL if no process executes.Observer processes are not taken into account.The integer parameter is a dummy parameterneeded since operators must have parameters. */GetState : PId -> CharString;/* Returns the name of the current state of aprocess instance (or previous if the processis not in a state)par 1: the pid of the process instance */GetNoOfInst: charstring -> integer;/* Returns the number of instances for aparticular process typepar 1: the name of the process type */terminated: PId -> boolean;/* Returns true if the process instance isterminated otherwise falsepar 1: The PId value of the process instance */GetProcedure: PId -> charstring;/* Returns the name of the procecure a processinstance currently has called. If no procedureis called `none' is returnedpar 1: The PId value of the process instance */InProcedure: PId, CharString -> boolean;/* Returns true if a process instance currentlyexecutes in a specific procedure, otherwisefalsepar 1: The PId value of the process instancepar 2: The name of the procedure */GetNoOfSignals: PID -> integer;/* Returns the number of signals currently in theinput port of a process.par 1: The PId value of the process instance */GetSignalType: PId, integer -> charstring;/* Returns the name of the signal type for asignal in the input port of a process instancepar 1: The PId value of the process instance.par 2: A number (>=1) identifying the signal */InQueue: PId, charstring -> boolean;/* Returns true if a process instance currentlyhas a signal of a specific type in its inputport queuepar 1: The PId value of the process instance.par 2: The name of the signal type. *//* Variable access functions. These functions returna variable value that corresponds to one of thevariables of a process instance as specified bythe parameters.par 1: The PId value of the process instance.par 2: Variable name */v : PId, charstring -> integer;vInteger : PId, charstring -> integer;v : PId, charstring -> real;vReal : PId, charstring -> real;v : PId, charstring -> boolean;vBoolean : PId, charstring -> boolean;v : PId, charstring -> Character;vCharacter : PId, charstring -> Character;v : PId, charstring -> Time;vTime : PId, charstring -> Time;v : PId, charstring -> Duration;vDuration : PId, charstring -> Duration;v : PId, charstring -> Charstring;vCharstring : PId, charstring -> Charstring;v : PId, charstring -> PId;vPId : PId, charstring -> PId;EnvOutput : CharString -> Boolean;/* Returns true if the transition currentlyexecuting is caused by a signal from theenvironment with a specified name, otherwisefalsepar 1: The name of the signal type */The Access ADT also includes a utility procedure called Report that if called from an observer process will generate an Assertion report in the explorer. The procedure takes a charstring as parameter and this is the string that will be presented in the Assertion report.
An example of the usage of some of the operators is:
P := GetPId( `Initiator', 1 ),CS := GetState( P )This example assigns the PId value of the first Initiator process to the PId variable P, and then assigns the name of the state of this process to the charstring variable CS.
An example of a statement that will access the variable value for one of the variables of another process instance is:
LocalVar := v(P,'Var')In this example we assume that we have a PId variable P that identifies a process that has a variable Var of type for which a v operator is defined. The statement will access the value of Var and assign it to the local variable LocalVar.
The operators for accessing the value of a variable are given in two versions for each predefined simple type: the v operator and the vXXX operator, where XXX is the name of the type. They are equivalent and the only time there is a need to use the vXXX operator is when it is not possible to resolve by context which of the v operators that is intended.
To access variables of sorts that are syntypes to the predefined simple types, the v operator for the corresponding predefined simple type can be used.
Accessing variable of structured types, enumeration types and user-defined types is a bit more complex. There are two possible ways to do it. Either define the v operator for the type in question, or use the #CODE operator and access the variable value using a C macro XVV.
Example 344 : Structured Types in Observer Processes
Consider the following structure definition:
newtype MSDUTypestructid IPDUType;num Sequencenumber;data ISDUType;endnewtype MSDUType;A v operator for this type can be defined as:
newtype MSDUTypeAccessliterals NotUsedMSDUTypeAccess;operatorsv /*#NAME 'XVNAME(MSDUType)'*/ :PId, charstring -> MSDUType;/*#ADT (H)#TYPE#define MSDUType #SDL(MSDUType)*/endnewtype MSDUTypeAccess;Once this definition is in place, variable values for the complex data type can conveniently be accessed using the new v operator. Note also that it is possible to access the values of the fields of the structure in a simple way:
LocalVar := v(P,'MSDUVar')!idIf the type is one of the types passed as values, according to the table in Parameter Passing to Operators, XVNAME should be substituted to XVNAME2.
However, if the values of the complex type only is accessed in a few places, it is possible to access them directly using the #CODE operator as illustrated in the following example:
LocalVar := #CODE(`XVV(#SDL(P),"Var",#SDL(MyType))')In this example we assume that we have a PId variable P that identifies a process that has a variable Var of type MyType. The statement will access the value of Var and assign it to the local variable LocalVar.
http://www.ibm.com/rational |
![]() |
![]() |
![]() |
![]() |