Bachelor and Master Theses

To apply for conducting this thesis, please contact the thesis supervisor(s).

Title:	Modeling and Model Transformation for Verification of ROS 2 Systems using Eclipse and UPPAAL
Subject:	Computer science, Embedded systems, Robotics, Distributed systems
Level:	Advanced
Description:	This thesis aims to create metamodels (using Eclipse EMF) for the structural and behavioural modelling of ROS 2 systems with the goal of formal verification using given formal models. Model transformations will be implemented to transform between the models and the given formal model in UPPAAL. In the first step, ROS 2 and the UPPAAL model will be analysed to identify and extract the essential features needed to create behavioural and structural models. These features include Quality of Service (QoS) attributes, extraction of communication,... Then, metamodels are to be defined, describing the identified features of ROS 2 systems. Following, the model transformations will be implemented and tested on created scenarios. The existing formal models in UPPAAL may be refined, improving verification by inclusion of different Quality of Service attributes in communication. Therefore, suggestions may be made throughout the thesis.
Start date:
End date:
Prerequisites:	Knowledge of C++, EMF, Modeling and ROS 2
IDT supervisors:	Lukas Dust
Examiner:	Cristina Seceleanu
Comments:
Company contact: