Martin-Luther-Universität Halle-Wittenberg

Logo des Lehrstuhls Software-Engineering und Progammiersprachen

Kontakt

Andreas Both
Institut für Informatik
Martin-Luther-Universität
Halle-Wittenberg

Raum 3.21
Von-Seckendorff-Platz 1
06120 Halle

Weiteres

Login für Redakteure

Kurz und knapp: Forschungsthema

Auf dieser Seite werden kurz und knapp in Frage/Antwort-Form die Eigenschaften des entwickelten Verifikationsverfahrens für Komponentensoftware und SOAs vorgestellt.

Was ist das Thema der Forschungen?

Das entwickelte Verfahren betrachtet die Sicherstellung der Funktionalität von Sofware die aus Komponenten (z. B. Webservices) zusammengesetzt wurde. Dafür werden die Interaktionen zwischen den Komponenten überprüft und sichergestellt, dass kein Verhalten möglich ist, dass verboten wurde. Es wird überprüft ob die Zusammenschaltung (composition) von Komponenten korrekt erfolgte und somit zuverlässig gearbeitet werden kann. [BZ08a,BZ08b]

Muss der Quellcode eines Webservices/Komponente freigegeben werden?

Das Verfahren benötigt den Quellcode nicht. Nichtsdestotrotz wird der Quellcode benötigt, um eine abstrakte Darstellung zu erzeugen. Diese Darstellung lässt kaum Rückschlüsse auf die Implementierung zu, ist aber immer noch verständlich. Der Quellcode wird also nur lokal und einmalig benötigt und nicht veröffentlicht. [BZ08a,BZ08b]

Wie kompliziert ist der zu formulierende Vertrag (Protokoll)?

Der hier formulierte Vertrag ist sehr einfach zu verstehen. Dies ist gilt insbesondere im Vergleich zu anderen Arbeiten (z.B. behavioral protocols). Die (graphische) Darstellung orientiert sich Workflow-Repräsentationen. Sie enthält nur die aufzurufenden Aktionen (Beispiele). [BZ08a]

Ist das Verfahren auch benutzbar, wenn man nichts von Model Checking versteht?

Das entwickelte Verfahren ist dafür ausgelegt, von allen am Entwicklungsprozess beteiligten Rollen genutzt werden zu können. Insbesondere orientieren sich die Verträge (Komponenten-Protokolle) an den Bedürftnissen von Business Analysts, Component Designern, Testern und auch Managern. [BZ09b,BZ08c,BZ08a]

Wer kann/sollte einen Komponenten-Vertrag (Protokoll) formulieren?

Dies ist abhängig vom gewünschten Zweck. Wenn z.B. ein Webservice in einer SOA immer korrekt benutzt werden soll, dann sollte der Entwickler selber das Protokoll erstellen um zu beschreiben, welche Benutzung vorgesehen ist [BZ08a,BZ08c,BZ09e]. Soweit in einem frühen Entwicklungsstadium die Spezifikation genutzt werden soll, dann wäre der Protokoll-Verantwortliche in der Gruppe der Business Analysts, Berater oder Component Designer zu suchen. Soll ein (neuer) Geschäftsprozess sichergestellt werden könnte auch ein Manager das (graphische) Protokoll definieren [BZ09b].

Mit welche Programmiersprachen kann das Verfahren umgehen?

Es handelt sich um ein allgemeines Verfahren [BZ08a]. Prinzipiell können alle imperativen und objekt-orientierten Programmiersprachen betrachtet werden. Implementierungen erfolgten für Python, PHP und BPEL.

Was sind die Besonderheiten des Verifikationsverfahrens?

Der Vertrag (Service-Protokoll) wurde von der Implementierung getrennt. Dies vereinfacht das Verfahren für den Benutzer und erhöht gleichzeitg die Mächtigkeit, da kompliziertere Repräsentationen im "Hintergrund" verwendet werden können. [BZ08c]

Was versteht man unter Komponenten- und Service-Protokollen?

Diese Protokolle beschreiben, wie eine Komponente/Service durch andere Komponenten benutzt werden soll. Es sind also Aufrufreihenfolgen enthalten, die beschreiben welche Funktionsaufrufe der Entwickler wann erwartet (Beispiele für Protokolle).

Mit welchen Komponentensystemen/Architekturen kann das Verfahren umgehen?

Es handelt sich um ein generalisiertes Verfahren. Deshalb ist es möglich beliebige Komponentensysteme (z.B. J2EE, .NET, Webservices, Corba) zu betrachten. Gleiches gilt für die verwendeten Programmiersprachen.

Welche Eigenschaften werden überprüft?

Mit Protokollen lassen sich Sicherheitseigenschaften und Zuverlässigkeit prüfen. Aufgrund der verwendeten Modellprüfung wird jedes potenzielle Problem entdeckt und gemeldet.

Was kann das Verfahren nicht absichern?

Das hier entwickelte Verfahren betrachtet (bisher) keine Daten. Deshalb ist nicht möglich zu überprüfen, ob eine Berechnung das richtige Ergebnisse liefert. Es kann in diesem Fall lediglich die Aussage getroffen werden, dass für die Berechnung eines Datums alle erforderlichen Methoden aufgerufen wurden.

Zum Seitenanfang