Preisverleihung: Heinz Zemanek-Preis 2006

"Reasoning about Specifications in Model Checking" ausgezeichnet

HANIVAL Internet

Wien (pts010/01.12.2006/09:26) Die Preisverleihung des Heinz Zemanek-Preises 2006 fand im Rahmen der Konferenz Semantics2006 am 28.11.2006 in Wien im TechGate Vienna statt.

Der Heinz Zemanek-Preis wird alle 2 Jahre vergeben. 2006 wurde er erstmals für 2 Kategorien ausgeschrieben. Kategorie A für Dissertationen und Kat. B für sonstige Forschungsarbeiten (z.b: Habilitationen). Der Heinz Zemanek-Preis 2006 in der Kategorie an geht an Dr. Marko Samer (TU Wien) für die Dissertation mit dem Titel "Reasoning about Specifications in Model Checking". Im Alltag sind wir ständig mit automatisierten Systemen konfrontiert, deren mögliche Fehlfunktion mit hohen Kosten verbunden ist oder sogar Menschenleben gefährden kann.

Beispiele für derart kritische Systeme sind Flug- und Eisenbahnkontrollsysteme, Automobilelektronik, medizinische Instrumente, Steuerungen von Atomkraftwerken, Finanztransaktionssysteme, Telekommunikationssysteme usw. Aus diesem Grund befassen sich Informatiker auf dem Gebiet der Formalen Methoden mit Verifikationstechniken, die es erlauben, subtile logische Fehler in solchen Systemen mit Hilfe des Computers zu finden. Dr. Samer (geb. 1977) verfasste seine Dissertation unter der Betreuung von Prof. Helmut Veith (TU München, Carnegie Mellon) und Prof. Georg Gottlob (Oxford, TU Wien) am Institut für Informationssysteme der TU Wien. Im Zentrum seiner Dissertation steht die praxiserprobte Verifikationstechnik Model Checking. Model Checking ist ein aktuelles Forschungsgebiet der Informatik im Schnittbereich zwischen Grundlagenforschung und Anwendung und wurde mittlerweile von führenden Industrieunternehmen, wie etwa Intel, IBM, Microsoft und Siemens, als Schlüsseltechnologie erkannt.

Wird beim Model Checking ein Fehler gefunden, so liefert der Computer eine Fehlerbeschreibung zurück, mit deren Hilfe das untersuchte System korrigiert und einer erneuten Prüfung unterzogen werden kann. Dieser Vorgang kann so lange wiederholt werden, bis kein Fehler mehr gefunden wird. Dabei kann es passieren, dass das System - obwohl noch fehlerhaft - alle formalen Anforderungen erfüllt, aber nur deshalb, weil diese unvollständig spezifiziert sind und nur erwartete Fehler abdecken. In praktischen Anwendungen kommt dieser Fall relativ häufig vor und ist immer ein Hinweis auf ein ernstzunehmendes Problem. In seiner Dissertation hat Dr. Samer einen neuartigen Zugang zur Lösung dieser Problematik aufgezeigt und systematisch untersucht. Dazu hat er eine mathematische Beschreibungsmethode und Algorithmen entwickelt, die auf sogenannten temporallogischen Queries basieren. Mit diesen können nicht nur erwartete Eigenschaften des untersuchten Systems nachgewiesen werden, sondern der Computer berechnet "intelligent" bislang unbekannte Eigenschaften des Systems. Die Resultate der Dissertation wurden bei mehreren internationalen wissenschaftlichen Konferenzen publiziert.

In der Kategorie B wählte die Jury die Habilitaion von Priv.Doz. Dr. Helwig Hauser "Generalizing Focus+Context Visualization" aus.

Fokus+Kontext Visualisierung: gezieltes Fokussieren, ohne den Kontext zu verlieren
Überall dort, wo aufgrund von Umfang und Komplexität die gleichzeitige Darstellung aller Daten scheitert, ist es für eine tiefgehende Datenanalyse notwendig, den BenutzerInnen flexible Interaktionsmöglichkeiten einzuräumen, so dass sie gezielt auf ausgewählte Teile des Datenbestandes fokussieren können. Anwendungsbeispiele sind die Fokus+Kontext Visualisierung medizinischer 3D-Daten, z.B. aus der Computertomographie, großer Datensätze aus der Strömungssimulation, sowie von Daten aus großen Datenbanken. Traditionell werden hierfür Selektions- und Zoomtechniken eingesetzt - einzelne Teile der Daten werden für die Visualisierung ausgewählt und dann vergrößert dargestellt; der Rest der Daten wird dabei aber unbeachtet gelassen. Beim selektiven Zoomen über mehrere Größenordnungen hinweg (10fach-Zoom oder mehr) laufen jedoch die BenutzerInnen Gefahr, die Orientierung im Datensatz zu verlieren bzw. die vergrößerten Details nicht mehr im Kontext der restlichen Daten wahrnehmen zu können. Genau hier hakt die Fokus+Kontext Visualisierung (focus+context visualization) ein: mittels moderner graphischer Differenzierungstechniken wird es möglich, tiefgehende Einblicke in Details selbst sehr grosser Datensätze zu bekommen, ohne dabei den Kontext zu verlieren. Dies führt zu mehr Effizienz bei der Datenanalyse durch verbesserte Orientierung und Navigation in den Daten.

Die Preise wurden von der Juryvorsitzenden Univ.Prof.Dr. Gerti Kappel und Univ.Prof.Dr. Heinz Zemanek überreicht.

Aussender:	Oesterreichische Computer Gesellschaft (OCG)
Ansprechpartner:	Mag. Christine Haas
Tel.:	01/512 02 35 /51
E-Mail:	hass@ocg.at