|Michael Weber||Disclaimer||Last modified: 2004-06-08 13:41 UTC|
MOVES: Software Modeling and Verification
|Computer Science / RWTH / I2 / Research / AG / MCS / SDL / Internal / Eval-sdl2xta|
Evaluation of the sdl2xta tool by a simple example
Tooling employedThis evaluation was done using:
The ExampleAs Example we took a very simple SDL system: A spec called Test holds a Block B which holds two processes A and B again.
The two processes are connected via a channel, that only carries one message. Thus the state space is considerably small.
The only actions that take place in the system are sending a message from A...
...as well as the reception of this message by B:
SDL/PR representationWe used Telelogic SDT in order to model the system above and to generate the resulting SDL/PR code:
Conversion to xta using sdl2xtaWe 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 modelFirst 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:
However, it is possible to hide some of the helper processes to get a better overview:
Mapping between SDL and XTAThis 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.
ConclusionThe 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: