5.3. Entwicklungsumgebungen für Formale Methoden

Software-Entwicklungsumgebungen (SEU's) sollen alle Phasen des Software-Lebenszyklus durch Werkzeuge unterstützen. Sie werden gewöhnlich dadurch entwickelt, daß existente Werkzeuge in einen Entwicklungs-Rahmen (z.B. HP SoftBench, Atherton Backplane oder der ECMA Standard PCTE) eingepaßt ("plugged in" - "eingesteckt") werden, der Basisdienste für die Steuerung, die Daten, die externe Darstellung und die Integration auf der Plattform anbietet. Die praktische Erfahrung in der Industrie zeigt, daß die Integration einer vollständigen Umgebung aufbauend auf einem solchen Rahmen extrem kostspielig ist, ebenso die Wartung. Werkzeuge sind nicht für die Integration entwickelt worden und habe nicht genau die Schnittstellen, die erforderlich sind; daher werden Adapter oder Filter meist mit sehr rudimentärer Technologie (C, LEX etc.) entwickelt.

So entsteht ein Bedarf für eine fortschrittlichere Technologie der Integration, auf einer höheren Ebene; diese Technologie sollte die Flexibilität eines "plug-in"-Ansatzes mit solchen Software-Engineering Paradigmen wie typsicheren Schnittstellen zwischen Werkzeugen verbinden. Neuere Forschung zeigt, daß eine höhere funktionale Sprache hier entschiedende Vorteile über die traditionalle Technologie bietet.

In diesem Projekt soll eine universelle Entwicklungsumgebung zur Verfügung gestellt werden, in der Werkzeuge zur Unterstützung formaler Methoden integriert werden; dies bedingt spezielle Anforderungen. Wie die Erfahrungen des Vorprojekts PROSPECTRA zeigen, sollten auch für die Entwicklung der Werkzeuge und der Umgebung wieder Formale Methoden einsetzbar sein. Dadurch wird die Einheitlichkeit erhöht und Teile des Systems können formal korrekt bewiesen werden. Mit einer höheren funktionalen Sprache wird ein Schritt in diese Richtung gemacht; so könnte auch (durch Parametrisierung höherer Ordnung) eine Plattform für schnelle Prototypisierung geschaffen werden.



Abbildung 5.3-1: Der KORSO Systemarchitektur-Rahmen

5.3.1. KORSO Systemarchitektur-Rahmen

Im Vorprojekt KORSO wurde, aufbauend auf dem KORSO Methodik-Rahmen [PW 94], ein KORSO Systemarchitektur-Rahmen [KM 94] entworfen. Es werden die speziellen Eigenschaften beschrieben, die eine Entwicklungsumgebung, die auf die Unterstützung formaler Methoden zugeschnitten ist, besitzen sollte.

Der KORSO Systemarchitektur-Rahmen existiert bisher nur auf dem Papier; allerdings sind weite Teile ähnlich wie in konventionellen CASE Umgebungen bzw. dem Europäischen Standard PCTE (Portable Common Tool Environment, [ECMA 93]). Die Systemarchitektur (vgl. Abb. 5.3-1) ist auch mit dem Referenz-Modell für Entwicklungsumgebungen ([VMOD], vgl. Abb. 5.3-2) direkt verträglich: grob entspricht der Subsystem Interaction Manager dem Toolbus, der User Interaction Manager der Benutzerschnittstelle, der Development Manager der Kombination aus den Schichten für Entwicklungssteuerung bzw. Sicherheits- und Integritätsanforderungen, der Repository Manager der Kombination aus dem Konfigurationsmanagement und der Schicht für die Objektverwaltung, etc.). Im folgenden soll auf die Eigenheiten, die sich aus der Verwendung formaler Methoden ergeben, näher eingegangen werden.



Abbildung 5.3-2: Das Referenz-Modell für Entwicklungsumgebungen

5.3.2. Datenbasisverwaltung

Objekte, strukturelle und semantische Relationen

Objekte, die am Entwicklungsprozeß beteiligt sind (sog. "Einheiten"), sind z.B. Spezifikationen, Programme, Beweisverpflichtungen und Beweise, Lemmata, Transformationen; sie alle müssen in einer Entwicklungs-Datenbasis repräsentiert werden [PW 94], [KM 94]. Dabei spielen in einem Entwicklungsgraphen die strukturellen Abhängigkeiten (z.B. Import, Erweiterung, Vererbung) und methodischen Relationen (z. B. Verfeinerung, Modifikation, Korrektheit eines Entwicklungsschrittes aufgrund eines Beweises) eine wesentliche Rolle; sie ersetzen die klassischen Versions- und Konfigurationsinformationen. Zusätzlich sollten Management-Informationen (z.B. Person des Entwicklers, beteiligtes Entwicklungswerkzeug) abgelegt werden.

