Teilprojekt D3
Aus GRK-Wiki
zum übergeordneten Forschungsbereich
Inhaltsverzeichnis |
Bedienbarkeit, Komposition und Rücksetzbarkeit von Workflows
Workflows der im Graduiertenkolleg betrachteten Art können als Implementierungen von Geschäftsprozessen aufgefasst werden. Grundlegende Fragestellungen an Workflows sind damit im Rahmen von Geschäftsprozessen beantwortbar. Beispielsweise die folgenden: Ist ein Workflow bedienbar? Simuliert er einen gegebenen anderen? Sind zwei Workflows komponierbar, sind sie äquivalent, bildet der eine eine Umgebung des anderen? Ganz besonders wichtig sind Fragen der Rücksetzbarkeit (Kompensation) von Aktionen. Für die Verifikation der o. g. Eigenschaften müssen sie zunächst formal dargestellt werden. Dafür hat sich temporale Logik, in verschiedenen Varianten und Ausdrucksstärken durchgesetzt. Eine für Workflows wichtige Eigenschaft ist beispielsweise die Bedienbarkeit durch einen anderen Workflow oder allgemein durch mehrere andere, die entweder unabhängig voneinander agieren oder sich synchronisieren. Ein weiteres Beispiel ist die Eigenschaft eines Workflows, eine (oder sogar die liberalste) bedienende Umgebung eines gegebenen Workflows zu sein.
Stand des Wissens
Die Entwicklung theoretisch begründeter Konzepte, verfügbarer Werkzeuge und implementierter Workflow-Engines verläuft derzeit stürmisch. Modelliert wird dabei nur in Teilen. Allerdings gibt es bereits eine gut ausgebaute Theorie für Geschäftsprozessmodelle, mit Petrinetzen als bevorzugtem Ausdrucksmittel für Kontrollstrukturen und Abstract State Machines für semantische Aspekte.
Vorarbeiten der beteiligten Wissenschaftler
Seit Ende der 90er Jahre untersucht die Arbeitsgruppe von W. Reisig Fragen der Modellierung von Geschäftsprozessen und der Analyse von Geschäftsprozessmodellen. Die Habilitation [1] systematisiert verschiedene Transaktionsbegriffe, die für das Graduiertenkolleg nützlich sind. In [2] werden Workflows als spezielle Petrinetzmodule betrachtet. Neben Petrinetzen wurden insbesondere Abstract State Machines (ASM) zur Modellierung herangezogen. [3] schlägt liberale Begriffe für Geschäftsprozessmodelle und ihre Komposition vor, so dass beliebige Modelle komponierbar sind. [4] konzentriert sich auf Fehlerbehandlung und Kompensation am Beispiel der Sprache BPEL4WS. Der Begriff der verteilten Bedienbarkeit wurde in mehreren Arbeiten untersucht [5], [6], [7]. Die relevanten Vorarbeiten von H. Schlingloff betreffen hauptsächlich die temporale Spezifikation und Analyse von Abläufen sowie deren Anwendung in verschiedenen Praxisbereichen [8]. Von beiden Betreuern der geplanten Dissertation wurde eine Reihe von Techniken zum Model-Checking entwickelt und implementiert, speziell zur Verifikation von Petrinetzen [9], [10]. Diese Techniken können in der geplanten Arbeit vorteilhaft eingesetzt werden. Die enge Kooperation zwischen den Arbeitsgruppen von W. Reisig und H. H. Schlingloff wird durch die aktuelle Publikation [11] dokumentiert. Seit einem Jahr ist Dr. Martens an das IBM T. J. Watson Research Center in New York beurlaubt. Damit erhält das Graduiertenkolleg Einblick in aktuelle Forschungslinien der IBM im Bereich Web Services und Workflow-Engines für spezielle Anwendungen über die einschlägigen Publikationen (siehe [12], [13], [14] sowie [15], [16], [17], [18]) hinaus. Die aktuellen Arbeiten von J. Fischer zur Sprachtransformation auf Metamodellebene [19] runden das Spektrum an Vorarbeiten für dieses Dissertationsvorhaben ab.
Geplante Arbeiten
Eine erste Aufgabe der geplanten Dissertation ist es, die Unterschiede herkömmlicher und im Graduiertenkolleg verwendeter Workflows formal herauszuarbeiten. In der Dissertation sollen dann typische Workflows der im Graduiertenkolleg untersuchten Katastrophenmanagementsysteme mit den Kalkülen Petrinetze und ASM modelliert werden. Möglichkeiten einer automatischen Generierung dieser Modelle aus sprachbasierten Workflow-Beschreibungen (E1, E3) sind zu betrachten und im Erfolgsfall generell zu priorisieren. Den zentralen Schwerpunkt bildet die Verifikation der entwickelten Modelle, also der prinzipielle Nachweis der Bedienbarkeit, Simulierbarkeit, Komponierbarkeit und Äquivalenz. Eine wichtige Technik ist dabei das Model-Checking. Ziel der Arbeit ist die Vervollkommnung der Modellierungs- und Analyseverfahren für Workflows der im Kolleg vorkommenden Art, die sowohl auf der Ebene des Katastrophenmagements (E3) als auch auf der P2P-Middleware-Ebene (D1) zum Einsatz kommen.
Referenzen
[1] E. Kindler: Systematische Spezifikation und Verifikation von Datenkonsistenzkriterien. Habilitationsschrift, Mathematisch-Naturwissenschaftliche Fakultät der Humboldt-Universität zu Berlin, 2000.
[2] A. Martens: Verteilte Geschäftsprozesse - Modellierung und Verifikation mithilfe von Web Services. Dissertation, Institut für Informatik, Humboldt-Universität zu Berlin, erschienen in WiKu: Stuttgart, Berlin & Paris, 2003.
[3] W. Reisig: Modelling- and Analysis Techniques for Web Services and Business Processes. Athen, 2005.
[4] D. Fahland, W. Reisig: ASM-based Semantics for BPEL- The Negative Control Flow. In: International ASM Conference 2005, Paris, März 2005.
[5] W. Reisig, K. Schmidt, Christian Stahl: Verteilte Geschäftsprozesse modellieren und analysieren. Informatik-Berichte Nr. 182, Humboldt-Universität zu Berlin, 2004.
[6] K. Schmidt: Distributed Usability of Web Services. In: E. Kindler (ed.): Proc. 11th Workshop on Algorithms and Tools for Petri Nets (AWPN '04), pp. 19-24, Paderborn 2004.
[7] K. Schmidt: Controlability of Business Processes, Informatik-Bericht 180, Humboldt-Universität zu Berlin. 2004.
[8] H. Schlingloff, M. Friske: Von Use Cases zu Test Cases- Eine systematische Vorgehensweise. In: MBEES - Model Based Engineering of Embedded Systems Dagstuhl (Dez. 2004). T. Klein, B. Rumpe, B. Schätz (eds.); TU Braunschweig Report TUBS-SSE 2005-01, 2005.
[9] H. Schlingloff: Partial State Space Analysis of Safety-Critical Systems. Habilitation Thesis, University of Bremen, Juni 2001.
[10] W. Reisig: Modeling- and Analysis Techniques for Web Services and Business Processes. Informatik-Bericht 183, Humboldt-Universität zu Berlin, 2004.
[11] A. Martens, H. Schlingloff, K. Schmidt: Modeling and Model Checking Web Services. Accepted for ENTCS - Electronic Notes in Theoretical Computer Science; Elsevier, 2005.
[12] A. Martens, C. Stahl, D.Weinberg, D. Fahland, T. Heidinger: Business Process Execution Language for Web Services – Semantik, Analyse und Visualisierung. Informatik-Berichte Nr. 169, Humboldt-Universität zu Berlin, Juli 2004.
[13] A. Martens: Analysis and re-engineering of Web Services. In: Tagungsband of 6th International Conference on Enterprise Information Systems (ICEIS'04). Porto, Portugal, 2004.
[14] A. Martens: Verteilte Geschäftsprozesse - Modellierung und Verifikation mit Hilfe von Web Services. WiKu-Verlag 2004.
[15] W. Reisig, A. Brade: ASM Models for Web Services. Informatik Bericht 181, Humboldt-Universität zu Berlin, 2004.
[16] K. Schmidt: Automated Generation of a Progress Measure for the Sweep-Line Method. Proc. 10th Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2004, LNCS 2988, pp. 192 - 204, 2004.
[17] K. Schmidt, C. Stahl: A Petri net semantic for BPEL4WS - validation and application. In: E. Kindler (ed.): Proc. 11th Workshop on Algorithms and Tools for Petri Nets (AWPN '04), pp. 1 - 6, Paderborn, 2004.
[18] J. M. Vidal, P. Buhler, C. Stahl: Multiagent systems with workflows. IEEE Internet Computing, 8(1), pp. 76 - 82, Januar 2004.
[19] J. Fischer, A.Kunert, M.Piefel, M. Scheidgen: Toolbased ULF-Ware - An Open Framework for Integrated Tools for ITU-T Languages. In: Proc. of 12th International SDL Forum, Grimstad May 2005. Appears in LCNS 2005.
