unilogo width=2.5cm

Diplomarbeit

Werkzeuggestützte Herleitung von Protokollen

Hintergrund

Komponenten (Klassen, Module und Subsysteme) verfügen über eine Schnittstelle, die ihre zulässige Verwendungsweise definiert. Der Begriff Schnittstelle wird oft in einem sehr engen Sinne aufgefasst: als die Menge exportierter (bzw. auch importierter) Routinen, Typen und globaler Variablen (bei Modulen) bzw. Methoden und Attribute (bei Klassen). Diese Art von Schnittstelle bezeichnen wir als die syntaktische Schnittstelle. Sie ist mit einfachen Mitteln zu erkennen. Gemäß Parnas [1] ist der Begriff Schnittstelle jedoch viel weiter zu fassen: als die Menge aller zulässigen Annahmen über eine Komponente. Hierzu zählen alle Vor- und Nachbedingungen von Routinen der Komponente, alle Konsistenzbedingungen der Typen und Variablen bzw. Attribute sowie auch Annahmen über das Laufzeitverhalten und den Speicherbedarf.

Eine spezielle Form der Annahmen über Komponenten sind sequentielle Beschränkungen der Ausführungsreihenfolge ihrer Operationen (d.h. Aufrufe der Routinen und Zugriffe auf Variablen und Attribute ihrer Schnittstelle). Beispielsweise muss vor Verwendung eines abstrakten Datentyps Stack zuerst die Initialisierungsroutine und zuletzt die Freigaberoutine aufgerufen werden. Außerdem darf zu keinem Zeitpunkt die Anzahl der Pop-Operationen die der Push-Operationen überschreiten.

Solche Sequenzbeschränkungen können mit herkömmlichen Programmiersprachen nicht formuliert werden und werden leider, selbst wenn diese Möglichkeit besteht, nur in seltenen Fällen von Programmierern tatsächlich ausreichend dokumentiert. Die Verletzung solcher Sequenzbeschränkungen hat in der Regel ein Fehlverhalten während der Laufzeit zur Folge.

Unit-Tests können diese Fehler zum Teil aufdecken, geben allerdings keine Garantie, dass wirklich alle Fehler gefunden werden. Außerdem liefern Unit-Tests keine Erklärung, wie es zum Fehler kommt. Durch statische Prüfung können solche Fehler vermieden und erläutert werden. Solche statische Prüfungen sind leider nicht vollständig automatisierbar, da viele daran geknüpfte Fragen unentsceidbar sind. Sie müssen somit zu einem großen Teil vom Menschen übernommen werden. Der Aufwand statischer Prüfungen durch den menschlichen Analytiker ist jedoch ohne Werkzeugunterstützung sehr hoch. Außerdem unterlaufen menschlichen Analytikern Fehler, insbesondere wenn Information mühsam von Hand gesammelt werden muss.

Olender und Osterweil [2] haben für die statische Prüfung von Sequenzbeschränkungen ein Verfahren entwickelt, das Sequenzbeschränkungen prüft, wenn diese in Form einer regulären Sprache spezifiziert werden können (denn dann ist diese Frage entscheidbar). Verwendet wird hierzu ein Datenflussrahmenwerk. Butkevich und Kollegen [4] schlagen ebenfalls reguläre Sprachen zur Spezifikation von Sequenzbeschränkungen von Klassen und Schnittstellen vor. Diese Spezifikationen werden im Falle von Vererbungen auf Konformität geprüft. Somit ist zwar eine Konformität zwischen Spezifikationen sichergestellt, nicht jedoch die Konformität des Quelltextes bezüglich der Spezifikation. Model-Checking-Methoden können für die Prüfung von Sequenzbeschränkungen ebenfalls herangezogen werden; allerdings bedarf es hierfür zunächst der Extraktion des Modells aus dem Quelltext [5].

Sowohl Olender und Osterweil als auch Butkevich und Kollegen setzen die Existenz einer Spezifikation voraus, die für viele reale Systeme nicht vorliegt. Cook und Wolf [3] schlagen deshalb vor, Modelle des Verhaltens durch eine Markov-Analyse der tatsächlichen Ausführung herzuleiten. Diese Informationen können Rückschlüsse auf Sequenzbeschränkungen zulassen. Wie beim Testen besteht auch hier das für nichttriviale Systeme unlösbare Problem, eine vollständige Abdeckung aller möglichen Eingaben zu erreichen, um jedes prinzipiell mögliche Verhalten zu erkennen.

Eigene Vorarbeiten

Unser prinzipielles Vorgehen zur statischen Herleitung von Protokollen wurde bereits ausgearbeitet [7, 9]. Das semi-automatische Verfahren zur Herleitung von Sequenzbeschränkungen stützt sich auf folgende verfügbare Informationsquellen:

  • die tatsächliche Verwendungsweise des Moduls oder der Klasse in Form statischer Spuren aller Instanzen des Moduls bzw. der Klasse; die statische Spur einer Instanz (eines Objekts) enthält alle und nur jene Anweisungen, die potentielle Operationen auf diesem Objekt darstellen [6]; statische Objektspuren werden durch statische Kontroll- und Datenflussanalysen ermittelt [6]
  • statische Informationen über die inneren Abhängigkeiten des Moduls oder der Klasse (Kontroll- und Datenabhängigkeiten)
  • Domänenwissen unter Einbeziehung des menschlichen Experten und möglicherweise verfügbarer Dokumentation
Unser Prozess der Protokollherleitung lässt sich wie folgt beschreiben: Zunächst werden die statischen Spuren aller Instanzen eines Moduls oder einer Klasse extrahiert. Die gefundenen statischen Spuren stellen beispielhafte Verwendungen dar und bilden somit das Rohmaterial für den Herleitungsprozess. Diese statischen Spuren können dann durch den Benutzer validiert werden. Die validierten statischen Spuren können vollautomatisch vereinheitlicht werden, soweit dies durch bekannte Techniken aus der Automatentheorie möglich ist; z.B. können durch bekannte Verfahren zur Umwandlung von nichtdeterministischen endlichen Automaten in deterministische Automaten gemeinsame Präfix ­ und in umgekehrter Form auch gemeinsame Suffixe ­ gefunden werden [10].

Mittels Graphmustern kann der Benutzer darüber hinaus häufig wiederkehrende Verwendungsmuster aufspüren, die sich einer konservativen vollautomatischen Vereinheitlichung entziehen. Ein Beispiel hierfür sind Operationen, die teils durch Prädikate bedingt und teils unbedingt ausgeführt werden. Dieses Muster liefert einen Hinweis, dass das Prädikat optional sein könnte. Dank der Unterstützung von Program-Slicing kann der Benutzer seine Hypothesen über Sequenzbeschränkungen rasch verifizieren. Der Benutzer wird durch unsere Datenflussanalysen dabei auf Seiteneffekte der Operationen aufmerksam gemacht. Hat eine Operation keine Seiteneffekte und geht von ihr auch keine Kontrollabhängigkeit für andere Operationen des Moduls bzw. der Klasse aus, dann ist diese Operation möglicherweise optional in einer Sequenz.

Der Benutzer selbst kann zu jeder Zeit eigene Sequenzbeschränkungen bzw. -lockerungen hinzufügen. Auf diese Weise können möglicherweise wieder neue vereinfachende automatische Transformationen angewandt werden. Der Herleitungsprozess ist somit iterativ und inkrementelle.

Ein erster rudimentärer Prototyp zur Unterstützung dieses Prozesses wurde im Rahmen einer Diplomarbeit für C-Komponenten implementiert. Der Prototyp dient als Konzeptbeweis, genügt jedoch nicht für echte Fallstudien. Realistische Fallstudien müssen durchgeführt werden, um die Tragfähigkeit des Verfahrens zu ermitteln. Der Prototyp berücksichtigt außerdem auch keine inneren Kontroll- und Datenabhängigkeiten der Komponente selbst und bietet dem Benutzer nicht die Möglichkeit, eigene Graphmuster bzw. Graphtransformationen anzugeben.

Aufgabenstellung

Die Aufgabe dieser Diplomarbeit ist es, den vorgeschlagenen Prozess durchgängig durch Werkzeuge zu unterstützen. Hierzu kann eine Reihe existierender Bausteine übernommen werden (eventuell mit Anpassungen):
  • Extraktion statischer Spuren, die bereits die extrahierten Spuren in einem Resource-Flow-Graph (RFG) ablegt
  • Visualisierung der Objektspuren im Grapheneditor Gravis für RFGs
  • vollautomatische Vereinheitlichung der Objektspuren mit Hilfe von Techniken aus der Automatentheorie
  • rudimentäre Implementierung zur Suche nach Graphmustern in RFGs
Im Einzelnen umfasst die Diplomarbeit folgende Aufgaben:
  • Anpassung der vollautomatischen Vereinheitlichung an die Änderungen, die sich für die Modellierung von Objektspuren seit der Arbeit von Timo Heiber ergeben haben
  • semiautomatische Vereinheitlichung der Objektspuren mit Hilfe von benutzerdefinierten Graphmustern; hierzu muss ein Formalismus zur Spezifikation von Grapmustern für die Zwecke der Vereinheitlichung beschrieben und umgesetzt werden ("generische" Muster); die Graphmuster sollen vom Benutzer in Gravis graphisch spezifiziert werden können; eine entsprechende textuelle Repräsentation der Graphmuster ist ebenso zu spezifizieren und zu unterstützen
  • Spezifikation (durch den Benutzer) und Berücksichtigung (durch die Analysen) äquivalenter Operationen: beispielsweise soll für einen Datentyp Stack ausgedrückt werden können, dass sich ein Push und ein unmittelbar darauf folgendes Pop gegenseitig aufheben; diese Äquivalenzen können mit Hilfe der Graphmuster spezifiziert werden, sie unterscheiden sich jedoch darin, dass hierzu zusätzlich der Graph transformiert wird; außerdem sind diese Muster spezifisch für eine Komponente
  • Integration der vollautomatischen und semi-automatischen Vereinheitlichung im Grapheneditor Gravis
  • optional, sofern die Zeit reicht: Durchführung einer Fallstudie an einem realen System; als ein Kandidat hierfür kommt das System concepts in Frage
Die Graphmuster und Graphtransformationen sollen möglichst allgemein für den RFG implementiert werden, so dass sie auch für andere Zwecke wiederverwendet werden können.

Die Ansprüche an die Qualität der Implementierung sind hoch. Es soll ein tatsächlich verwendbares Werkzeug entwickelt werden. Vollständige Dokumentation und ein umfangreicher systematischer Test sind deshalb Teil der Aufgabe.

Implementierungs-
werkzeuge

Der Ada-Compiler Gnat; Bauhaus-Werkzeuge.

Voraussetzungen

Kenntnisse in Ada 95.

Literatur

  1. D. L. Parnas:
    On the Criteria to be Used in Decomposing Systems into Modules. Communications of the ACM, 5(12), December 1972, 1053-1058.
  2. K.M. Olender, L.J. Osterweil:
    Interprocedural Static Analysis of Sequencing Constraints, ACM Transactions on Software Engineering and Methodology, Vol. 1, No.1, pp. 21-52, January 1992.
  3. J. E. Cook, A. L. Wolf:
    Discovering Models of Software Processes from Event-Based Data. ACM Transactions on Software Engineering and Methodology, Vol. 7, No. 3. July 1998, pp. 215-249.
  4. S. Butkevich, M. Renedo, G. Baumgartner und M. Young:
    Compiler and Tool Support for Debugging Object Protocols. In Proceedings of the Eighth International Symposium on Foundations of Software Engineering for Twenty-First Century Applications, 2000, pp. 50-59.
  5. J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, H. Zheng: Bandera:
    Extracting Finite-State Models from Java Source Code. In Proceedings of the International Conference on Software Engineering, 2000, pp. 439-448.
  6. T. Eisenbarth, R. Koschke, G. Vogel:
    Static Trace Extraction. In Proceedings of the Working Conference on Reverse Engineering, IEEE Computer Society Press, Oktober 2002.
  7. R. Koschke, Y. Zhang:
    Component Recovery, Protocol Recovery and Validation. In 3. Workshop Software-Reengineering, Bad Honnef (10./11.Mai 2001), Fachberichte Informatik, Universität Koblenz-Landau, Nr. 1/2002, pages 73-76, Januar 2002.
  8. G. Vogel:
    Extraktion statischer Objekt-Traces zur Erkennung und Beschreibung von Konnektoren. Diplomarbeit, Nr. 1940, Institut für Informatik, Universität Stuttgart, 2001.
  9. T. Heiber:
    Semi-automatische Herleitung von Komponentenprotokollen aus statischenVerwendungsmustern. Diplomarbeit, Fakultät Informatik, Universität Stuttgart, 2001.
  10. E. Hopcroft, J.E. UlLman, J.D.:
    Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

Betreuer

Dr. Rainer Koschke (Zi. 2.160)


Valid HTML 3.2! Last modified: Mon Aug 25 16:36:20 MET 2003
admin@droste.informatik.uni-stuttgart.de