Kontakt
Andreas Both
Institut für Informatik
Martin-Luther-Universität
Halle-Wittenberg
andreas.both@informatik.uni...
Raum 3.21
Von-Seckendorff-Platz 1
06120 Halle
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
- [BZ08a] Andreas Both and Wolf Zimmermann. Automatic protocol conformance checking of recursive and parallel component-based systems. In Michel R. V. Chaudron, Clemens A. Szyperski, and Ralf Reussner, editors, Component-Based Software Engineering, 11th International Symposium (CBSE 2008 ), volume 5282 of Lecture Notes in Computer Science, pages 163–179. Springer , October 2008. BibTEX
- [BZ08b] Andreas Both and Wolf Zimmermann. Automatic protocol conformance checking of recursive and parallel component-based systems. Technical Report 2008/01, University Halle-Wittenberg, Institute of Computer Science, June 2008. BibTEX
- [BZ08c] Andreas Both and Wolf Zimmermann. Automatic protocol conformance checking of recursive and parallel BPEL systems. IEEE Sixth European Conference on Web Services (ECOWS ’08 ), 0:81–91, IEEE , 2008. BibTEX
- [BZ09a] Andreas Both and Wolf Zimmermann. Model checking of component protocol conformance – optimizations by reducing false negatives. In International Workshop on Formal Aspects of Component Software (FACS’09 ), Eindhoven, November 2009 (to be published as extended version in ENTCS ). BibTEX
- [BZ09b] Andreas Both and Wolf Zimmermann. On more predictable implementations of reliable workflows in service-oriented architectures. IEEE Seventh European Conference on Web Services (ECOWS ’09 ), 0: 87-96, IEEE , November 2009. BibTEX
- [BZ09c] Andreas Both and Wolf Zimmermann. Sicherstellung der Funktionalität in Komponentensystemen und Service-orientierten Architekturen. In Erik Maehle Stefan Fischer and Rüdiger Reischuk, editors, GI-Jahrestagung , volume 154 of Lecture Notes in Informatics , pages 425;3336–3349. GI, 2009. BibTEX
- [BZ09d] Andreas Both and Wolf Zimmermann. A step towards a more practical protocol conformance checking algorithm. In 35th Euromicro Conference on Software Engineering and Advanced Applications (SEAA 2009 ), pages 458–465. IEEE Computer Society , August 2009. BibTEX
- [BZ09e] Andreas Both and Wolf Zimmermann. Supporting the development process of reliable software during the composition process using interaction protocols. Technical Report 2009/04, University Halle-Wittenberg, Institute of Computer Science, September 2009. BibTEX
- [FB09] Rene Franke and Andreas Both. Tool demo: Component-based infrastructure for protocol conformance checking of component-based software. In International Workshop on Formal Aspects of Component Software (FACS’09 ), Eindhoven, November 2009. BibTEX