[I2 logo] [RWTH logo] MOVES: Software Modeling and Verification
(Informatik 2)
Computer Science / RWTH / I2 / Research / AG / MCS / SDL / Internal / Eval-sdl2xta
Printer-friendly
Evaluation of SDL2XTA

Evaluation of the sdl2xta tool by a simple example

Tooling employed

This evaluation was done using:
  • UPPAAL 3.2.13, the output generated by sdl2xta leads to syntactical errors using later versions of UPPAAL
  • sdl2xta build from May 2004 (Fedora)

The Example

As Example we took a very simple SDL system: A spec called Test holds a Block B which holds two processes A and B again.
Overview of SDL specification
The two processes are connected via a channel, that only carries one message. Thus the state space is considerably small.
The two connected processes
The only actions that take place in the system are sending a message from A...
States of A
...as well as the reception of this message by B:
States of B

SDL/PR representation

We used Telelogic SDT in order to model the system above and to generate the resulting SDL/PR code:
system Test;
block B referenced;
endsystem Test;

block B;
signal
sig;
signalroute chan
from A to B with sig;
process A referenced;
process B referenced;
endblock B;

process A;

start;
output sig;
nextstate -;
endprocess A;

process B;

start;
nextstate Stat;

state Stat;
input sig;
nextstate -;
endstate;
endprocess B;

Conversion to xta using sdl2xta

We employed the tool sdl2xta in order to convert the PR representation. We recieved this console output as well as this XTA output file.

The resulting UPPAAL model

First of all, sdl2xta generated a minor syntactical error for the given system:
A decleration and instantiation of a Timer process was generated, however a Timer process template was not (presumably because we did not use any timers at all). This could simply be fixed by deleting the appropriate two lines.

During conversion from SDL to XTA sdl2xta loses all formatting information. Note that Telelogic SDT is able to annotate the SDL/PR code with comments which hold formatting information in order to rebuild the visualization from those files. However, sdl2xta does not make use of this property. Thus the resulting UPPAAL processes look much more complex than they actually are:
UPPAAL model without formatting
This screenshot should make clear that a manual step of arrangement is inevitable before one could proceed with the actual analysis. However, even when arranged in an appropriate way, the model easily becomes quite huge and so hard to follow during simulation:
Simulation
However, it is possible to hide some of the helper processes to get a better overview:
Simulator with deactivated helper processes

Mapping between SDL and XTA

This analysis however, becomes rather complicated, too, since for every single state in the SDL spec, one obtains several ones in the UPPAAL model. Also those states are differently labeled and surrounded by various helper states. Apart from that, sdl2xta generates a runtime system that simulates message queues and process dispatching. Details on that can be found in Hessel's thesis.
Anyway, if one manages to still interpret and evaluate the model after all, from what we saw during our tests, the actual model checking seems to work appropriately:
Output of the model checker

The picture above shows the following situation: We have converted the model  to XTA, loaded this into UPPAAL and now want to check the property "Is there a chance that process B ever recieves a message from A?". As you can see, this is not straightforward to model in the UPPAAL query language - especially under the model generated by sdl2xta: The E<> part is as expected. B however has to be adresses by it's (first and only) instance B_2_0. Also one has to manually derive from the model that nextstate2 is the first state  reached, after B receives the message from A. This manual step might still be doable in such small models. In industry-sized systems however this might cause quite some trouble and is also quite errorprone.

Conclusion

The tool sdl2xta gives a good first approach to model checking of SDL. It is capable of translation of a subset of SDL (see thesis), which might be an appropriate choice for what parts of SDL are automatedly verifiable at all. However, the implementation suffers from two big drawbacks:
  • The generated models are poorly layouted. A manual step of arrangement is necessary if one wants to employ the simulator. This step can employ a lot of time for industry-sized systems.
  • It is a hard, manual job to identify SDL states in the UPPAAL model. Thus the translation of requirements for the SDL spec to requirements for the UPPAAL model is everything else but straightforward. Last but not least it also mitigates one's confidence in this semi-automated approach, which is a disadvantage that is not to underestimate.
Valid HTML 4.01 Strict! Valid CSS!