Formale Methoden erweitern das traditionelle Vorgehen des Software Engineering um Verfahren, die die Zuverlässigkeit und Korrektheit sicherheitsrelevanter Teile großer Softwaresysteme mit mathematischer Sicherheit garantieren. Man spricht in diesem Zusammenhang auch von beweisbar korrekten Programmen. Die Leitvorstellung des Vorhabens Verisoft besteht darin, Methoden und Werkzeuge ingenieurmäßig auszurichten und integrierte, mehrere Ebenen umfassende Computersysteme durchgehend formal zu verifizieren. Insbesondere soll die Effizienz bei der computergestützten Durchführung von Beweisen, die notwendig ist, um menschliches Versagen nach Möglichkeit auszuschließen, verbessert werden. Projektbegleitend werden vier konkrete Anwendungsszenarien, davon drei aus dem industriellen Sektor, prototypisch realisiert. Insgesamt sollen die gewonnenen Erkenntnisse und erzielten Fortschritte zu einem entscheidenden Produktivitäts- und Qualitätsschub für die Industrie führen und deutschen Unternehmen dauerhafte internationale Wettbewerbsvorteile verschaffen. Die Erfahrungen, die bei der DFKI GmbH im Bereich der formalen Methoden gerade durch die Entwicklung und Anwendung von VSE (Verification Support Environment) in industriellen Projekten gesammelt wurden, stellen eine Basis für die ehrgeizigen Projektziele von Verisoft dar. Hierbei wird VSE zur Spezifikation und Verifikation auf den verschiedenen Ebenen der Softwareentwicklung, d.h. von abstrakten Systembeschreibungen bis hin zur Verifikation von (kryptographischen) Protokollen, C-Programmen und Pointern,Verwendung finden. Verisoft ist ein langfristig angelegtes Forschungsprojekt, das vom Bundesministerium für Bildung und Forschung (BMBF) gefördert wird. Projektträger ist das Deutsche Zentrum für Luft- und Raumfahrttechnik. Das Konsortium von Verisoft besteht aus den folgenden Partnern: DFKI GmbH, Universität des Saarlandes (Konsortialführung), BMW AG, Infineon Technologies, MPI Informatik Saarbrücken, T-Systems, Technische Universität München, Technische Universität Darmstadt, AbsInt, Universität Karlsruhe (TH)

[Zurück]