Automatic Formal Model Generation and Analysis of SDL (2003)
AUTHORS:
Aalto Annikka,
Husberg Nisse,
Varpaaniemi Kimmo
BOOKTITLE:
SDL 2003: System Design, 11th International SDL Forum, Stuttgart, Germany, July 1--4, 2003, Proceedings
SERIES:
Lecture Notes in Computer Science
VOLUME:
2708
PAGES:
285--299
URL:
http://users.tkk.fi/~kvarpaan/info/AaHuVrp03.html
@inproceedings{ AaHuVrp03, editor = "Reed, Rick and Reed, Jeanne", author = "Aalto, Annikka and Husberg, Nisse and Varpaaniemi, Kimmo", publisher = "Springer-Verlag, Berlin, Germany", note = "© Springer-Verlag Berlin Heidelberg 2003", title = "{A}utomatic Formal Model Generation and Analysis of {S}{D}{L}", url = "http://users.tkk.fi/~kvarpaan/info/AaHuVrp03.html", series = "Lecture Notes in Computer Science", 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", pages = "285--299", volume = "2708", flags = "ANNA-MARIA", year = "2003", keywords = "SDL, reachability analysis, high-level Petri nets, state space explosion problem", 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." }