||Integration of "UML-ised" Formal Techniques and Tools with RSL and the RSL toolset
||Bjørner, Dines (Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Haxthausen, Anne Elisabeth (Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
||Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
||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.
||Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU : DK-2800 Kgs. Lyngby, Denmark
||RAISE; RSL; Graphical Notations; UML; Live Sequence Charts; Eclipse
Creation date: 2006-06-22
Update date: 2012-12-19