Endlich Bug-frei mit Formaler Verifikation

Termin: Sonntag, 16:00 - Raum V5 - Dauer 60 Min.

Schon 1961 schlug John McCarthy, Turing-Award Gewinner und Autor, der den Begriff der Künstlichen Intelligenz prägte, folgendes vor:

„Instead of debugging a program, one should prove that it meets its specification, and this proof should be checked by a computer program.“

Nach nun 60 Jahren seit McCarthys Aussage ist Software ein stetig wachsender und integraler Bestandteil unseres täglichen Lebens sowie kritischer Infrastruktur, u. a. in medizinischen Geräten, Automobilen usw. Solche kritischen Systeme werden umfangreicher, komplexer und bestehen aus Zehntausenden bis Millionen Zeilen Code.

In diesem Vortrag wird gezeigt, warum eine formale Verifikation mit mathematischer Genauigkeit selbst bei kleinen Algorithmen nötig ist. Dazu wird die Programmiersprache Ada/SPARK 2014 präsentiert, die es erlaubt, effiziente und fehlerfreie Software zu entwickeln. Insbesondere gelingt dies, indem der Quelltext durch eine Spezifikation angereichert und anschließend mithilfe automatischer sowie interaktiver Theorembeweiser verifiziert wird.

Zum Schluss wird die Komponenten-basierte Softwarearchitektur anhand des Praxisbeispiels des Kryptotelefons SINA Communicator H präsentiert. Diese Architektur, die unter anderem auf dem Open Source Seperationkernel Muen sowie Linux basiert, erlaubt es, sicherheitskritische Eigenschaften eines Gesamtsystems zu zeigen.

Cloud-Pad für Publikumsinteraktion: Pad

Video-Aufzeichnung:

Creative Commons Lizenzvertrag Download MP4 (251 MiB)