@inproceedings{85ab2df01dee43989e48692337cc0d88,
title = "A transformation of SDL specifications : a step towards the verification",
abstract = "Industrial-size specifications/models (whose state space is often infinite) can not be model checked in a direct way— a verification model of a system is model checked instead. Program transformation is a way to build a finite-state verification model that can be submitted to a model checker. Abstraction is another technique that can be used for the same purpose. This paper presents a transformation of SDL timers aimed at the reduction of the infinite domain of timer values to a finite one with preserving the behaviour of a system. A timer abstraction is proposed to further reduce the state space. We discuss the ideas behind these transformations and argue their correctness.",
author = "N. Ioustinova and N. Sidorova",
year = "2001",
doi = "10.1007/3-540-45575-2_9",
language = "English",
isbn = "3-540-43075-X",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "64--78",
editor = "D. Bjorner and M. Broy and A. Zamulin",
booktitle = "Perspectives of System Informatics (4th International Andrei Ershov Memorial Conference, PSI 2001 Akademgorodok, Novosibirsk, Russia, July 2–6, 2001. Revised Papers)",
address = "Germany",
note = "conference; 4th International Andrei Ershov Memorial Conference ; Conference date: 01-01-2001",
}