Bachelor and Master Theses

Robot Operating System (ROS) is widely used in academia and industry, and importantly is leveraged in safety-critical robotic systems. The quality of ROS software can affect the safety and security properties of robotics systems; therefore, reliability and quality are imperative to guarantee. Therefore, it is important to formally perform software verification. This can be seen in the development process of a safety-certified software in automobile and robotics companies such as Volvo Group.

In this project, we aim to develop a compiler that translates a ROS software, i.e., ROS2 codes, to the Rebeca modeling language that is being formally verified for the safety and security properties using model checking.

Rebeca and ROS2:

Rebeca is an actor-based modeling language and its extension; Timed Rebeca is used for verifying embedded and real-time systems properties.

ROS2 is a collection of tools and libraries that aid robotics software development. Based on the architecture of the ROS2, the middleware layer is developed using C, while the higher layer can be implemented using various programming languages such as Java, Python, and C++. The ROS community uses Git repositories for its source code, hosting them freely on GitHub.

Objective:

The goal of this thesis is to develop a compiler to generate a Timed Rebeca code from a ROS2 code.

In particular, building a programming tool (a simple compiler) to translate the source language (it's ROS2) to the target language (it's Timed Rebeca).

Expected outcomes:

- Develop a compiler for transforming a ROS2 code to a Timed Rebeca code.

- Provide the applicability of the developed compiler in an academic or industrial example.

References:

ROS2: https://docs.ros.org/en/dashing/Concepts.html

Rebeca Homepage: http://rebeca-lang.org/Rebeca 

This thesis is primarily intended for Basic and Advanced Level student(s) with good knowledge of C/C++, Java, and modeling system design.

Don't hesitate to contact me (fereidoun.moradi@mdu.se) if you have any questions. We can discuss and fit the project idea based on the thesis requirements, estimated time for doing the literature review, writing the thesis and implementation.

Volvo CE (VCE)