[an error occurred while processing this directive]

Student Topics

Bachelor Projects, Master Projects, Hiwi-Jobs

We are constantly looking for students interested in bachelor or master projects in our group. At the moment, we also have some positions as research assistants (Hiwi-Students) available.

Some currently available projects:

Mentor Conversation

Bachelor program documents
Master program documents

Modeling of Embedded (Automotive) Systems

Model-based construction of software has become increasingly important especially for embedded sofware, e.g. software that runs in cars, airplanes, or small devices. In all of these domains, software quality, i.e. the absence of bugs, is very important. In our research, we aim to improve software quality by proving some properties - like unreachability of certain "error-states" - by means of model checking.

We use tools like UPPAAL and Rational Rose Real Time enhanced with our own techniques. To test and evaluate these techniques, we need models of larger and "more real-life" systems as input. We also plan to check "higher-level" modeling languages such as (Real Time) UML or domain-specific languages such as AUTOSAR by means of model transformation.

Here are some specific ideas that could be done either as Bachelor Project, Master Project or Hiwi position (25 - 85 hours per month, depending on your time and ambition):

Projects for Students on Bachelor Level

Projects for Students on Master Level

Please note that these are only some suggestions. You are welcome to bring your own ideas for projects in this general setting.

Contact: Wei Wei




Heuristics-Guided Dependability Analysis

Stochastic Model Checking is an automated technique to systems with respect to their performance and dependability which are important aspects of the system quality. However, current stochastic model checking tools do not provide diagnostics and debugging information. This fact constrains their practical use. We are working on this problem in the scope of the DiRePro project funded by the DFG and associated with the Transregional Collaborative Research Center 14 AVACS. We investigate methods to generate diagnostics information for stochastic model checking. We apply heuristic-guided search algorithms, like Best-First Search, to efficiently determine diagnostic traces, also known as failure traces or counterexamples, which carries large amount of probability. The delivered traces are essential tools for diagnostics and debugging. In the course of our work on this topic, a prototype tool called DiPro has been implemented. DiPro is implemented in Java and linked to the stochastic model checkers PRISM developed bei the research group of Prof. Marta Kwiatkowska at the Computing Laboratory of the University of Oxford, UK and to MRMC developed by the Formal Methods & Tools (FMT) group at the University of Twente, The Netherlands and the Software Modeling and Verification (MOVES) group at RWTH Aachen University, Germany under the guidance of Prof. Dr. Ir. Joost-Pieter Katoen.

Features of DiPro:

  1. Directed and undirected search algorithms for exploring the state space of probabilistic models on-the-fly
  2. Generation of diagnostic traces carrying a high amount of probability and counterexamples for probabilistic timed safety propertie
  3. On-the-fly visualization of state space of probabilistic models
  4. Presenting the solution in various formats, e.g. AUT and DOT

DiPro is still under construction and a lot of work should be done to achieve the status of a stable and convenient tool. Within the scope of the development of DiPro we offer Bachelor and Master projects in the following tasks:

  1. Implementation of Interfaces to existing stochastic model checkers like MRMC [already done]
  2. Integration of DiPro into PRISM Model Checker
  3. Working on the visualization of state spaces
  4. Modeling of practical case studies in PRISM and analyzing them using DiPro

While Bachelor projects are on the level of development and application, Master projects are supposed to be research oriented involving creativity and autonomous problem solving. Concrete samples for project topics:
Bachelor

Master On both Bachelor and Master levels the work is performed in agreeable environment. The close collaboration with other team members and the intensive and direct supervision make it easier to come up with creative ideas, to address challenges and to solve problems.

In the case of interest, please contact us per e-mail or phone. We will be happy to talk to you about details in an individual meeting.

Contact: Husain Aljazzar

Applications of Graph Search Algorithms

We work on developing directed graph search algorithms to be used in the verification of computer systems. Such algorithms are guided using heuristics which makes them highly scalable. We offer student projects on both bachelor and master level in this field. For instance:
Bachelor Master

Contact: Husain Aljazzar



VIP

VIP ist ein systemunabhängiger Editor für die Modellierungssprache V-Promela. V-Promela ist eine visuelle, objektorientierte Erweiterung von Promela zur hierarchischen Modellierung von Architektur und Verhalten von verteilten, nachrichten-basierten reaktiven Systemen. Auf Bachelor-Level bieten wir Projektthemen in den folgenden Aufgabenbereichen:

Contact: Husain Aljazzar



[an error occurred while processing this directive]