Bounded Model Checking for RSL using RT-Tester |
| | 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 | | Type | Master's thesis [Academic thesis] | | Year | 2016 | | Publisher | 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 | | Series | DTU Compute M.Sc.-2016 | | Note | DTU supervisor: Anne Elisabeth Haxthausen, aeha@dtu.dk, DTU Compute | | Electronic version(s) | [pdf] | | Publication link | http://www.compute.dtu.dk/English.aspx | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|