Verification Support Environment (VSE)

Project Description

The use of software systems in safety critical areas (traffic, medicine) is increasingly growing. Thus, trustworthyness and reliability as well as certification of such systems have become issues of great importance. In order to meet the highest levels of dependability for such systems formal methods to support the software development process are required.

During 1991 - 1995 a consortium of german universities and industry cooperatively worked on the project VSE which was ordered and funded by the Bundesamt für Sicherheit in der Informationstechnik (BSI). The main goal of the project VSE was to obtain a software development environment (VSE-tool) which particularly supports modeling and verification of safety critical porperties in software systems.

Specifically with respect to safety critical properties of software systems the application of formal methods has proven to be absolutely necessary. On one hand in this project functional and operational (state oriented) specification and modeling methods as well as the according deduction methods have been integrated within a system. On the other hand the strict formal methods have been embedded in a classical CASE tool.

The main contribution of the department of AI to the project were on one side the development of a specification and modeling language and according methods, and on the other side the participation - partly in a controlling role for formal modeling aspects - in substantial case studies, in order to try out and demonstrate the developed methods and supporting tools.

The project has been completed successfully early 1995 and the VSE system has been delivered to the principal (BSI). For the current state of continued work on VSE see the DFKI VSE project page

Following the VSE project a project VSE-Pilot (VSE-Pilotstudien) has been conducted in order to demonstrate the industrial applicability of the VSE system. This project was funded by the BSI, too, and supported by the same partners that were involved in the VSE project. Eight safety critical case studies were selected from a broad spectrum of application areas which had been suggested by industrial users with interest in applying the VSE system. The eight case studies were carried out by the users who had suggested them; they were supported in this work by the VSE consortium. Two of the applications were attended to by the department of AI.

• Together with the Institut für Eisenbahnwesen und Verkehrssicherung (IfEV) at the University of Braunschweig a safety critical core of the controlling software for the electrical locally operated railway switch (elektrisch ortsbedienten Weiche - EOW), an industrial product of the `IVV Ingenieursgesellschaft für Verkehrsplanung und Verkehrssicherung', Braunschweig, has been modeled, refined, and verfied with the formal methods provided in VSE.
• Together with TÜV Nord, Hamburg, the controlling software of a measuring device has been modeled and verified formally. In order to receive a TÜV certificate for measuring devices also the controller software of the devices needs to be validated. In this case study besides conventional validation procedures also formal verification applying the VSE system has been performed.

At the end of the project `VSE-Pilotstudien' the results from the case studies were presented to the public.

Group Members

• F.W. von Henke
• E. Canver
• D. Schwier

Project Partners

• Deutsches Forschungszentrum für Künstliche Intelligenz (DFKI), Saarbrücken
• Institut für Logik, Komplexität und Deduktionssysteme, Karlsruhe
• DASA - Dornier
• ist - innovative software technologie

Publications

• IFA Symposium 1992 - Overview paper on VSE
• 3. German IT Security Congress 1993 - Overview paper on VSE
• Ulmer Informatik Berichte 96-01 - technical report on the EOW case study.
• ATP 5, 1997 - Article on the EOW case study.