Finished Projects
KI-LOK － Test Procedures for AI-based Components for Railway Systems
The KI-LOK project researched new test procedures and tool-based methods for the validation and certification of AI-supported technologies for safety-critical applications in railway technology.
The use of AI-based components is being considered for many novel railway systems. However, certification of AI components is still a major challenge. The KI-LOK project studied new test procedures for AI-based components to enable certification.
In the KI-LOK project the HHU has shown how to apply formal mathematical models to increase the safety of AI systems, with the long term goal of obtaining understandable safety cases and achieve certification. The HHU has studied the „certifying control“ approach, whereby the AI has to produce in addition to its output a certificate. This certificate can be changed by an independent classical piece of software. For a case study of detecting signs and signals during shunting movements the HHU has shown that the “false positive” rate can be reduced by this technique to almost zero. To detect “false negatives”, the HHU has developed a formal B model which can be used at runtime to check the AI output for plausibility (e.g., to detect missing signals at points where a signal is expected). The formal models enabled the use of “safety shields” which surround the AI components.
More information can be found in the final report (only available in German) and on the project website.
Funding guideline „Neue Fahrzeug- und Systemtechnologien“ BMWi
Funding period: 01.04.2021 － 30.09.2024
Project management HHU: Michael Leuschel
Project partners:
- Hitachi Rail (GTS Deutschland GmbH) － formerly Thales Deutschland GmbH
- Fraunhofer Institut für Offene Kommunikationssysteme FOKUS
- IT Power Solutions GmbH
- neurocat GmbH
PyJIT
PyPy is an open source project that implements a flexible interpreter for Python in Python. Only few lines of code are required to implement modern security mechanisms or alternate concurrency models. Adaption of PtPy in industrial settings requires a combination of the flexibility and good performance. Within the PyJIT project we develop a "Just in time" compiler toolkit. We hope to develop a Python implementation that is not only more flexible but also faster than the reference implementation. The project will open new fields of application for Python, such as porting Python to specialized hardware (embedded systems). We will apply the techniques also to other languages.
ProCSP
Extension of ProB to be able to animate CSP-M specifications in FDR syntax and link them with B machines. Funded by AWE.
Gepavas
A DFG-funded project on directed and parallel model checking of high-level specifications. Started 2008.
We investigated two approaches:
- Directed Model Checking
- Parallelization
DEPLOY
An EU-funded Framework 7 IP; has started in February 2008.
Deploy Website
Advance
An EU-funded Framework 7 STREP; to start in October 2011.
ADVANCE Website
ASAP
The overall aim of this project is to develop techniques which enable the development of sophisticated and reliable software systems that are easy to maintain, and can be deployed on new generation, pervasive computing platforms.
PyPy
PyPy is a reimplementation of Python written in Python itself, flexible and
easy to experiment with. Our long-term goals are to target a large variety of platforms, small and large, by providing a compiler toolsuite that can produce custom Python versions. Platform, Memory and Threading models are to become aspects of the translation process - as opposed to encoding low level details into a language implementation itself. Eventually, dynamic optimization techniques - implemented as another translation aspect - should become robust against language changes. The EU-funded period of the project is finished, but development continues and we have requested funding for a follow-up project.
Rodin
Our overall objective is the creation of a methodology and supporting open tool platform for the cost effective rigorous development of dependable complex software systems and services.
TSAS
The Trusted Software Agents and Services (TSAS) project is investigating and demonstrating the Trust issues that arise from accessing software services and utilising agent technology in PervasiveComputing environments. The project is developing software/hardware demonstrators with which to explore and highlight trust matters in the context of applications such as home finance or tele-medicine. The project is also examining the appropriate validation techniques that can help to achieve assurance of trustworthiness in such technologies.
ABCD
Automated Validation of Business Critical Systems with Component Based DesignsThe objective of this project is:
- to increase the uptake of formal modelling in the business critical systems industry.
We plan to achieve this by:
- lowering the cost of entry and
- increasing the benefits of using formal modelling.
We will be able to:
- lower the cost by building a repository of generic models of systems and components;
- increase the benefits by making verification and validation of critical systems available to real system architects;
- lower the cost and increase the benefits by providing automated tool support.
The focus is on support of system definition and architectural design so that the systems integrator can more easily model systems and validate proposed system architectures.
iMoc
The main objective of the project is to study the potential of automatically deriving abstractions for infinite model checking through a combination of existing technology for the automatic control of partial evaluation and abstract interpretation. First successful experiments of this idea have been conducted using the ECCE and LOGEN tools. The project consists of a theoretical study coupled with the implementation of a combined partial evaluation and abstract interpretation system (based upon ECCE). The practicality of the approach will be gauged on realistic examples, some of them coming from the EPSRC funded ABCD project for the validation of business-critical systems.
Additional pointers:
IOPS
Improving Offline Program Specialization This is a DAAD funded project in collaboration with the group of Germán Vidal from the University of Valencia. Scheduled to run from January 2007 to December 2008.
JASP
Demonstrably correct compilation of Java Byte Code. Three month industrially sponsored project.