Grafische Darstellung der Datenbasis

Der Entwickler sollte durch geeignete grafische Darstellung der Objekte und Relationen unterstützt werden, um sich auf das wesentliche konzentrieren zu können und die Übersicht nicht zu verlieren. Mit einer selektiven Visualisierung der Datenbasis wird es überhaupt erst möglich, sich auch bei sehr großen Entwicklungen im System zurechtzufinden. So können Strukturen besser und schneller erkannt werden, wodurch beispielsweise der Vorgang der Wiederverwendung erheblich unterstützt werden kann. Abb. 5.3-3 zeigt die Visualisierung eines kleinen Entwicklungsgraphen mit dem Visualisierungssystem daVinci: die Darstellung der strukturellen Abhängigkeiten der Teilspezifikationen (dünne Pfeile) sowie eines korrekten Entwicklungsschritts von SCAN nach SCAN1 durch Anwendung einer parametrisierten Transformationsregel SplitOfPostcondition SOPC(E,H), eine Beweisverpflichtung ScanSplit, etc. daVinci [FW 94, 95] ist in Bremen entstanden, öffentlich verfügbar und wird weltweit in vielen Projekten eingesetzt. Derzeit ist daVinci in der Lage, zyklische oder azyklische gerichtete Graphen automatisch in hoher Qualität zu visualisieren. Dabei werden verschiedene ästhetische Kriterien wie z.B. die Minimierung von Kantenkreuzungen berücksichtigt. Künftig werden auch verschiedenartige kontextsensitive grafische Darstellungen (z.B. Teilgraphen als geschachtelte "Boxen", als eingerückte Texte), die über Beschreibungsdefinitionen generiert werden, gleichzeitig in mehreren Sichten möglich sein, wobei immer alle Sichten interaktiv bearbeitet werden können.



Abbildung 5.3-3: Entwicklungsgraph, visualisert mit daVinci

5.3.3. Benutzungsoberfläche

Die KORSO Systemarchitektur sieht einen eigenen User Interaction Manager vor. Wichtig ist die konsequente Trennung von grafischer Darstellung auf der Oberfläche einerseits und Kommunikation mit dem benutzten Werkzeug andererseits, das völlig autonom die Semantik von Objekten etc. kennt und verwaltet. Nur durch eine solche Trennung wird es möglich, eine einheitliche Benutzungsschnittstelle zu realiseren, bei der jede Interaktion mit dem Benutzer protokolliert und kontrolliert werden kann (siehe Abschnitt 5.3.4, Abschnitt 5.3.5); alle Objekte müssen aber auch jederzeit interaktiv (im Dialog mit dem benutzten Werkzeug) über die Visualisierung manipuliert werden können. Mit daVinci kann eine solche einheitliche Benutzungsoberfläche realisert werden. So kann künftig auch auf die Inhalte von Objekten in der Datenbasis (z.B. abstrakte Syntaxbäume für Spezifikationen) zugegriffen werden.

5.3.4. Integration von Subsystemen und Werkzeugen, Interaktion

Integration von Subsystemen

Die KORSO Systemarchitektur ist eine offene Systemarchitektur, in die neue Werkzeuge oder Subsysteme integriert werden können. Dazu werden geeignete Kommunikationsprotokolle definiert (vgl. Abschnitt 5.3.4.), wobei besonders auf die Kontrolle der Korrektheit bei Interaktionen geachtet werden muß (vgl. Abschnitt 5.3.5.). Die hierarchische Darstellung in Abb. 5.3-1 weist besonders darauf hin, daß auch sog. "fremde Subsysteme" (d.h. existierende, die nur geringfügig oder gar nicht änderbar sind) eingebunden werden können; dann wird die Architektur rekursiv, da sich das Bild an der Stelle other Subsystem wiederholt, wobei der ursprüngliche Subsystem Interaction Manager nun mit dem neuen Subsystem Interaction Manager in der Instanz von other Subsystem kommuniziert (vgl. Abb. 5.3-4). Durch diese hierarchische Struktur wird die Lokalität der Interaktionen bzw. die jeweilige Verkapselung betont.



Abbildung 5.3-4: Fremdes Subsystem im KORSO Systemarchitektur-Rahmen

Verschiedene Formen der Verkapselung können auftreten: das fremde Subsystem (bzw. Werkzeug) hat

