@phdthesis{
    Makela:LicTech,
    author = {M{\"a}kel{\"a}, Marko},
    ps = "rasn.ps",
    school = "Helsinki University of Technology, Department of Computer Science and Engineering",
    title = "A Reachability Analyser for Algebraic System Nets",
    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 thesis also introduces the modelling formalism of the analyser, algebraic system nets. The thesis 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.",
    address = "Espoo, Finland",
    month = "March",
    flags = "LICTHESIS public copy",
    year = "2000",
    keywords = "many-sorted algebras, algebraic system nets, distributed systems, reachability analysis",
    pdf = "rasn.pdf",
    type = "Licentiate's Thesis",
    superseded = "HUT-TCS-A69"
}