Proof-Carrying Code (Lab)

 

Organisator: Prof. Dr. Heiko Mantel
Registrierung: im Sekretariat des Fachgebiets bei Frau Kraft (Sprechzeiten Frau Kraft)
Literatur: Wird in der Vorbesprechung bekanntgegeben
Vorbesprechung: 15. April 2010, 16:30 Uhr, S2/02 E302
Wöchentlicher Termin: Mi, 16:15-17:55 Uhr in E306
Kontakt: Bei Fragen bitte an Dieter Schuster wenden.

Das Praktikum gehört zu Foundations of Computing (Modulhandbucheintrag).

Vorwissen:
  • Programmieren in Java
  • Pflichtvorlesungen der ersten vier Semester Informatik

Thema:

Bei einer gegebenen Software lässt sich nicht ohne weiteres sagen, ob sie die Eigenschaften erfüllt, die der Hersteller für die Software verspricht. Liegt eine formale Spezifikation dieser Eigenschaften vor, so kann mit mathematischen Methoden beweisen werden, ob die Software diese Eigenschaften erfüllt.

Die Idee des Proof-Carrying-Code ist, die Software mit einem Beweis zu bündeln, anhand dessen gewisse Eigenschaften der Software überprüft werden können. Die Erstellung dieser Beweise sind eher schwierig, die Überprüfung der Software anhand des Beweises kann hingegen automatisch erfolgen. Der Aufwand der Beweisüberprüfung kann relativ hoch sein, insbesondere auf ressourcenarmen mobilen Endgeräten.

In diesem Praktikum wollen wir ein Rahmenwerk für Proof-Carrying-Code aufbauen. Die zu überprüfende Software soll als Java-Bytecode vorliegen, das Rahmenwerk soll in Java geschrieben sein. Die praktische Verwendbarkeit des Rahmenwerks soll an einer Fallstudie überprüft werden.

Hierzu wollen wir eine Client-Server-Infrastruktur aufbauen, wobei die Clients, die die Programmüberprüfung durchführen auf mobilen Endgeräten, wie zum Beispiel Handys oder PDAs, laufen sollen. Aus der Ressourcenknappheit dieser Geräte ergeben sich weitere Anforderungen an das Rahmenwerk.

Das Praktikum kann gemeinsam mit dem "PCC-Seminar" im gleichen Semester besucht werden.


Folgen Sie dem Link zu den Internen Webseiten.

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang