Abstract:

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.