Kolloquium Wintersemester 1998/99
Die Dozenten der Informatik
Prof. Dr. Bernhard Möller, Universität Augsburg
spricht über
Deduktiver Hardware-Entwurf - Ein algebraischer Ansatz
| Datum: | Montag, 19. Oktober 1998
| | Zeit: | 17:30 Uhr
| | Ort: | Hörsaal 1, Römerstraße 164
|
ZusammenfassungFormale Methoden dienen der Erstellung nachweisbar korrekter Soft- und Hardware. Ein spezieller Ansatz hierzu ist der deduktive Entwurf, bei dem eine korrekte Implementierung durch Umformung aus einer formalen Spezifikation gewonnen wird.
Formale Entwicklungen in reiner Prädikatenlogik erweisen sich oft als sehr unhandlich und unübersichtlich. Insbesondere ist die Manipulation von Quantoren aufwendig. Es zeigt sich aber, daß durch geschickte Definition geeigneter algebraischer Operatoren häufig auftretende Teilformeln eingekapselt und wesentlich leichter manipuliert werden können. Dies ermöglicht einerseits knappere und durchsichtigere Spezifikationen und andererseits übersichtlichere Entwicklungen, da oft viele kleine kleine Schlüsse auf der prädikatenlogischen Ebene zu einem einfachen algebraischen Gesetz in Gleichungs- oder Ungleichungsform über den Operatoren ersetzt werden können.
Wir zeigen Anwendungen auf Beschreibung und Entwurf von Hardware. Als konkrete Beispiele dienen einige systolische Schaltungen sowie ein algebraischer Nachweis der Korrektheit eines einfachen Befehlsfließbands.
(Der Vortrag findet statt anläßlich des 70. Geburtstages von em. Prof. Dr. Wolfgang Everling.)
Letzte Änderung:
6. Oktober 1998, 9:05:43
| 
.
Wintersemester 1998/99
Everling1
Meyer