Extending the Translation from SDL to Promela

This paper tackles the problem of model-checking SDL programs that use the save operator. Previous work on model-checking SDL programs with SPIN consisted in translating SDL into IF (using sdl2if) and finally IF to Promela (if2pml). However, the save operator of SDL is not handled by the (final) translator if2pml. We propose an extension of the if 2pml tool that translates IF into Promela programs with save operators. We also add an abstraction method on buffer messages to if2pml allowing the user to gather some buffer messages into one abstract value. We use our extended version of if2pml to validate an Unmanned Underwater Vehicle (UUV) subsystem specified with SDL.