This project is my Master’s Thesis at the Technical University of Denmark.The goal of the project is to create an integrated formal method for software engineering combining the strong sides of formal specification languages with those of graphical notations. Formal specification languages provide precise descriptions of domains and requirements and allow properties of such descriptions to be verified by formal proofs. Graphical notations are intuitively understandable and typically offer a hierarchical view of a system that allows major system parts to be easily identified. By linking the two, it should be possible to benefit from the best of both worlds.
- Acrobat PDF (602 kB)
As a preparation for the thesis I wrote a report in which the syntax and well-formedness conditions of Message Sequence Charts, Statecharts and Petri Nets are formalised in RSL. The report also presents three examples where a system is modelled in RSL and one of the graphical notations in parallel.