Automatic Formal Model Generation and Analysis of SDL

Reference:

Annikka Aalto, Nisse Husberg, and Kimmo Varpaaniemi. Automatic formal model generation and analysis of SDL. In Rick Reed and Jeanne Reed, editors, SDL 2003: System Design, 11th International SDL Forum, Stuttgart, Germany, July 1–4, 2003, Proceedings, volume 2708 of Lecture Notes in Computer Science, pages 285–299. Springer-Verlag, Berlin, Germany, 2003. © Springer-Verlag Berlin Heidelberg 2003.

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

Keywords:

SDL, reachability analysis, high-level Petri nets, state space explosion problem

Suggested BibTeX entry:

@inproceedings{VarpaaniemiKimmo-AaHuVrp03,
    author = {Annikka Aalto and Nisse Husberg and Kimmo Varpaaniemi},
    booktitle = {{S}{D}{L} 2003: {S}ystem Design, 11th International {S}{D}{L} {F}orum, {S}tuttgart, {G}ermany, {J}uly 1--4, 2003, Proceedings},
    editor = {Rick Reed and Jeanne Reed},
    note = {© Springer-Verlag Berlin Heidelberg 2003},
    pages = {285--299},
    publisher = {Springer-Verlag, Berlin, Germany},
    series = {Lecture Notes in Computer Science},
    title = {{A}utomatic Formal Model Generation and Analysis of {S}{D}{L}},
    volume = {2708},
    year = {2003},
}