Formale Software-Entwicklung

Seminar im Sommersemester 2007

Jeder Seminarteilnehmer hält einen 45-minütigen Vortrag (plus 15-minütige Diskussion) und erstellt dazu kommentierte Folien. Anwesenheit bei den anderen Vorträgen und Beteiligung bei der Diskussion ist verpflichtend. Die Vorträge finden wie folgt statt (alle Räume im Informatik-Hauptgebäude 50.34):

• Donnerstag, 12.7. vormittags (Raum -109):
  • 9.00 Sebastian Buchwald: Generische Klassen in Java 5
  • 10.00 Helmi Jouini: "Type Erasure" in Java 5
  • 11.00 David Dueck: BLAST
  • 12.00 Simon Greiner: Autotest
• Donnerstag, 12.7. nachmittags (Raum -107):
  • 14.00 Jonathan Dees: Ada Einführung
  • 15.00 Ingmar Wirths: Ada SPARK95
  • 16.00 Erik Burger: RTSJ
• Freitag, 13.7. vormittags (Seminar Theorie und Anwendung von Model Checking, Raum -108):
  • 9.00 Daniel Bruns: Grundlagen Model Checking
  • 10.00 Markus Kuderer: Uppaal Theorie
  • 11.00 Christoph Scheben: Das Uppaal Tool
  • 12.00 Jonida Saqe: PRISM: Theorie probabilistischer Modellprüfung
• Freitag, 13.7. nachmittags (Raum -108):
• 14.00 Hilal Akbaba: Spec# Einführung
• 15.00 Stefan Hartte: Spec# Boogie

Hinweise für gute Seminarvorträge:

• A. Zeller: Der perfekte Seminarvortrag
• F. Mattern: Seminarvortrag - Hinweise zur Präsentation

Materialien:

1. AADL, ''The Architecture Analysis and Design Language''
   • AADL Einführung
   • Weitere Informationen: AADL Webseite, Publikationen zu AADL


2. Ada, eine Programmiersprache
   • 1. Vortrag: Ada Reference Manual
   • 2. Vortrag: Ada Ravenscar Profile, Guide for the use of the Ada Ravenscar Profile in high integrity systems
   • 3. Vortrag: SPARK 95
   • Weitere Informationen: Webseite mit frei erhältlichen Büchern über Ada, SPARK Webseite


3. Autotest, automatisches Testen basierend auf Design by Contract
   • Autotest Webseite
   • Weitere Informationen: TestStudio, Automatic Testing Based on Design by Contract, Test Wizard: Automatic test case generation based on Design by Contract


4. BLAST, ''a software model checker for C programs''
   • Checking Memory Safety with Blast
   • Weitere Informationen: BLAST Webseite


5. Daikon, ''an implementation of dynamic detection of likely invariants''
   • Dynamically Discovering Likely Program Invariants to Support Program Evolution
   • Weitere Informationen: Daikon Webseite


6. Java 5 Typsystem
   • 1. Vortrag: Generische Klassen in Java 5 und ihre Auswirkungen auf das Typsystem
     Material: u.a. Adding Wildcards to the Java Programming Language"
   • 2. Vortrag: "Type Erasure" - Motiviation, Folgen, Abhilfen
     Material: u.a. Efficient First-Class Generics on Stock Java Virtual Machines", the NextGen project


7. Javolution, ''The Java Solution for Real-Time and Embedded Systems''
   • Javolution Webseite


8. RTSJ, ''Real-Time Secure Java''
   • RTSJ Webseite
   • The Real-Time Specification for Java


9. Spec#, ''a new attempt at a more cost effective way to develop and maintain high-quality software''
   • 1.Vortrag: The Spec# Programming System - An Overview
   • 2. Vortrag: Boogie - A Modular Reusable Verifier for Object-Oriented Programs
   • Weitere Informationen: Spec# Webseite, Weakest-Precondition of Unstructured Programs