From C/C++ Code to Formal Models and Vice Versa

The modern embedded software development process promotes the use of formal methods for modeling and verification. However, the gap between formal models and practical code implementations remains a significant challenge. Bridging this gap is essential for comprehensive software correctness and seamless integration.
The goal of this thesis is to develop a framework that automates the translation of C/C++ code into formal models and vice versa.

Download as PDF

Thesis Type:

  • Master Thesis / Bachelor Thesis

Goal and Tasks:

  • Develop set of rules for translating C/C++ code to formal model tool UPPAAL;
  • Automate the translation of code to models and models to code;
  • Proof of concept: RTOS C code implementations.

Recommended Prior Knowledge:

  • C or C++ programming;
  • Embedded Systems;
  • Real-Time Operating Systems.


  • a.s.a.p.