Student Topics

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.

Have a look at some currently available projects or at the completed projects and theses:

• Modeling of Embedded (Automotive) Systems
• Heuristics-Guided Dependability Analysis
• Quantitative Analysis of Software and Software Architectures
• VIP

Mentor Conversation

Bachelor program documents

• Mentorengespräch (German) [PDF] [RTF]

Master program documents

• Mentor Counseling Protocol (German) [PDF] [RTF]
• Mentor Counseling Protocol (English) [PDF] [RTF]

Model-based construction of software has become increasingly important especially for embedded software, 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.

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

• Model Checker for SURTA
  (Project / Thesis)
  
  In the SURTA (Semantics of UML-RT in AsmL) project (PDF ), we translate models from UML Real Time to Abstract State Machine Language (AsmL). The goal of this project, is to create a tool based approach that will enable us to do model checking on the resulting AsmL models and interpret the results of the model checking on the level of the UML-RT model. The moonwalker model checker can serve as a basis for this work.

 

• Modeling and Verification of Parts of the FlexRay Bus
  (Project)
  
  To asses the scaling and applicability of the approach, case studies need to performed. One case study could be based on the FlexRay Automotive Bus (http://www.flexray.com/). To perform the case study, part of the FlexRay Automotive Communication Protocol needs to be modeled in UML-RT. After that, verification properties need to be selected, on basis of the FlexRay specification and the verification needs to be performed with our tools.

Projects for Students on Master Level

• Definition and Implementation of Model Transformations between different modeling languages
• Verification of some part of the AUTOSAR specification
• Derivation of Abstractions for Model Checking

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

Contact: Florian Leitner-Fischer

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
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

• Visualization Techniques for probabilistic Counterexamples
  (Project / Thesis)
  DiPro uses the commercial framework yFiles (www.yworks.com) to visualize the counterexamples as a graph. Since this is only one way to visualize counterexamples, we would be interested in a comparison of different open source visualization frameworks and ways to further integrate the idea of interactive counterexample exploration. Furthermore, the visualizations shall be developed in a way that they can be used on a high-resolution display (e.g. EyeVis Display or Powerwall).

Master

• Modeling of practical (industrial) case studies in PRISM and analysing them using DiPro
• Working on visualization techniques for diagnostic traces
• ...

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: Florian Leitner-Fischer

When developing a safety-critical system it is essential to obtain an assessment of different design alternatives.
In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work.
We work on developing methods and tools that bridge the gap between academia and industrial practice.
QuantUM is one of these tools and allows for the quantitative safety analysis of UML models.

Bachelor

• QuantUM Release 1.0
  (Project)
  In this project the step from research prototype to release candidate shall be made.
  In order to reach the quality needed for a public release, the graphical user interface of QuantUM needs to be extended,
  the XMI import needs to be revised and some minor bugs need to be fixed.

Master

• Extending QuantUM to support the SysML
  The QuantUM tool is based on a UML profile that is used to annotate the UML models. This profile shall be extended to allow the application to the SysML.

• Extending QuantUM to support AADL
  The Architecture Analysis and Design Language is a architecture description language standardized by SAE and is widely used in the avionics field.
  It shall be investigated whether the QuantUM approach can be extended to AADL.
  

Contact: Florian Leitner-Fischer

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:

• Reverse-Engineering von VIP: Erstellung eines UML-Modells, Erkennung von Entwurfmuster, Dokumentation, etc.
• Pflege, Weiterentwicklung, Testen, etc.

Contact: Florian Leitner-Fischer

This is a (incomplete) list of current and completed projects and theses.

Projects for Students on Bachelor Level

• Modelling of the AUTOSAR NVRAM Manager as a Matlab / Simulink Model
  (Project)
  
  The goal of this project was to model the AUTOSAR NVRAM Manager as a Matlab / Simulink Model based on the AUTOSAR standard specification.

• Simulink Design Verifier vs. SPIN - A Comparative Case Study
  (Thesis) - PDF
  
  An increasing number of industrial strength software design tools come along with verification tools that offer some property checking capabilities. On the other hand, there is a large number of general purpose model checking tools available. The question whether users of the industrial strength design tool preferably use the built-in state space exploration tool or a general purpose model checking tool arises quite naturally. Using the case study of an AUTOSAR compliant memory management module we compare the Simulink Design Verifier and the SPIN model checking tool in terms of their suitability to verify important correctness properties of this module. The comparison is both functional in that it analyzes the suitability to verify a set of basic system properties, and quantitative in comparing the computational efficiency of both tools.

• Assesment of Modeling Languages for Automotive Software Engineering
  (Project)
  
  In order to assess the modeling languages UML 2.1, SysML and UML-RT parts of the AUTOSAR architecture shall be modeled in each language.
  Based on the gained experience, the three languages shall be compared and advantages / disadvantages identified.

• Model Checker for SURTA
  (Thesis)
  
  In the SURTA (Semantics of UML-RT in AsmL) project (PDF ), we translate models from UML Real Time to Abstract State Machine Language (AsmL). The goal of this project, is to create a tool based approach that will enable us to do model checking on the resulting AsmL models and interpret the results of the model checking on the level of the UML-RT model. The moonwalker model checker can serve as a basis for this work.

• Visualization Techniques for probabilistic Counterexamples
  (Project)
  
  DiPro uses the commercial framework yFiles (www.yworks.com) to visualize the counterexamples as a graph. Since this is only one way to visualize counterexamples, we would be interested in a comparison of different open source visualization frameworks and ways to further integrate the idea of interactive counterexample exploration. Furthermore, the visualizations shall be developed in a way that they can be used on a high-resolution display (e.g. EyeVis Display or Powerwall).

Projects for Students on Master Level

• An Experimental Comparison of Counterexample Generation Methods for Markov Decision Processes
  (Thesis)

• Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples
  (Project)
  
  Failure mode and effects analysis (FMEA) is a technique to reason about possible system hazards that result from system or system component failures. Traditionally, FMEA does not take the probabilities with which these failures may occur into account. Recently, this shortcoming was addressed by integrating stochastic model checking techniques into the FMEA process. A further improvement is the integration of techniques for the generation of counterexamples for stochastic models, which we propose in this project. Counterexamples facilitate the redesign of a potentially unsafe system by providing information which components contribute most to the failure of the entire system. The usefulness of this novel approach to the FMEA process is illustrated by applying it to the case study of an airbag system provided by our industrial partner, the TRW Automotive GmbH.

• Quantitative Safety Analysis of UML Models
  (Thesis)
  
  When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Another obstacle is, that the methods often require a profound knowledge of formal methods, which can rarely be found in industrial practice. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. We propose a UML profile that allows for the specification of all inputs needed for the analysis at the level of a UML model. The QuantUM tool which we have developed, automatically translates an UML model into an analysis model. Furthermore, the results gained from the analysis are lifted to the level of the UML specification or other high-level formalism to further facilitate the process. Thus the analysis model and the formal methods used during the analysis are hidden from the user.