Verisoft Project Summary

Verisoft Project Summary

The Verisoft Project is a long-term research project funded by the German Federal Ministry of Education and Research (BMBF). The Verisoft Project is planned over eight years, the first four of which have presently been approved and funded by the BMBF starting from July 2003.

The Verisoft Project aims to develop techniques, which permit the pervasive formal verification of computer systems comprising hardware, system software, communication systems, and applications. As a proof of concept, these techniques are being applied to four prototypical systems, three of which are in industrial context:

• In subproject 3, the hardware of a 32-bit industrial microcontroller are to be verified.
• In subproject 4, a chipcard-based biometric identification systems is being examined.
• In subproject 6, an eCall system for automobiles is verified, which is automatically placed on the mobile phone net after the sensors of a car have detected that it was involved in a crash. The application runs on a system of several electronic control units (ECUs). The local application programs of the ECUs run on top of a simple real time operating system kernel like described in the OSEKTime standard. ECUs are connected via a FlexRay-like communication bus.
• In subproject 2, the seamless verification of the Academic System is attempted. This system consists of hardware (processor and devices) on top of which runs a microkernel, an operating system, and communicating applications. Subproject 2 is not in industrial context and therefore not subject to confidentiality constraints. Implementations, models, and proofs are meant to be disclosed when complete.