ELITE NETZWERK BAYERN

English  Sprachen Icon  |  Gebärdensprache  |  Leichte Sprache  |  Kontakt


Aktuelles aus den Elitestudiengängen

Vortrag „System Verified - Can we go to the Beach now?“

Im Rahmen des Elitestudiengangs Software Engineering hielt Dr. Peter Höfner von Data61 in Sydney am 11. April 2016 einen Vortrag über den Stand der Technik und der Forschung im Bereich der Softwareverifikation.

In seinem Vortrag „System Verified - Can we go to the Beach now?“ beschrieb Dr. Höfner zunächst, was in der Softwareverifikation in den letzten Jahren erreicht werden konnte: Von verifizierten Kommunikationsprotokollen über formal als korrekt bewiesene Dateisysteme bis hin zu voll verifizierten Betriebssystemen. Im Folgenden wurde die Frage erläutert, ob das bereits Erreichte genügt, um fehlerfrei arbeitende Software für die Benutzer zu garantieren. Dr. Höfner zeigte, dass dem nicht so ist. Für das fehlerfreie Arbeiten von Software sind viele Ebenen zu betrachten:

Stimmen die Requirements?
Entspricht die formale Spezifikation genau den informellen Requirements?
Ist die Implementierung in ihrem Verhalten äquivalent zum formalen Modell?
Erhält der Compiler die Semantik des Programms?
Führt die Hardware das compilierte Programm korrekt aus und verhalten sich alle Prozessorvarianten, Chipsätze usw. für das Programm gleich?

Bisher betrachten kein Verifikationsprojekt und keine Fallstudie alle diese Ebenen. Die Untersuchungen beschränken sich auf einen Ausschnitt all dieser Fragen, so dass selbst mathematisch bewiesene Korrektheit in den durch die Verifikation betrachteten Ebenen kein fehlerfreies Verhalten beim Einsatz der Software garantiert. In den nicht-betrachteten Ebenen können immer noch Fehler enthalten sein. Daher ist die Verifikationstechnik trotz großer Fortschritte noch lange nicht am Ziel und es verbleiben noch viele Forschungsfragen.

Text und Bild: ESG Software Engineering

veröffentlicht am