Evaluation of the sdl2xta tool by a simple example

...as well as the reception of this message by 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:
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:

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:
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.