 |
|
|||
| Kontakt | Index | Suche | Rundgang | English |
Diese Seite enthält Material und zusätzliche Informationen
zur Veranstaltung im SS 2004
Berndt Farwer, Rüdiger Valk, Michael Köhler
Exemplarisch für andere Ansätze erlernen die Teilnehmer den Umgang mit dem Werkzeug "Maude", das die Ausführung von Ersetzungstheorien auf Basis algebraischer Datentypen erlaubt. Formale, in Vorlesungen gelehrte Ansätze werden konkret angewendet. Mögliche Anwendungsfelder sind Sicherheitsprotokolle oder Webdienste. Inhalt: Zentrale Infrastuktur-Elemente der Informatik - wie beispielsweise Computer-Chips, Betriebsysteme, Middle-Ware-Componenten - benötigen eine Absicherung der Korrektheit, die nicht mehr durch systematisches Testen, sondern nur noch durch eine formale Verifikation gewährleistet werden kann. Dies ist schon bei einfachen Beispielen nur mit Rechnerhilfe durchführbar.
Gegenstand des Projektes ist die rechnerunterstützte Spezifikation und Verifikation von Software. Zum Einsatz kommen dabei formale Modelle und Ansätze, die zum Teil schon in Grundlagenveranstaltungen vorgestellt wurden. Dazu gehören die algebraische Spezifikation von Datentypen (analog zu Typen der Objektorientierung), die Formaliserung nebenläufiger Systeme durch Petrinetze oder die Verifikation durch temporale Logik (CTL oder LTL).
Das Projekt soll sich am Ablauf eines wissenschaftlichen Workshops orientieren. Das Thema des Workshops befasst sich allgemein mit rechnerunterstützten Korrektheitsbeweisen von Software. Die Anwendungsfelder sind beispielsweise:
Die Projektteilnehmer definieren sich Teilprojekte und fassen ihre Arbeiten in Form eines Beitrages zusammen. Das Verfahren ist zweistufig: Zuerst wird ein Kurzbeitrag (extended abstract) verfasst, der die Fragestellung des Gebiets und das Vorhaben darstellt. Die Kurzbeiträge werden von allen Teilnehmen (konstruktiv) begutachtet. Danach wird die Langfassung erstellt, in der das Vorgehen und die erzielten Ergebnisse dargelegt werden. Auch die Langfassungen werden von den Teilnehmern begutachtend diskutiert. Die finalen Fassungen werden abschließend in Form eines Sammelbandes gebündelt. Zum Ende des Projektes findet der Workshop statt, wo die Ergebnisse im Form von Vorträgen präsentiert werden. Es ergibt sich folgender Terminplan (aktualisiert am 11.6.04):