* keinen eigenen User Interaction Manager, hier kann die Interaktion mit dem Benutzer über dieselbe Schnittstelle mit dem selben "look and feel" abgewickelt werden; andernfalls muß die Benutzungoberfläche gewechselt werden und die Übertragung von einem Objekt in die andere "Welt" muß indirekt (nicht über die gemeinsame Oberfläche wie z. B. mit "cut-and-paste") erfolgen. Dabei ist zu beachten, daß in jedem Fall, auch wenn eine Übertragung auf einer einheitlichen Oberfläche "scheinbar" textuell mit "cut-and-paste" erfolgt, die Korrektheit der Interaktion durch einen Subsystem Interaction Manager bzw. Development Manager kontrolliert werden muß. Dieser Fall tritt z.B. auf, wenn eine Gleichung aus einem "Fenster" in einem anderen (zur Substitution, als Ersetzungsregel, etc.) eingesetzt werden soll: es muß geprüft werden, ob sie in dem Anwendungskontext überhaupt legal (d.h. sichtbar, ohne Umbenennung verwendbar, typkorrekt etc.) ist.

* keinen eigenen Repository Manager, Objekte und ihre Relationen (s.u. Abschnitt 5.3.2) können einheitlich verwaltet werden; andernfalls kann über die Schnittstelle nicht direkt auf Objekte zugegriffen werden und es können insbesondere keine Relationen direkt etabliert werden, u.U. muß eine eigene "Schattenstruktur" mit Kopien oder Platzhaltern verwaltet werden. Diese Problem tritt z.B. auf, wenn ein Beweiser lokal Lemmata (mit Beweisen) generiert, die zur Wiederverwendung auch in der zentralen (bzw. übergeordneten) Projektdatenbasis in Relation zu anderen Objekten abgelegt werden soll.

Formen der Kopplung

Die konventionelle Form der Integration von Werkzeugen (bzw. Subsystemen) ist die der engen oder losen Kopplung [YWA 92]. Die enge Kopplung (als neue Module einer Systemerweiterung) bringt einen hohen Integrationsaufwand mit sich und ist in der Regel nur möglich, wenn die Implementierungssprachen übereinstimmen. Die lose Kopplung (z.B über Unix-pipes oder einen "SW-System-Bus" niederer Ebene) ist sehr flexibel, hat aber den gravierenden Nachteil, daß auf statische Prüfungen, wie z.B. Typkorrektheit einer Kommunikation, verzichtet werden muß. Ein neues Integrations-Paradigma der dynamischen Kopplung wurde kürzlich vorgestellt [Karl 94a], das die lose Kopplung mit typ-sicherer Kommunikation verbindet. Dazu wird eine statisch getypte funktionale Programmiersprache um Konzepte der dynamischen Typüberprüfung [ACP 91, LM 91] und dynamisches Linken erweitert. So können alle Formen der Kopplung (ungekoppelt, eng, lose, dynamisch) in einem einheitlichen Rahmen zur Verfügung gestellt werden.

Verkapselung, Schnittstellen

Ein genereller Ansatz zur Verkapselung eines unabhängig entwickelten Werkzeugs ist der, daß man es mit einer Schnittstelle (als Abstrakter Datentyp) umgibt, die in einer Skript-Sprache definiert ist. Die Systemintegration wird dann in der Skript-Sprache definiert. Die entscheidende Charakteristik solcher Sprachen (z.B. TCL [Oust 93]) ist, daß Programm-Skripte eigene ("first-class") Werte sind, die zwischen Werkzeugen übertragen werden können. Dabei leidet allerdings die Effizienz erheblich (diese Sprachen werden interpretiert); außerdem sind sie fast ungetypt. Dagegen kann eine funktionale Programmiersprache mit den oben beschriebenen Erweiterungen [Karl 94a, b] als typsichere, effizient übersetzbare Skript-Sprache verwendet werden, in der Programm-Skripte streng-getypte persistente Werte sind. Dieser Ansatz verbindet die Vorteile von Skript-Sprachen mit denen funktionaler Sprachen (Typsystem, referentielle Transparenz, Strukturierungskonzepte wie parametrisierte Moduln) und (algebraischer) Spezifikationssprachen, so daß sogar über die Korrektheit von Kombinationen und Kommunikationen Beweise geführt werden könnten.

Kommunikationsprotokolle

