Integration of Specification Techniques

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.

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.