Die Allgegenwärtigkeit von Mehrkern-Rechnerarchitekturen und Cloud Computing fordern von heutigen Software-Entwicklern, mehr und mehr Programmcode für komponenten-basierte Software zu schreiben. Dabei werden Komponenten entweder lokal nebenläufig ausgeführt oder laufen verteilt über ein Netzwerk und kommunizieren mittels asynchronem Nachrichtenaustausch untereinander. Da die so aus Komponenten gebauten Softwaresysteme auch immer häufiger in sicherheitskritischen Bereichen eingesetzt werden, müssen sie a priori robust und zuverlässig sein, sodass der mathematische Nachweis der Programmkorrektheit zu einer entscheidenden Aufgabe der Softwaretechnik wird.

Dieses Forschungsprojekt entwickelt formale Modelle für state-of-the-art Programmierparadigmen und APIs, wie beispielsweise Grand Central Dispatch, die es Programmierern ermöglichen, direkt asynchronen und nebenläufigen Programmcode zu schreiben. Ziel ist es, Softwaretechniker dabei so zu unterstützen, dass bereits durch die Art der Programmentwicklung die Korrektheit der Software garantiert ist.  Grundlegende Forschungsergebnisse hierzu basieren auf neuartigen, formalen Modellen der Automatentheorie und der Graphersetzungssysteme; das Projekt fokussiert auf die Entwicklung von (Semi-)Algorithmen zur automatischen Verifikation auf der Basis neuartiger Abstraktionstechniken. Langfristiges Ziel sind innovative algorithmische Ansätze zur automatischen Synthese, insbesondere im Kontext der lokalen und verteilten Synthese von Schedulern, welche auf Ideen der Spieltheorie (z. B. nebenläufige Imperfect Information Games) und des maschinellen Lernens (z. B. Unsupervised Gray/Black-Box Learning) zurückgreifen.

Partner dieses Forschungsprojekts sind Dr. Grégoire Sutre (LaBRI Bordeaux, Frankreich), Dr. Tristan Le Gall (CEA Saclay, Frankreich), Prof. Jean-Francois Raskin und Dr. Gilles Geeraerts (ULB Brüssel, Belgien), sowie Dr. Chris Poskitt (ETH Zürich, Schweiz).

Kontakt: Dr. Alexander Heußner

Publikationen:

• Geeraerts, G., Heußner, A. und Raskin, J.-F. Queue-Dispatch Asynchronous Systems. 13th Intl. Conf. on Application of Concurrency to System Design (ACSD 2013), S. 150-159, Barcelona, Spanien, Juli 2013. IEEE.
• Heußner, A., Le Gall, T., Sutre und G. McScM: A general framework for the verification of communicating machines. In C. Flanagan und B. König, Hrsg., 18th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), Band 7214 der Serie Lecture Notes in Computer Science, S. 478-484, Tallinn, Estland, März 2012. Springer-Verlag.
• Heußner, A., Leroux, J., Muscholl, A. und Sutre, G. Reachability analysis of Communicating Pushdown Automata. Logical Methods in Computer Science, 8(3), 2012.