Towards compositional verification of SDL systems

In this paper; a new method for proving qualitative properties of SDL-systems is presented, which is based on a compositional high-level Petri net semantics for SDL. Since emphasis is laid on the modelling of dynamic creation and termination of processes and of procedures, our method is especially interesting for typical client-server systems. By using M-nets as the semantic model Me are able to use 'state of the art' verification techniques, For instance, the verification component of the PEP tool may be applied which presently includes partial order based model checking and algorithms based on linear programming as well as interfaces to other verification packages such as INA, SMV and SPIN providing reduction algorithms based on BDDs, on the stubborn set or steep set method, and on symmetries, We show the benefits of our method applying it to a typical client-spryer system. After describing how safety, liveness and progress properties cart be checked fully automatically we give examples holy the compositional nature of the M-net semantics can be used to solve the 'state explosion' problem, and how interactive verification may extend the verification possibilities.