Goals and Results

The Verisoft project is a long-term research project funded by the German Federal Ministry of Education and Research (bmb+f). It aims at verifying five concrete application tasks, one from academic and four from industrial background. The verification will be formal and pervasive, i.e., computer-aided verification tools will be used throughout all layers of abstractions. This way, human errors are excluded, full coverage is achieved, and the results are based on a well-known small set of assumptions. Hence, the verified systems are of extreme quality as required in many industrial sectors, such as automotive engineering, security, and medical technology. Additionally, productivity is expected to increase, with all tools being specifically developed and enhanced for this task.

In the following, we give a detailed overview of the goals of Verisoft and the current results for the different subprojects. In addition to that, on the Verisoft Repository page you may find portions of the Verisoft results, which are sufficiently stable and do not contain confidential data of industry partners.

Subproject 1: Methods and Tools

In SP 1 the tools and methods, with which the verification tasks from subprojects 2, 3, 4, and 6 should be accomplished, are to be developed and extended. As a result, the mathematical gaps in the foundations should be formally solved.

Managers of subproject: (Freiburg University); (German Research Center for Artificial Intelligence)

Subproject 2: Academic System

In SP 2 a persistently verified system for signed e-mails is to be constructed. That system should be restricted to effectively applied solutions, so that it can serve as an example for an actual application. The verifiable features of the so-constructed system correspond to the required standards for real systems.

Manager of subproject: (University of Koblenz)

Subproject 3: Correct Industrial Hardware and Software System

In SP 3, both the Hardware of a 32bit-Microcontroller and one representative part of the software and system structure of a 'System-on-Chip' (SoC) from the mobile telephone sector are to be verified. For reasons of confidentiality, we cannot publish any details on this subproject.

Manager of subproject: Prof. Dr. Wolfram BŁttner, OneSpin Solutions

Subproject 4: Biometric Identification System

In SP 4, an access solution consisting of a biometric identification system where the reference data is saved on a Smartcard, is to be persistently verified.

Manager of subproject: (T-Systems)

Subproject 5: Project Management

In SP 5, project management operations relevant to the overall project are to be administered, the scientific work should be coordinated, the guidelines of the overall study and the information exchange are to be supervised and the technical agreement with the bmb+f and the project executing organization is to be completed.

Manager of subproject: (Saarland University)

Subproject 6: Automotive

In SP 6, an application from the automotive sectors shall be pervasively verified: the automatic emergency call system eCall places a call to the rescue coordination center and transmits the vehicle coordinates. To guarantee that this distributed system works correctly, the application eCall, a real-time operating system and a communication bus have to be considered.

Manager of subproject: (Technical University of Munich)

Revision 14 Dec 2006