TCS / Research / Publications / Automatic Translation of SDL into High Level Petri Nets
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Automatic Translation of SDL into High Level Petri Nets

Reference:

Annikka Aalto. Automatic translation of SDL into high level Petri nets. Technical Report B21, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, November 2004.

Abstract:

Designing, implementing and testing parallel and concurrent programs have traditionally been complex and error-prone tasks. Due to the concurrency and asynchronous communication within the system, the internal behavior of the system tends to be highly nondeterministic and error conditions may be impossible to reproduce. Formal methods address the problem by offering means for exhaustively analyzing all the alternative states of a system. There are many formal analysis methods, but reachability analysis is especially well suited for automatic analysis. In this method, all the reachable states of the system are generated from the model, and then it is checked that they fulfill some desired properties. One problem with the reachability analysis is the creation of the model. If done by hand, it is a very time consuming and error-prone task. This work describes sdl2pn, a front-end for Maria reachability analysis tool. The front-end consists of a parser for SDL-96 language and a model generator for Maria input language. It reads an SDL system description in textual representation and generates a text file containing the high-level Petri net model which can be read and analyzed by the Maria tool. The combination of sdl2pn and Maria can be used to analyze even quite large SDL systems without having to manually construct the model of the system.

Keywords:

SDL, high-level Petri nets, reachability analysis

Suggested BibTeX entry:

@techreport{HUT-TCS-B21,
    address = {Espoo, Finland},
    author = {Annikka Aalto},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {November},
    number = {B21},
    pages = {66},
    title = {{A}utomatic Translation of {S}{D}{L} into High Level {P}etri Nets},
    type = {Technical Report},
    year = {2004},
}

NOTE: Reprint of Master's thesis; see URL below.
PostScript (3 MB)
GZipped PostScript (488 kB)
PDF (782 kB)
See www.tcs.hut.fi ...

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 January 2010.