26. Sommerschule Marktoberdorf: Funktionstüchtigkeit von Software sichern

(openPR) Vom 3. bis 14. August 2005 findet zum 26. Mal die Sommerschule Marktoberdorf statt. 84 Jungwissenschaftler aus 20 Nationen setzen sich zwei Wochen lang mit aktuellen Forschungsergebnissen zur Zuverlässigkeit von Software auseinander. Das Institut für Informatik der Technischen Universität München veranstaltet seit 1970 gemeinsam mit der Ludwig-Maximilians-Universität diesen Kongress mit finanzieller Unterstützung der NATO (Security Through Science Programme).

Vor allem in sicherheitskritischen Bereichen muss die Zuverlässigkeit einer Software gewährleistet sein. Softwareentwickler setzen dafür so genannte Theorembeweiser ein. Mit diesem sicheren Verfahren kontrollieren sie ihre Modelle, die dahinter stehende Logik und das Verhalten des entwickelten Softwaresystems mit Hilfe von mathematischen Beweisverfahren. Dieser Vorgang ist gerade bei großen Softwaresystemen so komplex, aufwändig und fehleranfällig, dass Computer die mathematischen Beweise übernehmen. Prof. Tobias Nipkow von der Fakultät für Informatik der TUM hat den Theorembeweiser Isabelle maßgeblich mitentwickelt und wird neueste Arbeiten auf der Sommerschule Marktoberdorf vorstellen. Die Industrie nutzt ebenfalls Theorembeweiser: Chiphersteller wie Intel oder Infineon verifizieren ihre Chips bereits während der Designphase und vermeiden so teure Fehlproduktionen.

Im gängigen Verfahren wird die Funktionstüchtigkeit einer bereits bestehenden Software mit einem Theorembeweiser geprüft. Der Softwareentwicklungsprozess kann aber auch umgekehrt verlaufen: Nachdem die Anforderung an eine Software bekannt ist, wird die Funktionalität mathematisch mit dem Theorembeweiser bewiesen. Erst dann wird daraus der Softwarecode extrahiert. Diese Methode hat bislang nur auf wissenschaftlicher Ebene Relevanz. Neben der Sicherstellung der Funktionalität der Software kann das Beweisprogramm überraschende Algorithmen zu Tag fördern.

Die Sommerschule Marktoberdorf dient jedoch nicht nur dem wissenschaftlichen Austausch. In entspannter Atmosphäre werden Kontakte für künftige gemeinsame Projekte geknüpft, die sich im Idealfall auch als Karrieresprungbrett entwickeln.


Kontakt
Ursula Eschbach
Technische Universität München
Institut für Informatik
Boltzmannstraße 3
85748 Garching