@inproceedings{8eb0f843eab24f28b0b899e158c97c56,
title = "Extending the translation from SDL to promela",
abstract = "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 if2pml 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.",
keywords = "Data abstraction, Model-checking, Save operator, SDL formalism",
author = "Armelle Prigent and Franck Cassez and Philippe Dhaussy and Olivier Roux",
year = "2002",
language = "English",
isbn = "3540434771",
volume = "2318 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer, Springer Nature",
pages = "79--94",
editor = "Dragan Bo{\v s}na{\v c}ki and Stefan Leue",
booktitle = "Model Checking Software - 9th International SPIN Workshop, Proceedings",
address = "United States",
note = "9th International SPIN Workshop on Model Checking Software, SPIN 2002 ; Conference date: 11-04-2002 Through 13-04-2002",
}