TCS / Research / Publications / A Reachability Analyser for Algebraic System Nets
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

A Reachability Analyser for Algebraic System Nets

Reference:

Marko Mäkelä. A reachability analyser for algebraic system nets. Research Report A69, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, June 2001.

Abstract:

Concurrent and distributed systems are difficult to manage without using formal analysis methods. The user of formal methods has to find a balance between expressive power and tractability. A formalism with small expressive power may not suit well to describing all real-life systems, but on the other hand, performing exhaustive reachability analysis on a system defined using a highly expressive formalism may be an unsolvable problem.

Using extended many-sorted algebras, this work defines the data type system and the set of algebraic operations that the author has implemented in a reachability analyser intended for modelling computer software based communications protocols. The work also introduces the modelling formalism of the analyser, algebraic system nets.

The report discusses some implementation details of the reachability analyser both from a theoretical and from a software technology point of view. Finally, the work shows how some constructs difficult for other tools can be modelled using the new formalism, and describes how different programming language constructs can be transformed to parts of a model by a semi-automated compiler.

Keywords:

many-sorted algebras, algebraic system nets, distributed systems, reachability analysis

Suggested BibTeX entry:

@techreport{HUT-TCS-A69,
    address = {Espoo, Finland},
    author = {Marko M{\"a}kel{\"a}},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {June},
    number = {A69},
    pages = {93},
    title = {A Reachability Analyser for Algebraic System Nets},
    type = {Research Report},
    year = {2001},
}

PostScript (1 MB)
GZipped PostScript (471 kB)
PDF (867 kB)

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