Automatic Formal Model Generation and Analysis of SDL

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 considerably 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.

• Type: Conference
• Year: 2003
• Where: SDL
• Authors: Annikka Aalto, Nisse Husberg, Kimmo Varpaaniemi
• Keywords: Formal Model, Maria Reachability Analyzer, Petri Net Model, SDL 2003, SDL 2007