Department of Informatics

TU München - Fakultät für Informatik
Software & Systems Engineering Research Group


Competence Center Specification & Verification & Testing - Projects

Current Projects:

    The first phase of the project is focused on elaborating a modeling technique and methodology for the development of a system-under-development at DENSO. The second phase is planned to be a teaching one. funded by Denso Automotive
    from 2009

Former Projects:

  • Verisoft XT - Automotive Application
    The purpose of this project is to integrate verification techniques in real industrial development processes - from specification and analysis of requirements to a verified implementation. The aim is to delope methods necessary to bridge the gap from informal requirements towards formal specification and from there to executable mplementation.
    funded by the BMBF (Federal Ministry of Education and Research)
    in collaboration with Robert Bosch GmbH
    from 2007
  • Runtime Reflection is a project for establishing methods to dynamically analyse reactive distributed systems at runtime. The approach is layered and modular in that we provide the means for first detecting failures of a system by means of runtime verification and secondly, provide means for identifying their causes by means of a detailed diagnosis. As such, diagnoses can be subsequently used in order to trigger recovery measures, or to store detailed log-files for off-line analysis.

    Check out the Runtime Reflection homepage for further details, examples, downlaods etc.

  • SALT is a temporal specification language that is similar in spirit to programming languages like C and Java and is therefore well suited for software engineers. Its expressiveness, on the other side, covers LTL, or, when the realtime operators of SALT are used, covers TLTL (Timed LTL).

    Parts of SALT are similar in spirit to the specification language Sugar/PSL, a domain specific language used in hardware industry. SALT, however, is designed mainly for software systems. SALT is heavily influenced by the SpecPatterns approach, which collects and documents typical patterns occurring in industrial specifications to make them available to non-expert users. Contrary, however, SALT aims at supporting typical patterns by operators of its language.

    Check out SALT's homepage for further details, examples, downlaods etc.

  • AutoHMI is a project about the model-based design, specification, and verification of automotive human-machine interfaces (HMIs). In particular, we propose an approach for modeling the behavior, structure, and properties of HMIs, and to facilitate their automatic verification by means of model checking. We guide this process by using a well-defined quality model that applies to automotive HMIs and gives firm criteria not only to establish correctness, but also to reason about their usability and, ultimately, user acceptance.
  • INI.TUM (Ingolstadt Institutes of TU München), methods for the application of model-based testing in the automotive industry are developed. Especially in this domain, the expenses for defining test cases manually increases enormously. At the same time, the continously increasing complexity of software intensive functions in cars bears higher risks of undetected errors. In the project adequate modeling techniques are proposed for formally specifying the requirements which may additionally be used for test case generation. The test cases shall be generated in a way that the combination of requirements and known critical design decisions are considered.

    INI.TUM is a cooperation between TUM and Audi AG. Check out the projects' Homepage at INI.TUM (in german or english).

  • AutoFocus 2 Test Case Generator extends the CASE tool AutoFocus 2 by functionality for test case generation. Here we use Constraint Logic Programming (CLP) for test case generation. An AutoFocus model is translated into an equivalent CLP program. Then test case generation is done by solving goals in CLP which define the test case specification.
  • Verisoft-Automotive
    The main goal of the project is the persistent formal verification of computer systems. The correct functionality of systems, as they are applied, for example, in automotive engineering, in security technology and in the sector of medical technology, are to be mathematically proved.
  • DenTUM-I
    The goal of this project was to define a methodology for the model-based development of automotive systems. This methodology was evaluated by developing an Adaptive Cruise Control (ACC) system with Pre-Crash Safety (PCS) functionality.
    funded by Denso Automotive Deutschland
    from 2007
  • CoCoME (Common Component Modelling Example)
    at 2007
  • DenTUM-II
    The goal of this project was to refine a methodology for the model-based development of automotive systems. This methodology was evaluated by developing a Passive Entrance System.
    funded by Denso Automotive Deutschland
    from 2008


© Software & Systems Engineering Research Group
Sitemap |  Kontakt/Impressum
Letzte Änderung: 2011-12-20 17:11:32