Die historisch frühere und eine immer noch weit verbreitete Form ist die der modell-orientierten Spezifikation. Hier wird ein System mithilfe von bekannten Datenstrukturen wie Tupeln, Listen, Mengen, endlichen Abbildungen etc. modelliert, vgl. die Vienna Definition Method VDM sowie ihren Ableger Raise, ferner die mengentheoretische Spezifikationssprache Z [Spi 89], die an der Universität Oxford entwickelt wurde. Z hat sich in einer Reihe von Fallstudien [Hay 87], auch im industriellen Kontext, bewährt. Dazu trägt insbesondere der Z-Schema-Kalkül zur Modularisierung größerer Spezifikationen bei.
Der Vorteil der anschaulichen Modellierung wird damit erkauft, daß man immer ein konkretes Modell spezifiziert; es fällt so oft schwer, die Äquivalenz zu einem anderen Modell zu zeigen. Demgegenüber versucht man mit mehr axiomatischen bzw. algebraischen Spezifikationsmethoden, zunächst nur die notwendigen Eigenschaften eines Systems (oder Abstrakten Datentyps) festzuhalten; Überspezifikationen werden so vermieden und Freiheitsgrade für die Implementierung offen gehalten. Die erste formale Anforderungsspezifikation ist so oft noch nicht ausführbar, ermöglicht aber schon, formale Aussagen über das zu entwickelnde System abzuleiten. Sie wird schrittweise durch Verfeinerung über konkretere Entwurfsspezifikationen zu einer Implementierung entwickelt. Beispiele sind in [BKLOS 91] zu finden; ein Repräsentant ist das im BMFT-Vorprojekts KORSO entwickelte SPECTRUM (vgl. Beiträge in [BJ 94]).
Das Überprüfen von Spezifikationen in bezug auf das gewünschte Verhalten, spezielle Eigenschaften, etc. wird als Validieren bezeichnet (vgl. Abschnitt 5.2.3); man kann es auch als a-priori-Testen einer Spezifikation betrachten, gegenüber dem a-posteriori Testen eines Programms nach seiner Entwicklung. Hier sind die formalen Spezifikationen eine wesentliche Grundlage. Aus ihnen können nicht nur (oft zur Abnahme noch verlangte) a-posteriori Tests erzeugt werden, sie sind auch Eingabe für Prototypgeneratoren oder Animations- bzw. Simulationswerkzeuge. Eine besondere Rolle spielen hier direkt ausführbare Spezifikationen, z.B. operationell definierte aber noch ineffiziente Entwurfsspezifikationen; vgl. auch neuere Arbeiten zu "higher-order logic programming" [Qian 94] bzw. generell funktionale bzw. logische Programmiersprachen.
Der Entwurf von kommunizierenden, verteilten Systemen ist schwierig, weil gleichzeitig Phänomene wie Nebenläufigkeit, kausale Abhängigkeiten, Synchronisation, interne und externe Aktionen sowie Nichtdeterminismus beherrscht werden müssen. Dieses macht die Frage nach der Korrektheit solcher Systeme um so dringlicher. Um diese Schwierigkeiten zu meistern, sind viele Spezifikations-Formalismen für kommunizierende Systeme vorgeschlagen worden, die sich nach dem Abstraktionsgrad gruppieren lassen, mit dem sie die Details der Kommunikation und der verteilten Organisation wiedergeben:
* Eine "Black Box"-Sicht beschreiben logische Sprachen wie zum Beispiel Temporale Logik [MP 91] oder Prädikatenlogik [Heh 84, Hoa 85b, Bro 92].
* Mehr Details beschreiben Petri-Netze [Rei 85] und State Charts [Har 87] oder auch Action Systems [Bac 90, Lam 91], UNITY-Programme [CM 88] und Input/Output-Automaten [LT 89].
* Eine "Glas Box"-Sicht beschreiben Programmiersprachen wie CSP [Hoa 85a] und OCCAM [IN 88] oder Hardware-Entwürfe.
Da Entwürfe von kommunizierenden Systemen meistens mehrere solcher Abstraktionsebenen involvieren, muß der semantische Zusammenhang und der korrekte Übergang zwischen diesen Ebenen nachgewiesen werden. Diesem Ziel widmet sich insbesondere das ESPRIT-Grundlagenprojekt ProCoS (Provably Correct Systems) [Bjo 89, ProCoS 94].
Die wissenschaftlichen Anstrengungen zur formalen Behandlung solcher Systeme sind in letzter Zeit stark angewachsen. Dieses läßt sich insbesondere an Konferenzen ablesen, die sich speziell diesem Thema widmen, z.B. [BHRR 92, LRV 94].
Zur formalen Spezifikation von Realzeitsystemen ist häufig die Erweiterung der unter Abschnitt 5.1.2 genannten Spezifikationsmethoden um einen expliziten Parameter für die Zeit vorgeschlagen worden. Diese in [AL 92] als "old-fashioned recipe" bezeichnete Vorgehensweise findet sich z.B. in dem Verifikationskalkül von [Hoo 91] für zeitkritische kommunizierende Programme.
Erweiterte Temporale Logiken zur automatischen Verifikation von Automaten mit Zeitbedingungen werden in [AD 92, ACD 90] betrachtet. Ansätze der Prozeßalgebra für die Spezifikation von Realzeitabläufen werden in [BB 90] und [NSY 91] vorgeschlagen.
Diese Ansätze stellen den Verifikationsaspekt von fertigen Systemen in den Vordergrund. Wie diese Systeme aus gegebenen Anforderungen schrittweise entwickelt werden können, wird nicht behandelt. Methoden für diese Aufgabe werden u.a. im ProCoS-Projekt entwickelt.
Eine spezielle Logik zur Spezifikation von Realzeitsystemen ist der Duration Calculus [ZHR 92]. Der Duration Calculus basiert auf einem sehr einfachen semantischen Modell, dem der zeitabhängigen Zustandsvariablen. Der Kalkül selber kombiniert Intervall-Temporal-Logik mit dem Integral-Kalkül zur Bestimmung von Zeitdauern. Dadurch ergeben sich Ausdrucksmöglichkeiten, die in herkommlichen Temporalen Logiken für Zeit nicht gegeben sind. Besonders hervorzuheben ist, daß im Duration Calculus die Zeit nicht mehr als expliziter Parameter auftritt.
Im ProCoS-Projekt wird der Duration Calculus zur Spezifikation von Systemanforderungen eingesetzt und dient dann als Ausgangspunkt zur schrittweisen Entwicklung einer Implementierung [RRH 93, ProCoS 94]. Der Ansatz einer schrittweisen Verfeinerung von Realzeitsystemen wird auch in [SZH 94] verfolgt.
Die Spezifikationssprache SPECTRALSPECTRAL [KS 91] ist ein Ansatz, um mit möglichst wenig Konzepten sowohl Spezifikation im kleinen (einzelne Moduln) als auch Spezifikation im großen (Komposition) zu behandeln. Sie ist eigentlich eine Sprachfamilie, denn sie dient als Rahmen, in der verschiedene Logiken im kleinen realisert werden können, und damit auch heterogene Spezifikationen beschrieben werden können.
Die Forderung nach einem logischen Rahmenwerk, in dem Logiken so abstrakt beschrieben werden können, daß Strukturierung und Komposition ("Entwicklung im großen") unabhängig von den verschiedenen Logiken der Komponenten ("im kleinen") definierbar wird, liegt nahe. Zusätzlich soll die abstrakte Beschreibung sowohl für die Belange einer geeigneten Semantikdefinition als auch die Belange des Beweisens (von Hand oder mit Systemunterstützung) geeignet sein. Ferner sollte die Strukturierung von Spezifikationen auch zu einer davon abgeleiteten Strukturierung von Beweisen führen, um Einzelbeweise möglichst getrennt voneinander führen und evtl. wiederverwenden zu können (analog zur getrennten Übersetzung). Zusammengefaßt entsteht also der Bedarf nach multi-logischen Systemen, nach gegeigneten Abbildungen zwischen Logiken zum Notations- (evtl. Semantik- oder Paradigmen-) Wechsel und nach Abstraktion durch Parametrisierung. Liu hat, aus praktischen Erfahrungen im PROSPECTRA-Projek motiviert, in [Liu 94] ein solches logisches Rahmenwerk entwickelt, allgemeine Eigenschaften bewiesen und es als Erweiterung eines Logical Frameworks definiert. Im Unterschied zu "institutions" [GB 84, 92] basiert sein Ansatz zur Logikunabhängigkeit nicht auf der Erfüllbarkeitsrelation sondern der Konsequenzrelation; damit kann er sowohl modell-basierte semantische als auch Beweisaspekte abdecken.
Zusätzlich zu einer reinen Logikpräsentation, also der Darstellung einer Logik in einer Meta-Logik, wie sie in Logical Frameworks vorliegt (z.B. [HHP 87]) werden Logikmorphismen definiert. Die Strukturierung der Theoriepräsentation führt zu einer Strukturierung der Beweiskonstruktion, damit zu getrennter Beweisführung und Wiederverwendbarkeit. Wichtig ist vor allem auch die Definitionsmöglichkeit von anwendungsspezifischen Verfeinerungsrelationen zwischen strukturierten Theorien; so kann ein korrekter Entwicklungsschritt anwendungsabhängig von spezifischen Logiken definiert werden, auch von einer (abstrakteren) Logik in eine andere (konkretere), z.B. als Transformationsschritt von einer nicht-ausführbaren in eine ausführbare Spezifikation (vgl. Duration Calculus und CSP). Eine Verfeinerungsrelation zwischen Komponenten einer Spezifikation kann zu einer Verfeinerungsrelation auf der gesamten Spezifikation erweitert werden.
Es wird erwartet, daß sich durch die Strukturierungsmöglichkeiten, z.B. Verfeinerung und Parametrisierung, das Problem der Kombination von Methoden bzw. der unterliegenden Logiken strukturieren und leichter lösen läßt. So ist z.B. zur Kombination von zwei Semantiken (bzw. Logiken) nicht unbedingt (wie im klassischen Ansatz) die Konstruktion einer gemeinsamen Semantik notwendig, sondern nur die axiomatische Spezifikation der Gemeinsamkeiten; beide Logiken müssen dann diese Spezifikation im Sinne der Verfeinerungsrelation erfüllen.
Aufbauend auf den Erfahrungen des ESPRIT Projekts PROSPECTRA (siehe [Kri 90a, 91, KKLT 91, KKT 92] sowie den Sammelband [HK 93]) wurde im Bremer Teil des BMFT-Vorprojekts KORSO (siehe [Kri 94a, b]) ein einheitlicher semantischer Rahmen für Transformation und Verifikation entwickelt, der nicht nur den Beweis der Korrektheit einer Transformationsregel (analog zu einer Beweisregel) auf der Meta-Ebene erlauben soll, sondern auch eine Strukturierung durch Abstraktion von der unterliegenden speziellen Semantik/Logik der Objektsprache (vgl. die Multi-Logik Systeme in Abschnitt 5.1.3); Ziel ist, daß so nicht der gesamte Satz von Transformationsregeln für jede Objektsprache neu entwickelt und bewiesen werden muß, sondern nur die korrekte Instantiierung bzgl. einer speziellen Objektsprache.
Eine erfolgreich angewandte Methode, Programme in Maschinencode oder sogar Hardware zu transformieren, ist der "Normalform-Ansatz" aus Oxford [HHS 93, HZ 93]. Die Idee ist, in der Programmiersprache eine Normalform zu definieren, die quasi direkt in der gewählten Maschinensprache oder Hardware zu realisieren ist. Anschließend sind Transformationen anzugeben, die ein beliebiges Programm der Programmiersprache in kompositioneller Weise in diese Normalform bringen. Die taktische Kombination dieser Transformationen liefert dann einen Übersetzer von Programmen in Maschinencode bzw. Hardware.
Die ursprüngliche Motivation für CASE bestand in der Auffassung, daß semi-formale Beschreibungstechniken die mangelnde Präzision natürlich-sprachlicher Dokumente deutlich verbessern würden, ohne eine "Hemmschwelle" für Software-Entwickler darzustellen, wie sie etwa bei der Anwendung rein mathematischer Spezifikationssprachen festzustellen ist.
Nach anfänglicher CASE-Euphorie in den 80er Jahren ist heute ein deutliche Ernüchterung bei den Industrieanwendern eingetreten. Hierfür sind vor allem folgende Gründe zu nennen:
* Die von den CASE-Tool Vertreibern versprochenen Produktivitätssteigerungen (man sagte ursprünglich Steigerungen um etwa einen Faktor 5 voraus) sind drastisch geringer ausgefallen als erwartet (man spricht heute von etwa 15%-20%)
* Die Unzufriedenheit der Entwickler bei der Anwendung der Methoden is groß. Ein wichtige Ursache hierfür besteht darin, daß der semi-formale Charakter der Methoden an vielen Stellen der Spezifikation Eindeutigkeit suggeriert, in Wirklichkeit jedoch semantisch unscharf ist. Praktisch resultiert dies in Mißverständnissen zwischen den Entwicklern und zwischen Hersteller und Kunde, wenn diese das CASE-Dokument als Kommunikationsgrundlage verwenden.
* Die Anschaffungs- und Wartungskosten für etablierte CASE-Werkzeuge sind so hoch, daß die tatsächlich zu erwartende Produktivitätssteigerung erst sehr spät zu einem Return of Investment führt.
Mit dem Ziel einer Produktivitätsverbesserung werden heute mehrere objekt-orientierte Varianten der CASE-Methoden weiter verfolgt.
Um den Nachteil der unzureichenden Präzision zu überwinden, sind in den letzten Jahren in der Forschung Anstrengungen unternommen worden, CASE Methoden durch Kombination mit formalen Methoden zu semantisch eindeutigen Beschreibungssprachen zu machen. Für die bekanntesten CASE Methoden sind etwa folgende Arbeiten zu nennen:
* In [Br 91] wurden Bestandteile der CASE Methode SDL (Specification and Description Language) formalisiert. SDL wird hauptsächlich im Telekommunikationsbereich angewandt.
* Für Harels State-&Activitycharts wurden Semantiken in [HPPSS 87, KP 92, Hu 91] definiert. State-&Activitycharts werden heute zunehmend bei der Entwicklung von embedded Systems angewandt.
* Für Strukturierte Methoden (Strukturierte Analyse, Real-Time Analysis, Information Modelling, Strukturiertes Design, [DeM 79, HP 88, WM 85]) wurden Formalisierungen durch die Antragsteller entwickelt, vgl. Abschnitt 6. Strukturierte Methoden sind heute im industriellen Bereich die am weitesten verbreiteten CASE Verfahren.
Derzeit fehlen dem Anwender noch entscheidende Möglichkeiten, diese Forschungsergebnisse zu nutzen:
* Bei der Verwendung mehrerer Methoden im Projekt ist die Konsistenz der zugrunde liegenden Semantiken nicht nachgewiesen. Andererseits spielt die Methodenkombination eine wichtige Rolle, um die optimierte Durchführung einzelner Entwicklungsschritte zu ermöglichen.
* Die verfügbaren Semantiken können noch nicht auf die Randbedingungen des zu entwickelnden Zielsystems angepaßt werden. Damit wird die Spezifikation des Systems häufig sehr viel komplexer, als dies bei einer optimal angepaßten Spezifikationssemantik erforderlich wäre.
* Optimierung des Entwicklungsprozesses
* Erhöhung der Prozeßqualität
* objektive Zertifizierbarkeit des Entwicklungsprozesses, etwa im Sinne der DIN ISO 9000 Teil 3 [ISO 9000].
Vorgehensmodelle werden heute als notwendige Vervollständigung von Software-Entwicklungsmethoden angesehen: Spezifikations- und Entwurfssprachen und zugehörige Werkzeuge können erst dann optimal genutzt werden, wenn die Arbeitsschritte für ihre Anwendung im Projekt sinnvoll festgelegt sind.
Für viele Anwendungen industrieller Software-Entwicklung ist heute das V-Modell [VMOD] des Bundesinnenministeriums akzeptierter Standard. Während im CASE-Bereich die Projektabwicklung auf Grundlage des V-Modells bereits von manchen Werkzeugen unterstützt wird, ist die systematische Anwendung formaler Methoden im Software-Entwicklungsprozeß bisher noch nicht ausreichend untersucht worden. Erst recht fehlt die Einbettung formaler Methodenanwendung in das V-Modell.
Zur Beweisunterstützung bei der Entwicklung korrekter Realzeitsysteme wird von verschiedenen Forschern mit dem System PVS [ORS 92] experimentiert (vgl. z.B. [CRSS 94]). PVS gehört zur Familie der interaktiven Beweiser, die auf Logik höherer Stufe basieren, hat jedoch auch effiziente Entscheidungsprozeduren für Arithmetik fest eingebaut. Diese Kombination wird bei der Implementierung des Duration Calculus in PVS [SS 94] und des Verifikations- und Entwicklungskalküls von Hooman [Hoo 94] ausgenutzt.
Für eines der ersten Transformationssysteme, CIP-S ([B+ 85]), sowie der späteren Entwicklung PROSPECTRA ([HK 93]) stand vor allem formale Programmentwicklung auf der Basis von komplexen Transformationsregeln im Vordergrund. Die Integration von Matching-Techniken wurde hierbei noch nicht aufgegriffen. Dies gilt auch für Programm-Synthese Systeme wie KIDS (siehe [Smi 85, 91]), die ihnen in Hinsicht auf die Programm-Entwicklungsmethodik ähnlich sind. Beiden gemeinsam ist der Anspruch, auf der Basis von komplexen Regeln einen abstrakteren, benutzerfreundlicheren und wiederverwendbareren Stil der formalen Programmentwicklung darzustellen als die konventionellen a-posteriori-Verifikationsmethoden (z.B. mit LCF [Paul 87], KIV [HRS 91], oder [CO 92] basierend auf Isabelle [Paul 93]).
Die Ausdruckmöglichkeit von flexiblen Programm-Schemata ist bereits auf die Konstruktion von optimierenden Compilern angewandt worden, die den Übersetzungsprozeß als eine Abfolge von Normalformberechnungen bezüglich Programmtransformationen organisieren (vgl. OPTRAN [MWW 84], OPAL [GS 90]). Diese Systeme verwenden bereits raffiniertere Matching-Techniken, die allerdings auf einer ad-hoc Integration von Matching-Kombinatoren basieren. Im Bremer Ansatz können solche Kombinatoren (oder: Pattern-generierende Funktio-nen) durch rekursive Gleichungen definiert werden, wodurch mächtigere, auf die Objekt-Sprache abgestimmte Klassen von syntaktischen Schemata verwendet werden können ([SW 93, 94, Shi 94a, b]). Durch den darauf aufbauenden Transformationskalkül ist es möglich, effiziente Transformationstaktiken zu entwickeln.
Die Idee der transformationellen Programmentwicklung ist auch auf den Bereich der reaktiven oder kommuniziernden Systeme erweitert worden. So hat Back den ursprünglich nur für sequentielle Programme gedachten Refinement-Kalkül auf parallele und reaktive Programme ausgedeht [Bac90]. Back's Team arbeitet seit mehreren Jahren an einer Implementierungs des Refinement-Kalküls im logischen Rahmenwerkzeug HOL. Diese Implementierung ist jedoch nur von Experten nutzbar.
In Oldenburg wurde im Vorprojekt ProCoS der sogenannte MIX-Transformationskalkül entwickelt. Ausgangspunkt war dort ein CSP-artiges Kommunikationskonzept für reaktive Systeme. MIX umfaßt derzeit eine OCCAM-artige Programmiersprache und Konzepte von Action Systems und regulären Sprachen. MIX ist gut geeignet für die transformationelle Entwicklung kommunizerender, verteilter Systeme. Im Vorprojekt KORSO wurde der MIX-Transformationskalkül prototypartig in dem logischen Rahmenwerkzeug LAMBDA implementiert und an Fallstudien erprobt (siehe auch Abschnitt 6). Die Anwendung des entstandenen Transformationssystems verlangt jedoch genaue Kenntnisse des LAMBDA-Systems, die von außenstehenden Benutzern nicht erwartet werden können.
Generell ist heute der Standard, daß beim Erstellen von Spezifikationen bzw. Programmen die statische Semantik (Kontextbedingungen, Typen) überprüft werden. Ferner wird die Erstellung oft durch interaktives Arbeiten auf einer speziellen grafischen Darstellung der zugrunde liegenden abstrakten Syntax unterstützt (Struktureditieren von Texten, Formeln in mathematischer Notation, Strukturdiagrammen).