Eine Methode der Integration von Werkzeugen in einer Entwicklungsumgebung ist die über einen toolbus mit selective broadcasting, eingeführt in der FIELD Umgebung [Reis 90] und später im BMS der HP SoftBench [Caga 90] sowie ToolTalk von Solaris [Sun 93] übernommen. Ein Ansatz mit Funktionen höherer Ordnung in einer funktionalen Sprache (vgl. Messenger in [Karl 94c]) bietet signifikante Verbesserungen: System- und Werkzeug-Typen werden in einer dedizierten Datenbasis verwaltet. Auf der Basis von typ-sicherer Kommunikation lose gekoppelter Systemteile können Muster für Botschaften in Form von persistenten Filterfunktionen definiert werden; dies führt zu einem ungewöhnlichen Grad von Ausdrucksfähigkeit. Eine prototypartige Implementierung von Messenger wird derzeit begonnen.

System als Netzwerk kommunizierender Prozesse betrachten.

ECMA Standard PCTE

Das Referenzmodell für die Basisfunktionalität einer Software-Entwicklungsumgebung ist der europäische Standard PCTE (Portable Common Tool Environment, [ECMA 93]). Im wesentlichen werden Konzepte für die Unterstützung von (persistenter) Datenhaltung, Transaktionsverwaltung , Benutzungsschnittstellen, Kommunikationsdiensten, verteilter Verarbeitung und Verwaltung von Entwicklungsprozessen definiert. Derartige Basisdienste sind in der Regel auf darunterliegenden Betriebssystemen realisiert; typische Dienste wie Datei-, Namens- und Prozeßverwaltung oder Ein/Ausgabe werden auch von der Umgebung selbst zur Verfügung gestellt.

5.3.5. Verwaltung von Entwicklungen

Entwicklungsskripte

Die Entwicklungsgeschichte nimmt im Systemarchitektur-Rahmen eine zentrale Rolle ein [KM 94], vgl. Abb. 5.3-3. Der (fett gezeigte) Verfeinerungspfeil (z.B. SCAN1 "wurde korrekt entwickelt aus" SCAN) repräsentiert gleichzeitig den Entwicklungsschritt, der von einer Version zur nächsten führt. Im allgemeinen handelt es sich um eine Folge von Schritten, eine (Teil-) Entwicklung (vgl. Abschnitt 5.1.4), z.B. eine Komposition von Transformationen; dies entspricht dem Skript von Aktionen, die ein Delta im Sinne konventioneller Versionsverwaltung erzeugen. Eine Entwicklung annotiert den Verfeinerungspfeil (vgl. SOPC in Abb. 5.3-3), mit allen abgehandelten Beweisverpflichtungen, z.B. ScanSplit, sowie dem Teilgraph der dazu notwendigen Informationen.

Kontrolle der Korrektheit bei Interaktionen

Im System zeichnet der Development Manager die Entwicklungsskripte auf, vgl. Abb. 5.3-1. Dabei (d.h. im Kontext der abgelaufenen Entwicklung) wird die Zulässigkeit eines Entwicklungsschritts überprüft, soweit dies nicht schon statisch bei der Systemintegration bzw. den dynamischen Prüfungen im Subsystem Interaction Manager geschehen ist (vgl. die getypte dynamische Kopplung etc. in Abschnitt 5.3.4). Hier wird im Sinne einer globalen Integritätsbedingung durch Beweis oder dynamische Überprüfung sichergestellt, daß z.B. ein Lemma nicht (zyklisch im Entwicklungsgraphen) von sich selbst abhängig ist.

Kontrolle in Bezug auf ein Vorgehensmodell

Ein Entwicklungsskript, bzw. die Gesamtheit aller Skripte im Entwicklungsgraphen, dient natürlich auch zur Dokumentation des Vorgehens. Es wäre interessant festzustellen, ob man syntaktische oder semantische (d.h. dynamisch zu überprüfende) Kriterien aufstellen kann, die die Konformität einer Entwicklung zu einem gegebenen (instantiierten) Vorgehensmodell garantieren; dies ist bisher noch nicht untersucht worden.

Wiederverwendung von formalen Entwicklungen

Zur abstrakten Entwicklung korrespondiert eine konkrete Folge von Operationen im Entwicklungssystem; man kann ein solches Entwicklungs-"Skript" als eine Verfeinerung betrachten. Diese Korrespondenz ist die Grundlage für die Wiederverwendbarkeit von Teil-Entwicklungen [HK 93, KLWS 93, KLSW 94, BK 95]; das Skript wird in eine Entwicklung umgewandelt ("geliftet") und kann dann als formales Objekt durch Pattern-Abstraktion, Parametrisierung etc. abstrahiert, algebraisch manipuliert und transformiert werden (vgl. Abschnitt 5.1.4). Eine solches abstraktes Entwicklungsschema kann dann durch Instantiierung in einer ähnlichen Situation nachvollzogen werden ("replay").