Humboldt-Universität zu Berlin, Institut für Informatik, Prof. Dr. Holger Schlingloff
Block-Kurs "Algebraische Spezifikation von Software und Hardware"


Aktuelle Hinweise

Veranstaltungsunterlagen
Alle Foliensätze (C) M. Roggenbach, 2010. Verwendung gestattet nur für den prvaten eigenen Gebrauch; Weitergabe nur mit vorheriger schriftlicher Genehmigung!

Veranstaltungsankündigung

Der Kurs diskutiert Standard-Techniken der Spezifikation anhand konkreter Fragestellungen.

Zunaechst werden reaktive Systeme betrachtet, u.a. das Modellieren und Verifizieren einer Flugzeugmotor-Steuerung von Rolls-Royce in der Prozesslagebra CSP. Dann werden in der algebraischen Spezifikationssprache CASL Datentypen fuer konkreter verschiedene Anwendungsbeispiele (Telephon-Datenbank, Logische Gatter, von-Neumann Computer, Sortier-Algorithmen) modelliert und analysiert. Abschliessend wird die Integration von Daten- und Prozessspezifikation diskutiert: dazu wird ein realer Kreditkarten-Standard in der Sprache CSP-CASL formalisiert, verifiziert und getested.

Online-Übungen sowie der Einsatz von Werkzeugen zur Simulation, zum Modelchecken und zum Theorembeweisen geben der Veranstaltung einen praktischen Anstrich. Sollten ausreichend Laptops vorhanden sein, koennen diese Werkzeuge auch in den Online-Uebungen ausprobiert werden.

Die Veranstaltung ist (nach Absprache) prüfbar.

H. Schlingloff, 11.1.2010