Integration objekt-orientierter Modellierung und formaler Verifikation

mehr sicherheitskritische Anwendungen entstehen. Bisher unterstützen
jedoch Werkzeuge und Methoden zur formalenSoftware-Verifikation die in
der Praxis verwendeten Spezifikationsformalismen und Programmiersprachen
nur ungenügend.

In meinem Vortrag stelle ich das KeY-Projekt vor. Es verfolgt das Ziel,
dieses Problem zu überwinden und langfristig formale Methoden aus der
universitären Forschung in die betriebliche Anwendung zu transferieren.
Der methodische Ansatz besteht darin, ein kommerzielles CASE-Werkzeug um
Funktionalitäten für formale Spezifikation und deduktive Verifikation zu
erweitern. Damit soll es möglich werden, formale Methoden stufenweise
und ohne Änderung des Arbeitsumfeldes in die industrielle
Software-Entwicklung einzuführen.

Ein wichtiger Teil des KeY-Projektes, auf den ich detaillierter eingehen
werde, ist die Entwicklung einer Dynamische Logik für die
Programmiersprache Java Card und eines Kalküls, mit dessen Hilfe
Java-Programme verifiziert werden können.