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.
|Name||Lecture Notes in Computer Science|
|Conference||conference; 4th International Andrei Ershov Memorial Conference|
|Period||1/01/01 → …|
|Other||4th International Andrei Ershov Memorial Conference|