Automatische Erzeugung von Prototypen verteilter Anwendungen aus cTLA-Spezifikationen

摘要

Ein produktiver formaler Entwurf realistischer verteilter Anwendungen wird in der Regel nur mit Werkzeughilfe möglich sein. In einem formalen, korrektheitsgesicherten Entwurf ist der letzte Schritt der Übergang vom formalen Modell in eine konkrete Implementierung. Diese Umsetzung einer Spezifikation in eine Menge von auf konkreten Plattformen verteilt ablaufenden, zusammenwirkenden Programmen soll aus Qualitätsgründen möglichst automatisch ablaufen. In diesem Beitrag stellen wir die automatische Übersetzung von hinreichend detaillierten Spezifikationen verteilter Anwendungen in ablauffähige C++-Programme vor. Die Spezifikationen liegen in der in Dortmund entwickelten prozeßorientierten kompositionalen Variante von Leslie Lamports TLA [9]: cTLA [7] vor. Hinreichend detailliert bedeutet in diesem Zusammenhang auch die Einbindung konkreter Plattformelemente (APIs, Bibliotheken), die die Anwendung in korrekter Weise, also in richtiger Reihenfolge und mit richtiger Parametrisierung, ansteuern muß.