Formale funktionale Methoden in der Entwicklung paralleler Programme

Die Entwicklung korrekter und zuverlässiger Softwaresysteme ist trotz verbesserter Programmierumgebungen immer noch schwer zu verwirklichen. Dies gilt insbesondere für parallele und verteilte Implementierungen, bei denen durch die Verteilung von Aufgaben und zugehörigen Daten sowie die angestrebte Effizienzsteigerung eine zusätzliche, für den Programmierer schwer zu überschauende Komplexität entsteht. Nachträgliche Programmverifikation zum Beweis, dass ein Programm die in der Spezifikation des Programms beschriebene Aufgabe erfüllt, kann nur für sehr einfache Programme durchgeführt werden.
 
Der Einsatz formaler Methoden bei der Programmentwicklung durch schrittweise Ableitung einer Implementierung aus einer gegebenen Spezifikation stellt eine anerkannte und vielversprechende Alternative dar. Die meisten formalen Methoden zur Programmentwicklung benötigen mehrere Sprachebenen. Die Verwendung einer funktionalen Programmiersprache als formales Entwicklungswerkzeug hat den Vorteil, dass nicht nur die abstrakte Spezifikation der Aufgabenstellung und die abschließende Implementierung in der gleichen ausführbaren Sprache beschrieben werden, sondern auch die Ableitungsschritte und die Beweisführungen zu den Ableitungsschritten.
 
Zur Trennung von Algorithmus und benutztem parallelem Programmiermodell wird der Ansatz einer Abstrakten Parallelen Maschine (APM) eingeführt, die Transformationen zwischen Programmiermodellen erlaubt. Die Hinzunahme einer Kostendimension erlaubt die Bewertung der Algorithmen bzgl. der unterschiedlichen APMs.

Das Projekt wird als ARC-Projekt gefördert.

Mitarbeiter

Computing Science Department, University of Glasgow
Dr. John O'Donnell
Fakultät für Informatik, Technische Universität Chemnitz
Prof. Dr. Gudula Rünger