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