Teilprojekt D4
From GRK-Wiki
zum übergeordneten Forschungsbereich
Contents |
Deklarative Modellierung von Workflows
Im Graduiertenkolleg werden Steuerungsverfahren der P2P-Middleware-Ebene untersucht, die als Ensembles kooperierender, sich adaptiv modifizierender und selbstorganisierender Workflows aufgefasst werden. Das Zusammenspiel der Workflows wird im Kern durch einen Satz verteilter Basisalgorithmen organisiert, die insbesondere das System nach einer Störung selbständig stabilisieren sollen. Als Alternative zu den operationellen Beschreibungen von Workflows in D1 (Selbstorganisation in der P2P-Middleware), D3 (zur Verifikation allgemeiner Workflow-Eigenschaften wie Bedienbarkeit, Komposition und Rücksetzbarkeit), E2 (ausführbare, sprachbasierte Workflow-Modelle des Katastrophenmanagements) und E3 (Workflow-Steuerung von Geo-Informationsdiensten) werden hier deklarative Beschreibungen von Workflows untersucht. Dabei sollen insbesondere Eigenschaften der Adaptierbarkeit und der Selbststabilisierung modelliert und analysiert werden. Eine solche Beschreibung ist nicht notwendig unmittelbar implementierbar. Stattdessen werden die Eigenschaften der Workflows auf einer abstrakten, logikbasierten Ebene formuliert. Dies kann die Separierung von Systemkomponenten unterstützen und das Verständnis der Funktionalität erhöhen. Konkrete Anwendungen sind die Steuerungs-Workflows der P2P-Middleware-Ebene. Im Kern der Selbstorganisation sollen sich dort selbststabilisierende Algorithmen herauspräparieren und deklarativ charakterisieren lassen. Eine weitere Anwendung ist die abstrahierende Beschreibung des Verhaltens der Workflows für die Akteure einer Workflow-basierten Steuerung. Aus derartigen Beschreibungen können Anwendungsszenarien und Use Cases abgeleitet werden. Die deklarative Beschreibung der Workflows durch Angabe ihrer wichtigsten Eigenschaften bildet eine ausgezeichnete Grundlage für die Verifikation der Implementierungen (siehe B3), bei der zu zeigen ist, dass die Implementierungen tatsächlich die gewünschten Eigenschaften erfüllen.
Stand des Wissens
Web Services, Workflows und Geschäftsprozesse werden vielfach informell oder in Pseudo-Code formuliert, sprachbasierte Beschreibungen nehmen dabei jedoch zu [1]. Seit geraumer Zeit werden jedoch auch formale Modelle zur semantischen Präzisierungen der informalen Darstellungen publiziert, formuliert beispielsweise als Abstract State Machines oder Petrinetze. Adaption und Selbstorganisation bilden zusätzliche Ansprüche an die Modellbildung: Ein Modellalgorithmus muss dafür unabhängig von konkreten Netzwerktopologien formuliert werden. Dies gelingt nachgewiesenermaßen mit formalen Methoden. Mit Abstract State Machines [2] und symbolischen High-level-Petrinetzen [3] kann man beispielsweise Algorithmen für beliebige zusammenhängende Netzwerke charakterisieren. Komplexe Eigenschaften von Workflows wie z. B. Bedienbarkeit der Äquivalenz, sind bislang nicht deklarativ beschrieben worden.
Vorarbeiten der beteiligten Wissenschaftler
Im Rahmen einer DFG-Forschergruppe und zweier Projekte im Normalverfahren wurden in der Arbeitsgruppe von W. Reisig Methoden entwickelt, verteilte Basisalgorithmen zu modellieren und zu verifizieren. Die Monographie [3] präsentiert zentrale Ergebnisse, insbesondere auch verifizierte selbststabilisierende Algorithmen. Seit einigen Jahren werden am Lehrstuhl neben Petrinetzen verstärkt auch andere Formalismen zur Modellierung und Analyse von Workflows untersucht, insbesondere Abstract State Machines. Für beide Formalismen wurden entsprechende Varianten gebildet und angewendet (siehe [4] und [5]). Eine interessante Alternative ist Lamports TLA [6]. Diese Methode unterstützt insbesondere die Kompositionalität und eigenschaftserhaltende Verfeinerung von Modellen. Die Arbeitsgruppe von A. Reinefeld beschäftigt sich mit Fragen der Selbstorganisation und Skalierung hauptsächlich im Zusammenhang mit Grid-Computing [7]. Fragen der adaptiven Generierung von Workflows werden in [8] diskutiert.
Geplante Arbeiten
Im Zentrum der geplanten Arbeiten steht die deklarative Modellierung von Workflows. Dafür werden logik-basierte Methoden verwendet, die auch einen Bezug zu operationellen Darstellungen haben, insbesondere ASM, symbolische High-level-Petrinetze und TLA. Zur Durchführung stehen dabei zwei Teilaufgaben an: Zum einen werden die für das Ressourcenmanagement der P2P-Middleware-Ebene typischen Workflows identifiziert und deklarativ modelliert. Dabei werden insbesondere komplexe Eigenschaften wie Adaptierbarkeit und Selbststabilisierung logikbasiert charakterisiert. Hier ist eine enge Abstimmung mit den Arbeiten in B3 zur Protokollverifikation auf der Ebene selbstorganisierender Netze vorzunehmen. Der Schwerpunkt dieses Arbeitspaketes liegt darin, deklarative Techniken zu entwickeln, die adäquat für die Anwendungsdomäne sind. Zum anderen werden Verfahren entwickelt, die die Verifikation unterstützen, also den Nachweis, dass entsprechende Implementierungen der Workflows die o. g. Eigenschaften tatsächlich haben. Als erster Ansatz bieten sich dabei interaktive Techniken an, wie sie z.B. in Beweisern für Higher Order Logic implementiert sind.
Referenzen
[1] G. Alonso, F. Casati, H. Kuno, V. Machiraju: Web Services. Springer-Verlag 2004.
[2] E. Börger, R. Stärk: Abstract State Machines. Springer-Verlag 2003.
[3] W. Reisig: Elements of Distributed Algorithms. Springer-Verlag, 1997.
[4] W. Reisig: Modelling- and Analysis Techniques for Web Services and Business Processes. Informatik-Berichte Nr. 183, Humboldt-Universität zu Berlin, 2004. auch FMOODS 2005, Athen, LNCS erscheint demnächst.
[5] W. Reisig, A. Brade: ASM Models for Web Services. Informatik-Berichte Nr. 181, Humboldt-Universität zu Berlin, 2004.
[6] A. Alexander, W. Reisig: Compositional Temporal Logic Based on Partial Order. In: Proc. of the 11th Int. Symp. on Temporal Representation and Reasoning TIME 2004, pp. 125-132, IEEE 2004.
[7] A. Reinefeld, F. Schintke, T. Schütt: Scalable and Self-Optimizing Data Grids. In: Yuen Chung Kwong (ed.), Annual Review of Scalable Computing, vol. 6, Singapore University Press, Chapter 2, pp. 30 – 60, 2004.
[8] A. Andrzejak, U. Hermann, A. Sahai: FeedbackFlow - An Adaptive Workflow Generator for System Management. accepted to ICAC 2005.
