TGI-Lehre WWW
 
Kontakt | Index | Suche | Rundgang | English

Maschinelles Beweisen

Veranstalter: Berndt Farwer Michael Köhler Rüdiger Valk

Diese Seite enthält Material und zusätzliche Informationen zur Veranstaltung im SS 2004


18.336 Maschinelles Beweisen

   Berndt Farwer, Rüdiger Valk, Michael Köhler

6st. Di 10 - 14 C-221 Do 10-12 C-221

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).

Terminplan

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):

Material

Gefärbte Petrinetze, Abstrakte Datentypen und MAUDE
Folien zu LTL
Das Mikrowellenbeispiel in MAUDE

Einige Links

Security Protocols, Cryptography

http://www.lsv.ens-cachan.fr/spore/nssk.html
Security Linklist
Computer Security Group
SRI International - Computer Science Laboratory
Security Architectures for Large-Scale Distributed Collaboratory Environments
Ambient calculus
Peter Ryan , Computing Science, University of Newcastle

Coq, LEGO, etc.

Web Links. -- Theorem Provers
The COQ Proof Assistant
The Lego Proof System/

Petrinetze

World of Petri Nets
Basic Research in Computer Science (BRICS)


Korrekturen, Anmerkungen bitte an Michael Köhler
Letzte Änderung: 7.7.2004   http://www.informatik.uni-hamburg.de/TGI/lehre/vl/SS04/mb/