Bachelor and Master Theses

This thesis aims to implement automated model generation of behavioural models describing ROS 2 systems, containing the needed features for formal verification of execution. ROS 2 tracing will be used as an automated tool to generate ROS 2 system traces, which will be transformed into Eclipse EMF models.

In the first step, features will be identified and extracted that are important to formally verify the execution of ROS 2 systems (based on given formal models). Following, metamodels will be created in EMF containing the needed features.

ROS 2 tracing will be analysed regarding the given features and shortcomings. Shortcomings will be tackled by improvements to be implemented in the official tool library.

As a last step, model parsing (text-to-model transformation), where the tracing output will be translated to the defined eclipse models, will be implemented.

Knowledge in C++, Python, Modeling and ROS 2