Out-of-the-Box Ideas

Project Overview

Model-Based Systems Engineering (MBSE) is an essential approach for designing and analyzing complex Cyber-Physical Systems (CPSs). This project aims to compare different MBSE modeling languages by applying them to the same CPS, evaluating their strengths and weaknesses.

Project Objectives

1. Select a CPS to Model:
2. The system should ideally have both hardware and software components.Possible candidates include the OH-320 or a similar system.
3. Identify 2 or 3 MBSE Models:
4. Identify commonly used MBSE modeling languages.Evaluate their suitability for CPS modeling based on some aspects:
   • Expressivity: How well does the language capture a system’s complexity?
   • Validation & Verification Features: What built-in tools exist for correctness checking?
5. Model the same CPS Using Different MBSE Languages:
6. Implement the same CPS in multiple modeling languages.Compare the outcomes and assess differences in capabilities and usability of the MBSE models.

Expected Outcomes

• A comparative analysis of 2 or 3 MBSE languages for CPS modeling.
• A demonstration of how these different languages represent the same CPS.

 Connection to the ZORRO Project

This work contributes to ongoing research in the Zero Downtime for Cyber-Physical Systems (ZORRO) consortium:

• You will lay the foundation for a literature study on MBSE languages (relevant for industry stakeholders).
• Your MBSE models will be aligned with an existing conceptual model to:
• Validate that model's applicability.Demonstrate Fault Tree (FT) generation across different modeling languages.Explore how system models can be split across different modeling languages while maintaining consistency.
• Your MBSE models may be used to inspire a unifying representation for different MBSE models

Supervisors: Peter Lammich
In this project, you will design and optimize a drat certificate checker. DRAT is used to certify the outputs of SAT solvers. While the certificate checker is less complex than a SAT solver, it still has to perform some time-critical operations, that can profit a lot from low-level optimizations.

Supervisors: Edoardo Putti, Peter Lammich

Once you proved your program correct there is no need to debug it! Unfortunately all tools for performance analysis require debug information. We want to generate debug information for our verified program so that we can optimize them further. In this project you will learn how to use LLVM to generate debug information so that profilers and debuggers can be used with our verified toolchain.

Supervisors: Peter Lammich
Interactive Theorem Provers (ITPs) provide a way to develop computer checked (mathematical) proofs. In this project, you will learn to use an ITP, and apply it to formalize some interesting theory. The theory to be formalized will be chosen in coordination with the supervisor, to suit your interests and be realistically achievable for a BsC project.