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

Einordnung der wissenschaftlichen Veröffentlichungen

Die unten angegebenen Arbeiten betrachten die Verifikation von Komponenten-Software und Service-orientierten Architekturen (SOA). Dabei ist das Ziel nicht nur Spezifikationen des Verhaltens einer Komponente anzugeben, sondern Abstraktionen von realem Quellcode zu verwenden. Dies soll sicherzustellen, dass Aussagen über die Implementierung möglich sind und nicht nur Aussagen über eine Spezifikation (die potenziell nichts mit dem Quellcode zu tun hat).

Dies ist das erste Alleinstellungsmerkmal, das zweite ist die
Betrachtung von unbeschränkter Rekursion und unbeschränktem parallelem Verhalten. Für diesen Zweck werden Process Rewrite Systems (PRS) verwendet. Damit werden sehr viele Anwendungsbereiche eröffnet.

Die einfach zu verstehenden Verträge einer Komponente werden Komponenten- oder Service-Protokolle genannt (Beispiele). Besondere Erwähnung sollen die Arbeiten BZ09b und BZ09e finden. Diese Arbeiten zeigen die praktische Anwendung zur Unterstützung des Projektmanagements bzw. im Entwicklungsprozess. In diesen Arbeiten wird die praktische Relevanz besonders betont.

Im Folgenden sind die Veröffentlichungen kurz beschrieben:

  • BZ08a: Beschreibt das Problem und eine eingeschränkte Lösung, Synchronisation wird nicht betrachtet. Es werden erstmals Protokolle im Sinne eines Vertrags definiert, der losgelöst von der Implementierung existiert. Es wird erstmal die Combined Abstraction vorgestellt. Es wird ein allgemeines Verfahren vorgestellt wie mit Compiler-Technologien die vorgeschlagenen Abstraktionen automatisch erstellt werden können.
  • BZ08b: Ist eine Vorabversion von BZ08a.
  • BZ08c: Es wird die Anwendung für BPEL betrachtet. Dies verlangt auch eine Betrachtung der Synchronisation von Web Services. Die Erweiterung ermöglicht einen Einsatz in sehr vielen Kontexten.
  • BZ09a: Die Veröffentlichung betrachtet die Verbesserung des Model Checkings von Process Rewrite Systems unter dem Gesichtspunkt der Combined Abstraction. Dadurch werden weniger False Negatives erzeugt und eine bessere praktische Anwendung erreicht.
  • BZ09b: Thema dieser Arbeit ist die Verifikation von BPMN-Modellierung von Geschäftsprozessen. Hier wird gezeigt, dass bereits vor der Implementierung eines Workflows überprüft werden kann, ob dieser jemals die durch Service-Protokolle definierten Bedingungen erfüllen wird. Es muss also mit der Überprüfung nicht bis zur Fertigstellung der Implementierung gewartet werden. Die hohe praktische Relevanz wird gezeigt.
  • BZ09c: Das Verfahren wird so erweitert, dass es auch mit SOA umgehen kann, bei denen Services vollständig dynamisch gewählt werden (z.B. aus einem dynamisch gewählten UDDI-Dienst).
  • BZ09d: Ein neuer Algorithmus wird vorgestellt, dieser beschleunigt die Modellprüfung im praktischen Fall (wie Experimente zeigen).
  • BZ09e: Integration des Verifikationsverfahrens in iterative bzw. zyklische Softwareentwicklungsprozesse. So können  Komponente bereits zusammengefügt werden (Composition), ohne dass alle benötigten Komponenten implementiert oder bekannt sind. Dies ermöglicht eine Vorhersage von potenziellen Fehlern. Ansonsten ist es auch möglich zu beweisen, dass nie ein Fehler in diesen zusammengesetzten Komponenten auftreten kann.
  • FB09: Die implementierte Infrastruktur wurde bei einem Workshop ausführlich vorgestellt (Vortrag + Demo).

Quellen

Zum Seitenanfang