Title: Mapping UML diagrams to the Reactive Object Language (Rebeca)
Subject: Software engineering
Level: Advanced
Description: BACKGROUND
Model-Driven Engineering (MDE) is a software engineering branch that proposes the use of models as central artefacts of the development. The aim is to reduce the complexity of real phenomena by approaching them at a higher level of abstraction, where irrelevant details are hidden to the designer. Moreover, automated mechanisms, called model transformations, are used to produce refinements and/or syntheses of models to move towards other domains to perform specific kinds of analyses, and towards lower levels of abstraction to obtain executable specifications (like code in a target programming language).

UML is the de facto standard modelling language in industry. It is a general purpose language, such that any system can be modelled by using the concepts provided by the language. However, when specific analyses need to be performed it is usually preferable to map UML model contents towards other domains, where modelling concepts have stricter semantics and therefore it is possible to execute more precise evaluations. Notably, the Reactive Objective Language (Rebeca), is an actor-based modelling language that allows to perform formal verifications.

This thesis work aims at investigating the viable ways of mapping UML models towards Rebeca. Given Rebeca's characteristics, it is expectable the need for UML behavioural diagram(s) as minimal information of a system in order to obtain something meaningful to be analysed through Rebeca. Additionally, information from structural diagram(s) could be required. Starting from the required system information, modelled in the corresponding UML diagrams, the thesis should propose a mapping between UML concepts and corresponding Rebeca language concepts. The mapping is supposed to be complete enough to allow its direct implementation in a model transformation language to realise an automated translation, or to permit the "mechanical" production of target Rebeca models from source UML models without any relevant auxiliary information.

Upon completion, this work is expected to deliver:
- an analysis of appropriate/needed UML diagrams usable as sources for formal verifications supported by Rebeca;
- a detailed mapping procedure to translate the selected source UML concepts towards corresponding target Rebeca concepts;
- a validation of the method showing the applicability of the proposed solution on different exemplary cases.
Start date:
End date:
Prerequisites: The knowledge of UML is required, while the knowledge of MDE is highly recommended. Previous experiences with formal verification tools, Rebeca, and/or the Eclipse Modeling Framework might be helpful.
IDT supervisors: Antonio Cicchetti
Company contact: