Integration of "UML-ised" Formal Techniques and Tools with RSL and the RSL toolset

Steffen Andersen, Steffen Holmslykke

AbstractFormal methods and graphical notations are tools in software engineering and much attention is given to improve the integration of the two. In particular the Unified Modelling Language (UML) seems to have been adopted as a de facto standard in industry as a graphical notation and has attracted much research interest.

Many have focused on the formalisation of UML Class Diagrams with various success. In this thesis we go in the opposite direction. We "UML'ise" the formal specification language RSL by presenting a new diagram called Scheme Diagram which displays the structure of a RSL model. The diagram is visually inspired by the UML Class Diagram but is semantically directly mapped to RSL. A plug-in has been developed for the Eclipse Editor, which enables the user to draw diagrams and translate them into RSL.

Secondly we look at the rather new Live Sequence Charts (LSCs), which are a successor to Message Sequence Charts (MSCs) and hence Sequence Diagrams in UML. We formalise a subset in RSL and examine the usefulness of LSC in a RSL context. An equivalent of LSCs in RSL is presented which allows re nement of the initial model.
KeywordsRAISE, RSL, Graphical Notations, UML, Live Sequence Charts, Eclipse
TypeMaster's thesis [Academic thesis]
Year2005
PublisherInformatics and Mathematical Modelling, Technical University of Denmark, DTU
AddressRichard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby
SeriesIMM-Thesis-2005-20
Note
Electronic version(s)[pdf]
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering