Zum Abschluß der Artikelserie über formale Spezifikationsmethoden werden die drei vorgestellten FDTs im Vergleich diskutiert. Dabei zeigt es sich, daß die Methoden unter verschiedenen Blickwinkeln sehr unterschiedlich zu bewerten sind, so daß kein generelles Urteil möglich ist. Um für einen Einsatz eine Auswahl unter diesen formalen Methoden treffen zu können, sind die unterschiedlichen Aspekte nach ihrer Bedeutung für den jeweiligen Einsatzbereich zu gewichten.
Im folgenden werden wir die FDTs unter verschiedenen Gesichtspunkten betrachten. Weitere Aspekte (zum Beispiel Verfügbarkeit maschinengestützter Werkzeuge) können darüber hinaus bedeutsam sein. Mit dem Einsatz von formalen Spezifikationsmethoden können verschiedene Ziele verfolgt werden. Davon hängt es ab, welche Bedeutung den nachfolgenden Kriterien zur Bewertung der FDTs eingeräumt wird.
Aus diesen Gründen kann die folgende Diskussion weder einen Anspruch auf Vollständigkeit erheben, noch zu einem abschließenden Urteil über die behandelten FDTs gelangen.
Eine grafische Darstellung des Vergleichs ist in der Abbildung auf Seite 20 enthalten.
SDL und Estelle erlauben beide vollständige, formale Beschreibungen, jedoch erzwingen sie diese nicht. Zu SDL existiert eine Beschreibung der Sprachmittel, die neben der Darstellung mittels grafischer Symbole auch die formale Darstellung von Details genau regelt, jedoch ist die informelle Festlegung von wichtigen Protokolldetails in den Aktionssymbolen zugelassen.
In Estelle gibt es umfangreiche formale Sprachmittel, da Estelle Sprachumfang von Pascal einschließlich formaler Erweiterungen umfaßt. Die Ähnlichkeit zu Pascal erfordert jedoch prinzipiell einen hohen Grad an Detaillierung, der in Estelle durch Konstrukte wie ",,,", Primitive etc. wieder etwas verringert wurde. Dadurch geht aber auch der Zwang zur
Vollständigkeit der formalen Beschreibung verloren. So beschriebene Teile müssen eventuell über informelle Kommentare (binding comment) erklärt werden.
Lotos ermöglicht eine mathematisch exakte Beschreibung. Auch Datentypen sind nach einem mathematisch exakten Modell (abstrakte Datentypen) modellierbar. Durch die Methode werden vollständig formale Beschreibungen erzwungen, da keine informalen Sprachmittel vorgesehen sind.
Wegen des Umfangs von Spezifikationen, die in der Praxis zu erstellen sind, ist zur Verifikation maschinelle Unterstützung notwendig. Deshalb werden wir nur diese Möglichkeit diskutieren.
Maschinelle Methoden für SDL können erst benutzt werden, wenn der Graph in maschinenlesbarer Form repräsentiert wird. Es existieren Verifikationsmethoden für Protokollspezifikationen mittels endlicher Automaten. Sie lassen sich (unter Umständen nach gründlicher Überarbeitung) auch auf die erweiterten Automaten in SDL anwenden.
Für Estelle gilt aufgrund der Ähnlichkeit des zugrundeliegenden Modells dasselbe wie für SDL. Jedoch ist die Syntax einer Estelle-Spezifikation wegen ihrer Nähe zu Pascal relativ einfach maschinell zu bearbeiten. Die Sprache unterstützt zudem das Erreichen eines hohen Grades an formaler Exaktheit und Vollständigkeit. Allerdings kann sich der dazu notwendige Detaillierungsgrad auch hinderlich auswirken, da eine Spezifikation eigentlich auf höherer Ebene stattfinden sollte.
Die Darstellungsweise in Lotos mittels algebraischer Ausdrücke unterstützt die Durchführung eines konventionellen mathematischen Beweises. Die formale Exaktheit, Vollständigkeit und das hohe Abstraktionsniveau erleichtern die Durchführung eines (maschinenunterstützten) Korrektheitsbeweises von Spezifikationen gegenüber den gestellten Anforderungen.
Bei Verwendung von SDL oder Estelle ist Validieren durch Test (siehe "Generierung von Testfällen") zu erreichen. Bei automatischer Implementation sollte die Übereinstimmung mit der Spezifikation auf jeden Fall gegeben sein.
Die Methode der schrittweisen Verfeinerung einer Spezifikation bis zum Moduldesign ermöglicht es, eine der Spezifikation sehr ähnliche Implementation zu erstellen. Bei Estelle ist dabei die Ähnlichkeit zu Pascal noch zusätzlich von Vorteil.
Zu den Möglichkeiten, die SDL und Estelle bieten, kommt bei Lotos noch die Möglichkeit hinzu, die Übereinstimmung einer Lotos-Beschreibung der Implementation mit einer Lotos Beschreibung des Protokolls zu beweisen. Allerdings ist dadurch noch nicht geklärt, ob die Lotos-Beschreibung der Implementation mit der tatsächlichen Implementation übereinstimmt. Für alle drei Methoden gilt, daß sich aus einer Spezifikation, die in maschinenlesbare Form übersetzt wurde, automatisch die Menge aller möglichen Sequenzen von beobachtbaren Interaktionen eines Systems bestimmen lassen. Daraus lassen sich Testfälle generieren, mit deren Hilfe die Übereinstimmung von tatsächlichen Sequenzen einer Implementation mit Sequenzen aus dieser Menge überprüfen lassen. Obwohl die FDTs sich hierin nicht prinzipiell unterscheiden, sind doch die Methoden zur Bestimmung der erlaubten Interaktionssequenzen verschieden.
Hierunter ist zu verstehen, wie umfassend die Einsatzmöglichkeiten einer Methode im Laufe des Software-Life-Cycle sind.
"Bandbreite" der Methode
SDL ist von groben (nicht exakten oder vollständigen) Spezifikationen über detaillierte Spezifikationen bis hin zu Grob- (und eventuell auch Fein-)Design einsetzbar. Bei entsprechender maschineller Unterstützung ist SDL eventuell auch zur Implementation geeignet.
Dasselbe gilt auch für Estelle. Jedoch ist maschinelle Unterstützung durch die Pascal-Ähnlichkeit und die fehlende Grafik leichter zu erreichen.
Lotos ist von (vollständigen) Spezifikationen auf abstrakter Ebene über Verifikation der Spezifikation bis hin zu Grob- (und eventuell auch Fein-) Design einsetzbar. Eine geeignet gewählte Untermenge der Sprache könnte in Verbindung mit einer Trägersprache zur Realisierung der abstrakten Datentypen auch für die Implementation Verwendung finden.
Sie ist bei SDL sehr hoch, da grafische Darstellung und eingängige Symbole benutzt werden. Erfahrungen zeigen, daß ein unmittelbares Verständnis von einfachen SDL-Graphen auch bei "Sprachunkundigen" möglich ist. Bei höherer Detaillierung besteht jedoch die Gefahr, daß die Grafik schwer überschaubar wird.
Die Verständlichkeit der Beschreibungsmittel von Estelle ist wegen ihrer Ähnlichkeit zu Pascal für jeden der höhere Programmiersprachen kennt, recht einfach. Jedoch ist die Übersichtlichkeit einer Spezifikation in Estelle durch die lineare Form nicht so hoch wie in SDL. Schon bei kleineren Systemen mit geringer Detaillierungstiefe wird das Erfassen (und Verstehen) des Gesamtverhaltens des spezifizierten Systems schwierig. Hier bieten sich wiederum grafische Hilfsmittel (wie SDL) zur Darstellung der endlichen Automaten an.
Das hohe Abstraktionsniveau von Lotos-Spezifikationen erschwert ihre intuitive Verständlichkeit. Die Sprache ist durch ihre abstrakte mathematische Notation nur sehr schwer zugänglich. Auch die Sprachbeschreibung in ihrer bisher vorliegenden Form, die ebenfalls sehr abstrakt ist, dafür allerdings auch eine exakte Definition der Semantik der Sprache enthält, erschwert das Erlernen.
Bei maschineller Übersetzbarkeit ist zu unterscheiden zwischen einer Übersetzung zur Unterstützung der Überprüfung einer Spezifikation oder zum Generieren von Testsequenzen und einer Übersetzung zum Zweck der Implementation. Dabei spielt der letztgenannte Aspekt bei FDTs eine untergeordnete Rolle, da sie vom Konzept her nicht als Ersatz für Implementationssprachen gedacht sind, jedoch könnte dieser Aspekt zukünftig durchaus mehr Bedeutung gewinnen im Hinblick auf maschinelle Implementationsunterstützung.
Für SDL ist ein spezieller Grafikeditor erforderlich, um gleichzeitig mit der Grafik auch eine maschinell zugängliche Version der Beschreibung zu erstellen. Man kommt zwar auch ohne Grafikeditor aus durch Verwendung der linearen Syntax von SDL, jedoch ergibt dies Spezifikationen mit weit geringerer Übersichtlichkeit.
Wenn der Graph einmal abgespeichert ist, ist eine Übersetzung einfach durchzuführen, wenn alle für die Implementierung erforderlichen Informationen in Aktionssymbolen etc. angegeben wurden.
Wegen der Nähe zu Pascal ist die maschinelle Übersetzbarkeit von Estelle durch einen erweiterten Pascal-Compiler und eine geeignete Betriebssystemumgebung zur Prozeßsteuerung relativ einfach zu verwirklichen. Schwierigkeiten bei der Übersetzung bereiten Sprachkonstrukte wie "....", primitive, binding comment etc., die für eine automatische Übersetzung konkretisiert werden müssen.
Bei SDL und Estelle ist bei entsprechender Verfeinerung der Spezifikation die Möglichkeit zur Verwendung als Implementationssprache möglich .
Bei Lotos bieten der hohe Formalisierungsgrad und die Vollständigkeit innerhalb des Formalismus gute Voraussetzungen für eine maschinelle Übersetzung. Wegen des hohen Abstraktionsgrades erscheint es jedoch schwierig, eine maschinell erstellte lauffähige und gleichzeitig effiziente Implementierung zu erhalten. Jedoch ist eine Simulation des spezifizierten Systems, die keine Forderungen an die Effizienz stellt, denkbar.
Die einzelnen FDTs in der Zusammenfassung
Abschließend wollen wir noch einmal zusammenfassen, inwiefern die vorgestellten FDTs die in der ersten Folge dargestellten Anforderungen an eine formale Spezifikationsmethode erfüllen.
Es zeigt sich dabei, daß viele Anforderungen nur im Zusammenhang mit den anderen gesehen werden können. So ist eine kompakte Darstellung in jeder betrachteten FDT möglich, aber eine kompakte und vollständige Spezifikation erscheint uns nur in Lotos möglich (und auch dort nur mit Einschränkungen).
Andere Eigenschaften sind mit den FDTs erreichbar, werden jedoch nicht von ihnen erzwungen. So ist die Exaktheit der Darstellung mit jeder der FDTs erreichbar, jedoch nur Lotos bietet dem Benutzer keine Möglichkeit der vagen Beschreibung und erzwingt daher Exaktheit. Entsprechendes gilt für die Eindeutigkeit der Spezifikationen.
Manche Eigenschaften der FDTs leiten sich direkt aus den zugrundeliegenden Modellen her. So ist zum Beispiel eine Überprüfbarkeit der Spezifikation in jeder FDT möglich wenn auch die algebraische Beschreibungsweise in Lotos eine Überprüfung erleichtert. Ähnliches gilt für die Überprüfbarkeit der Konsistenz der Beschreibung.
Die SDL und Estelle zugrundeliegenden Modelle unterstützen eine mögliche automatische (effiziente) Implementierung wesentlich besser, als das Lotos zugrundeliegende Modell, legen aber gleichzeitig bestimmte Implementationen sehr nahe, erreichen also nur einen geringeren Grad an Implementationsunabhängigkeit. Maschinelle Bearbeitung von SDL-Spezifikationen erfordern spezielle Hilfsmittel wie zum Beispiel einen Grafikeditor.
Die verschiedenen Darstellungsmethoden wirken sich auf die intuitive Verständlichkeit und auf die Handhabbarkeit der FDT aus. So sind die Diagramme von SDL sehr leicht verständlich und einfach überschaubar. Ihre Erzeugung ist allerdings umständlich oder bedarf spezieller Hilfsmittel.
Estelle dagegen benutzt die von herkömmlichen Programmiersprachen bekannten Hilfsmittel und Darstellungsweisen. Dadurch wird eine bessere Handhabbarkeit gegenüber SDL erreicht. Erkauft wird sie mit verringerter Übersichtlichkeit und intuitiver Verständlichkeit.
Das Verständnis von Spezifikationen in Lotos erfordert eine gewisse Übung, da sich die verwendeten Beschreibungsmethoden deutlich von herkömmlichen Programmiersprachen unterscheiden. Die Operatoren sind durch ihre Komplexität nur von geübten Spezialisten sinnvoll zu handhaben.
Die Verwendung von abstrakten Datentypen birgt eine große Gefahr der Unterspezifikation oder der zur Inkonsistenz führenden Überspezifikation. Zum Beispiel kommt es leicht vor, daß eine Spezifikation in der Vielzahl der theoretisch möglichen (und eventuell unerwünschten) Ausprägungen nicht mehr überschaubar ist.
FDTs werden eine wachsende Bedeutung in der Zukunft haben. Dies gilt auch für andere Bereiche der Software-Entwicklung. Dabei werden sich gewiß, noch weitere formale Spezifikationsmethoden herauskristallisieren.
* Die Autoren Klaus-Peter Fischer (Dipl.-Math.) und Stephan Hesse (Dipl.-lnform.) sind Software-Entwickler speziell für Kommunikationssysteme sowie Berater aus diesem Gebiet bei der Telenet GmbH Geschäftsstelle Rhein-Main.