Von Sanduhren und Ladebalken: Alles Warten hat ein Ende

Dass die abstrakte Welt der höheren Mathematik ganz konkrete Auswirkungen auf den Alltag jedes Computernutzers hat, konnte jetzt ein internationales Forscherteam um den Freiburger Informatik-Professor Andreas Podelski unter Beweis stellen. Wer kennt nicht folgendes Problem: Ein Befehl, zum Beispiel zum Drucken eines Dokuments, wird abgeschickt, aber nichts passiert. Stattdessen erscheinen endlos ein Ladebalken oder eine Sanduhr auf dem Bildschirm. Die Lösung: die Mathematik des Unendlichen und ein eher zufällig entdecktes Resultat aus dem Jahr 1930.

Wenn man nach dem Absenden eines Befehls ewig warten muss und am Ende sogar der Computer ganz abstürzt, dann handelt es sich dabei um einen so genannten Terminierungsfehler im Betriebssystem des Computers. Genauer gesagt liegt der Fehler in dem Treiberprogramm, das den Befehl an den Drucker (oder ein anderes Gerät: Scanner, DVD-Laufwerk usw.) weitergibt. Gerätetreiber sind Programme, die z.B. von Microsoft als Teil des Betriebssystems Windows mitgeliefert werden.

Professor Podelski und sein Team stehen in engem Kontakt mit dem Forschungslabor von Microsoft in Cambridge, um an Problemen wie dem Terminierungsfehler zu arbeiten. Ein wichtiges Forschungsziel besteht darin, Terminierungsfehler auszuschließen. Bislang bestanden Qualitätskontrollen in der Entwicklung von Betriebssystemen und Gerätetreibern lediglich darin, möglichst viele Situationen zu simulieren. Die Anzahl der Faktoren, die beim Auftreten von Terminierungsfehlern eine Rolle spielen, ist jedoch sehr groß, und so werden nur die wahrscheinlichen Fälle getestet. Tatsache ist, dass auch die unwahrscheinlichen Fälle irgendwann einmal vorkommen.

Hier setzt die von Professor Podelski und seinem Doktoranden Andrey Rybalchenko neu entwickelte Methode an: Ausgehend von einem Resultat des englischen Mathematikers Sir Frank Ramsey aus dem Jahr 1930 entwickelten sie eine neue Mathematik des Unendlichen, aus der ein neuartiges Testwerkzeug hervorgeht. Stark vereinfacht handelt es sich dabei um eine neue mathematische Behandlung von nicht-terminierenden (mathematisch gesehen: unendlichen) Berechnungsabläufen des Computers.

Durch das neue Testverfahren konnten an einer Reihe von Gerätetreibern bereits Terminierungsfehler entdeckt und langfristig beseitigt werden – mit sichtbaren Ergebnissen für die Nutzer: Das immer wiederkehrende Problem, dass Befehle nicht ausgeführt werden, kann bei vielen gängigen Anwendungen nun ausgeschlossen werden. Noch ist die Zeit der Sanduhren nicht abgelaufen, aber dank des Freiburger Forscherteams wird das Glas nicht ständig von neuem umgedreht.

Kontakt:
Prof. Dr. Andreas Podelski
Albert-Ludwigs-Universität
Institut für Informatik
Georges-Köhler-Allee
79110 Freiburg
Tel. 0761-203 8241
podelski@informatik.uni-freiburg.de

Media Contact

Rudolf-Werner Dreier idw

Weitere Informationen:

http://www.uni-freiburg.de/

Alle Nachrichten aus der Kategorie: Informationstechnologie

Neuerungen und Entwicklungen auf den Gebieten der Informations- und Datenverarbeitung sowie der dafür benötigten Hardware finden Sie hier zusammengefasst.

Unter anderem erhalten Sie Informationen aus den Teilbereichen: IT-Dienstleistungen, IT-Architektur, IT-Management und Telekommunikation.

Zurück zur Startseite

Kommentare (0)

Schreiben Sie einen Kommentar

Neueste Beiträge

KI-basierte Software in der Mammographie

Eine neue Software unterstützt Medizinerinnen und Mediziner, Brustkrebs im frühen Stadium zu entdecken. // Die KI-basierte Mammographie steht allen Patientinnen zur Verfügung und erhöht ihre Überlebenschance. Am Universitätsklinikum Carl Gustav…

Mit integriertem Licht zu den Computern der Zukunft

Während Computerchips Jahr für Jahr kleiner und schneller werden, bleibt bisher eine Herausforderung ungelöst: Das Zusammenbringen von Elektronik und Photonik auf einem einzigen Chip. Zwar gibt es Bauteile wie MikroLEDs…

Antibiotika: Gleicher Angriffspunkt – unterschiedliche Wirkung

Neue antimikrobielle Strategien sind dringend erforderlich, um Krankheitserreger einzudämmen. Das gilt insbesondere für Gram-negative Bakterien, die durch eine dicke zweite Membran vor dem Angriff von Antibiotika geschützt sind. Mikrobiologinnen und…

Partner & Förderer