@MASTERSTHESIS\{IMM2016-06926,
    author       = "P. H. {\O}stergaard",
    title        = "Bounded Model Checking for {RSL} using {RT-}Tester",
    year         = "2016",
    school       = "Technical University of Denmark, Department of Applied Mathematics and Computer Science",
    address      = "Richard Petersens Plads, Building 324, {DK-}2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk",
    type         = "",
    note         = "{DTU} supervisor: Anne Elisabeth Haxthausen, aeha@dtu.dk, {DTU} Compute",
    url          = "http://www.compute.dtu.dk/English.aspx",
    abstract     = "The goal of this thesis is to implement a translator that takes the specification of a given {RSL} state transition system, and translates it into a corresponding model in {RT-}Tester. The purpose of this translation is to combine the powerful specification capabilities of {RSL} with the model checking capabilities of RTTester.

The method chosen to accomplish this goal, is to design an intermediate language which acts as a concise, concrete syntax for {RT-}Tester. {RSL} specifications are translated to this intermediate language, which is then parsed into a model in {RT-}Tester to be model checked.

The subset of {RSL,} which the translator accepts, is presented, and the syntax of the intermediate language is defined in the form of a {BNF} grammar. The translation to the intermediate language is defined mathematically using a system of inference rules.

The implementation of the translator and parser is described, and the implementation is tested to show that it matches the design. 

In conclusion the goal of the thesis is deemed fulfilled, albeit only for a subset of {RSL}.

Attached pdf full-text file, updated version March 2016"
}