![]() |
![]() |
![]() |
![]() |
![]() |
Verifying an MSC
MSC verification is one the major application areas for the SDL Explorer. This section describes how to use the Explorer to get started with MSC verification. It also gives some ideas of how to organize MSCs to be able to use common initialization MSCs and shows how to use batch files to achieve an efficient regression testing of an SDL system using MSC verification.
The first prerequisite for MSC verification is of course that we have an MSC that describes some desirable behavior that can be used to check the SDL system against. This MSC can be interactively created using the MSC Editor as part of a requirement analysis, but it is also possible to use MSCs created as execution traces in the SDL Simulator or the Explorer itself as input to the MSC verification.
It is worth noticing that the MSC does not have to be a process level MSC. It is possible to use MSCs where the MSC instances correspond to SDL blocks and systems, and even mixed MSCs where some instances correspond to processes and other to blocks.
There are some requirements on MSCs to be used for MSC verification; see Requirements for MSC Verification.
The characteristics of the MSC verification algorithm is further described in MSC Verification Options.
Basic MSC Verification
To verify an MSC for a system opened in the Explorer:
- If necessary, go to a system state that corresponds to the start of the MSC to verify. If the MSC describes events from the start of the system, go to the system start state. You may have to reset the explorer first, especially if you already have an MSC loaded.
- To start the MSC Verification, click the Verify MSC button in the Explore module, or enter the command Verify-MSC.
- The MSC that you want to verify has to be specified. Either select it in the File Selection Dialog that appears (in graphical mode), or enter the name of the file on the command line (in stand-alone mode).
Note: Illegal characters in path name
Please note that verifying an MSC fails if the path name of the MSC contains "(" or ")".
- A bit state exploration adapted to suit MSC verification is performed. After the exploration statistics, the result of the MSC verification is presented. If it was possible to find an execution trace that was consistent with the MSC, the text
** MSC <MSC name> verified **
- is printed, where <MSC name> is the name of the MSC that was checked. If it was not possible to find a consistent execution trace, the following text is printed:
** MSC <MSC name> NOT VERIFIED **- If the MSC was not verified, check the generated reports using the Report Viewer. There will be a number of "MSCViolation" reports. These reports identify the execution paths which violate the MSC, i.e., paths that contain events that are not part of the MSC. You may investigate these reports by using the method described in Examining Reports.
- If the MSC was successfully verified, there will be a
"MSCVerification" report (there may also be a number of
"MSCViolation" reports, but they can be discarded). You do not have to go to this report; the Explorer automatically goes to the state where the MSC was verified. This means that the current path is set up automatically.- To verify another MSC from the same start state, go to the top of the current path. It is now possible to directly start a new MSC verification, as described above (you do not have to reset the explorer).
When MSC verification is started, the current root of the behavior tree is redefined to the current state. This feature is used in the next section, Verifying a Combination of MSCs Using High-Level MSCs. (It also means that you may have to reset the explorer to be able to reach the system start state again.)
Converting Instances Before Verification
Before an MSC is loaded into the Explorer for verification, it is possible to perform instance conversion of the MSC. Instance conversion will convert the name of an instance to another name.
This is useful if you want to verify some, but not all, instances in an MSC with an SDL system. For instance, you may have an MSC describing a complete system but an SDL system for only a part of the system. In this case, you can convert the not wanted instances to be considered as environment in the Explorer, without changing the MSC.
Note that if you have more than one instance representing the environment, the environment instances must be separated using channel names.
Instance conversion is performed before an MSC is loaded into the Explorer by entering the command "Define-Instance-Conversion FromString ToString" for each instance name to be converted. All instance conversions can be listed by entering the command List-Instance-Conversion, and all instance conversion can be cleared by entering the command Clear-Instance-Conversion.
Consider an MSC with three process instances A, B and C. The SDL system specifies the behavior for instance A, but not for B or C. Before verifying the MSC, B can be converted to "channelB" and C to "channelC", where channelB is the existing SDL channel that will be used for communication between the existing A process and the non-existing process B, and channelC is the existing SDL channel that will be used for communication between the existing A process and the non-existing process C.
This is accomplished by entering the Explorer commands:
Define-Instance-Conversion B "channelB"Define-Instance-Conversion C "channelC"Verifying a Combination of MSCs Using High-Level MSCs
The high-level MSC that are available in MSC'96 provide a very convenient possibility to describe how many small MSCs are combined to form a larger use case or scenario. The Explorer support verification of high-level MSCs.
As an example, consider a situation where we have an MSC "init" that will describe some initialization phase that is needed to set up the SDL system to some "connected" state from where two features are accessible. These features are described by the MSCs "datatrans" and "finish". If this would be a communication protocol, the "init" might be a connection establishment, and "datatrans" and "finish" successful data transfer and connection release. This situation could be described using the high-level MSC in Figure 489.
To check this combination of MSCs simply verify the "inres1" high-level MSC and the explorer will generate one MSC verification report for each sequence of "leaf MSCs" that can be verified. In this case there will be reports for "init, finish", "init, datatrans, finish", "init, datatrans, datatrans, finish", etc. until the max depth for MSC verification has been reached.
State of the SDL Explorer after MSC Verification
When an MSC verification has been done, the current state of the explorer is different depending on how many MSC verification reports has been found:
- If 0 or more than 1 MSC verification report has been generated the current state of the explorer is the system state where the MSC verification was started from.
- If exactly 1 MSC verification report was generated the current state is the state where this report was found.
This is in many cases useful when using MSCs to navigate to a specific system state, especially in combination with command scripts as described in the next section. Note that if the MSC that is verified is an "old style" MSC without high-level MSCs or MSC reference expressions then there will always be at most one MSC verification report and this type of MSCs is thus best when using MSCs for navigation.
Using Batch MSC Verification
An efficient test strategy when incrementally developing SDL systems is to use regression testing. A set of MSCs describe the requirements on the SDL system and new MSCs are incrementally added to the set when new features are implemented in the SDL system. Each time a new feature is implemented the resulting system should be tested against all the old MSCs as well as the new ones, to make sure that no new errors have been introduced.
To accomplish this using the Explorer the most efficient way is to use the command script facility in the Explorer. A command script is simply a text file containing a number of Explorer commands, usually one command per line. A command file can be loaded into the Explorer by selecting Include Command Script from the Tools menu, or by entering the command Include-File.
Example 343 : Batch MSC Verification
A command script that when loaded will perform MSC verification for some requirements described as MSCs may look like:
log-on msc.logverify-msc inres1.mrmresetverify-msc init2.mscverify-msc inres2.mrmquitThe command Log-On is used to store the output from the verification on the file msc.log.
Note in Example 343 how the MSC init2 was used to set up the start state for the verification of the high-level MSC inres2.
Verifying Message Parameters
When verifying an MSC, the parameters of the messages in the MSC can sometimes be crucial and need to be verified, and sometimes be unimportant for the behavior in question. To support this, the verification of MSCs in the Explorer allows three different levels of matching of message parameters:
- No parameters are given for the message.
- Only some of the parameters are given.
- All of the parameters are given.
If no parameters are given, all possible actual parameters are accepted. If the signal is sent from the environment to the system, the parameter values that are defined using the test value facility are used by the Explorer when exploring the state space of the system.
When only some of the parameters are to be given, only the given parameters are checked during the exploration. The notation used to show that a specific parameter should be ignored during the verification is to simply leave out this parameter in the parameter list. For example, if only the second and fifth parameter should be used during the verification the parameter list would be ",2,,,true" in the MSC. Trailing commas can be left out, so if a signal has five parameters and only the first two are to be verified, the parameter list might be "1,2" which would ignore the last three parameters.
When only some of the parameters are given for a signal from the environment, the rest of the parameters are taken from the test value definitions when executing the signal output during state space exploration.
If all parameters are given, they are of course all checked.
Requirements for MSC Verification
The MSCs that can be loaded into the Explorer must comply with the following rules:
- It must be possible to map each MSC instance to either the environment, a channel to/from the environment, the entire SDL system, a block, or a process. This mapping is done by matching the name of the MSC instance with the names of the corresponding SDL entities. However, the name of an MSC instance can be changed before verification, see Converting Instances Before Verification.
- PId values are not allowed as parameters to MSC messages from the environment of the SDL system. PId values are allowed on internal messages and messages to the environment, but the values are not checked during the exploration.
- If the MSC is on process level, only one static instance of each process type is allowed in the MSC. There is no limit to the number of dynamically created MSC instances.
- Only the following events/symbols are interpreted in an old-style MSC. All other events are ignored or will not be accepted by the Explorer.
Conditions are interpreted as a synchronization point if Define-Condition-Check is set to "on", otherwise they are ignored. For more information, see Synchronizing Test Events with Conditions. Set, reset and timeout events on MSC instances representing SDL channels to the environment are only accepted by the Autolink test generation commands Generate-Test-Case and Translate-MSC-Into-Test-Case. For all other Explorer commands which load an MSC, timer events on environment instances are ignored and the Explorer generates a warning.
http://www.ibm.com/rational |
![]() |
![]() |
![]() |
![]() |