Automatic Formal Model Generation and Analysis of SDL

Abstract. A tool for verification of distributed systems defined using standard SDL-96 is described. The SDL description is automatically translated into a high-level Petri net model which is analyzed using the Maria reachability analyzer. Compared to manual design of a formal model for the system this saves a lot of time and greatly reduces the human mistakes in creating the model. The design process is also con-siderably more efficient because it is possible to check that the system is correct at a very early stage. Methods to reduce the complexity of the analysis both at the modeling and at the analysis level are discussed