next up previous

Final Report of the COST-247 Action

State Space Reduction of SDL with Partial-Order Methods

Alper Sen

TUBITAK Software R&D Center
Department of Electrical and Electronics Engineering,
Middle East Technical University,
Ankara, Turkey


State space generated during verification of protocols is usually so large that most of the time because of memory limitations verification is not completed. This problem is also known as the state-explosion problem. I worked on partial-order methods which make use of the modelling of concurrency by interleaving. We developed methods specifically for SDL systems one of which is read-first strategy saying that whenever an SDL process is at an input state then generate the exploration tree by expanding only this transition. This in fact leads to a great amount of reduction. Results for the effect of the methods have been illustrated by a new verification tool POVSDL. It has also been observed that POVSDL performs always better than commercial verifiers.

This presentation has been given during the COST-247 9th Management Committee Meeting (Antalya, Turkey, November 4--5, 1996).

COST-247 Working Group(s): 2

Web links :

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page