@MASTERSTHESIS\{IMM2005-03855, author = "S. Andersen and S. Holmslykke", title = "Integration of {''UML-}ised{''} Formal Techniques and Tools with {RSL} and the {RSL} toolset", year = "2005", keywords = "{RAISE,} {RSL,} Graphical Notations, {UML,} Live Sequence Charts, Eclipse", school = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}", address = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby", type = "", note = "Supervised by Professor Dines Bj{\o}rner and co-supervised by Associate Professor Anne Haxthausen", url = "http://www2.compute.dtu.dk/pubdb/pubs/3855-full.html", abstract = "Formal 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." }