Proof-Carrying-Code (Lab)

Interne Webseiten 

Organisator: Prof. Dr. Heiko Mantel

Anmeldung: Anmeldungen nimmt Elisabeth Kraft entgegen. Falls Sie sie nicht antreffen sollten, wenden Sie sich bitte an Alexander Lux im Büro nebenan (S2-02-E317).

Literatur: Wird in der Vorbesprechung bekanntgegeben

Vorbesprechung: Donnerstag 3. April 2008 um 13:30 Uhr in S202/E202.

Vorwissen:

  • Programmieren in Java
  • Pflichtvorlesungen der ersten vier Semester Informatik

Wöchentlicher Termin: Dienstag, 13:00-14:30 Uhr (verschoben von 14:25-16:05 Uhr) in S202/E312.

Kontakt: Bei Fragen bitte an Alexander Lux oder Dieter Schuster wenden.

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.

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