Computerwelt: Aktuelle IT-News Österreich


13.08.2015 pi/Rudolf Felser

TU Wien: International angesehener CAV-Award für Helmut Veith

Der Informatiker Helmut Veith von der TU Wien erhielt den prestigeträchtigen CAV-Award für computergestützte Verifikation.

Informatiker Helmut Veith von der TU Wien

Informatiker Helmut Veith von der TU Wien

© Philipp Horak

Computer machen Fehler, und Fehler sind ärgerlich. Weil kein Mensch ein kompliziertes Programm vollständig analysieren kann, wird diese Aufgabe heute automatisiert: Computerprogramme untersuchen, ob andere Computerprogramme (oder abstrakter ausgedrückt: logische Systembeschreibungen) korrekt sind. Prof. Helmut Veith vom Institut für Informationssysteme der TU Wien forscht seit Jahren mit großem Erfolg auf dem Gebiet Computer Aided Verification (CAV) und Model Checking. Nun erhielt er bei der internationalen CAV-conference gemeinsam mit sieben anderen Forscherinnen und Forschern mit dem CAV-Award, der als international angesehenste Auszeichnung auf diesem Gebiet gilt.

Ein Computerprogramm kann sich in vielen verschiedenen Zuständen befinden. Variablen können unterschiedliche Werte annehmen, und abhängig davon wechselt das Programm in einen neuen Zustand. Überprüft werden soll, ob bestimmte mathematisch formulierte Qualitätsanforderungen in jedem möglichen Zustand und jeder möglichen Programmausführung erfüllt werden. Solche Regeln können beispielsweise darin bestehen, dass das Programm niemals in einer unendlichen Schleife gefangen sein soll, aus der man nicht mehr herauskommt, oder dass bestimmte Werte der Variablen, die das Programm zum Absturz bringen würden, niemals angenommen werden dürfen.

Das System, das man untersuchen möchte, kann man sich wie ein riesiges Netz vorstellen. Jeder Knotenpunkt steht für einen bestimmten Zustand des Programms, und von jedem möglichen Zustand kann man eine bestimmte Anzahl weiterer Zustände erreichen. "Die einfachste Verifikationsmethode wäre es, die Zustände nacheinander zu durchlaufen und zu analysieren, ob es irgendwo zu Fehlern kommt", erklärt Helmut Veith. "Doch meistens ist die Anzahl der möglichen Zustände so groß, dass das völlig unmöglich ist." Mit dem verfügbaren Speicherplatz wächst die Anzahl der möglichen Zustände exponentiell an, daher können solche naiven Testverfahren nur Programme mit sehr kleinem Speicher analysieren. Man muss sich für die Praxis kluge Vereinfachungsstrategien überlegen.

ABSTRAHIEREN UND VERFEINERN

Gemeinsam mit einigen Kollegen entwickelte Helmut Veith vor etwa 15 Jahren das sogenannte "Counterexample-Guieded Abstraction Refinement" (CEGAR). Dabei wird das Computerprogramm, das untersucht werden soll, zunächst abstrahiert und vereinfacht, und dort wo es nötig ist, wird diese Abstraktion dann Schritt für Schritt verfeinert. "Wenn dann ein Zustand entdeckt wird, der gegen die Qualitätsanforderungen verstößt, muss man zunächst überprüfen, ob es sich tatsächlich um einen Fehler des Programms handelt, oder ob es bloß ein Artefakt aufgrund der Abstraktion ist", erklärt Helmut Veith. Ein echter Fehler wird gemeldet, ist bloß die Abstraktion am vermeintlichen Problem schuld, wird die Darstellung des Systems verfeinert und die Analyse geht weiter.

Model Checking spielt heute in der Industrie eine wichtige Rolle – sowohl im Bereich der Software als auch der Hardware-Erzeugung. Die CEGAR-Methode gilt als wichtiger Schritt, der die praktische Anwendung von automatisiertem Model Checking in der Industrie erst möglich gemacht hat.

Neben Helmut Veith wurden noch sieben weitere WissenschaftlerInnen mit dem CAV-Award ausgezeichnet – der Turing-Preisträger Edmund Clarke (Carnegie Mellon University), Orna Grumberg (Technion), Ronald H. Hardin, Somesh Jha (University of Wisconsin), Yuan Lu (Atrenta), Robert P. Kurshan (Bell Laboratories) und Zvi Harel (Technion). Übergeben wurden die Preise am 22. Juli.

Helmut Veith studierte an der TU Wien, wo er 1998 auch promovierte (Sub auspiciis praesidentis). Danach ging er an die Carnegie Mellon University in Pittsburgh (USA) und wechselte dann nach Deutschland – zunächst an die TU München, dann an die TU Darmstadt. Seit 2005 ist er Adjunct Full Professor an der Carnegie Mellon University (Pittsburgh, USA), und seit 2009 ist er Professor an der TU Wien. (pi)

Diesen Artikel

Bewertung:

Übermittlung Ihrer Stimme...
Noch nicht bewertet. Seien Sie der Erste, der diesen Artikel bewertet!
Klicken Sie auf den Bewertungsbalken, um diesen Artikel zu bewerten.
  Sponsored Links:

IT-News täglich per Newsletter

E-Mail:
Weitere CW-Newsletter

CW Premium Zugang

Whitepaper und Printausgabe lesen.  

kostenlos registrieren

Whitepaper

Kein Premium Inhalt vorhanden.

Aktuelle Praxisreports

(c) FotoliaHunderte Berichte über IKT Projekte aus Österreich. Suchen Sie nach Unternehmen oder Lösungen.

Zum Thema

  • Fabasoft AG

    Fabasoft AG Vereine und Verbände, Öffentliche Verwaltung, Medizin und Gesundheitswesen, Luft- und Raumfahrttechnik, Freie Berufe, Finanzdienstleistungen, Qualitätssicherung,... mehr
  • ELO Digital Office AT GmbH

    ELO Digital Office AT GmbH Mobile Lösungen und Applikationen, Dokumentenmanagement und ECM, Übernahme von Softwareprojekten, Systemintegration und Systemmanagement, Programmierung, Individual-Softwareentwicklung, IKT-Consulting,... mehr
  • SER Solutions Österreich GmbH

    SER Solutions Österreich GmbH Werbewirtschaft, Wasser- und Energieversorgung, Vereine und Verbände, Umweltschutz, Touristik, Personenverkehr, Öffentliche Verwaltung,... mehr
  • SEQIS GmbH

    SEQIS GmbH Qualitätssicherung, Expertensysteme, Tools, Security Audits, E-Commerce-Software, B2B Dienste und Lösungen, Übernahme von Softwareprojekten,... mehr

Hosted by:    Security Monitoring by: