Case Studies
Focus on Isabelle
LaTeX representation


   Current Projects:

    Collaboration between TU München and DENSO Corporation.
    Objectives: 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 an industy-oriented lecture cours for engeneers of DENSO (Japan).
    Funded by: Denso Automotive.
    Status: Project ongoing (2009 -).
  • AutoFocus3: Focus on LaTeX
    Objectives: Developing an add-on to the AutoFocus3 CASE tool to generate from an AutoFocus model the corresponding formal specification in FOCUS represented in LaTeX.
    Status: Project ongoing (2011 -).
  • Focus on Isabelle
    Objectives: Tool-support to the methodology Focus on Isabelle: developing a translator of formal specifications in FOCUS to Isabelle/HOL.
    Status: Project ongoing (2011 -).

   Former Projects:
  • Verisoft XT - Automotive Application (part of the Verisoft XT project):
    In collaboration with Robert Bosch GmbH
    Objectives: 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: BMBF (Federal Ministry of Education and Research)
    Status: Project completed (2007-2010).
    Collaboration between TU München and Denso Automotive Deutschland .
    Objectives: The goal of the 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.
    Status: Projects completed (2006 - 2007).
  • Verisoft Automotive (part of Verisoft, Verisoft @ Munich )
    In collaboration with BMW Group
    Objectives: 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.
    Funded by: BMBF (Federal Ministry of Education and Research)
    Status: Project completed (2003-2007).
  • CoCoME (Common Component Modelling Example)
    Objectives: Evaluation and comparizon the practical appliance of existing component models using a common component-based system as modelling example.
    Status: Project completed (2007)
  Maria Spichkova
  Last modified 29.07.2011