Publikationen zum Fachbereich Petrinetze

Bücher und Konferenzbände

• Jörg Desel, Peter Kemper, Ekkart Kindler, and Andreas Oberweis, editors. Algorithmen und Werkzeuge für Petrinetze, 5. Workshop, number 694 of Forschungsberichte, October 1998. Universität Dortmund, Fachbereich Informatik.

• Wolfgang Reisig. Petrinetze, Eine Einführung. Springer, 1982. Note: Mit Übersetzungen ins Chinesische, Englische, Italienische, Japanische und Polnische.

Dissertationen und Habilitationen

• Michael Weber. Allgemeine Konzepte zur software-technischen Unterstützung verschiedener Petrinetz-Typen. Dissertation, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, December 2002.

  Abstract: Petrinetze werden in vielen Bereichen als Modellierungstechnik verwendet. Die verschiedenen Einsatzgebiete und Modellierungsziele erfordern dabei unterschiedliche Typen von Petrinetzen. Einen Petrinetz-Typ kennzeichnen -- neben den üblichen Stellen, Transitionen und Kanten -- eine Menge zusätzlicher, spezifischer Elemente, sowie eine spezifische Schaltregel. In der Literatur findet man zahlreiche verschiedene Petrinetz-Typen. Diese Vielfalt an Petrinetz-Typen lässt sich nicht ohne weiteres überblicken. Deshalb fehlt es auch nicht an Versuchen, allgemeine Petrinetz-Typen oder Klassifikationen -- auch einzelner Aspekte -- zu etablieren. Allerdings erfassen die bisherigen Ansätze nur einen kleinen Teil aller Petrinetz-Typen. Unser semantisch orientierter Klassifizierungsansatz des Petrinetz-Hyperwürfels umfasst deutlich mehr Petrinetz-Typen und erhebt den Anspruch, universell zu sein. Der Petrinetz-Hyperwürfel hat einen syntaktisch orientierten Klassifizierungsansatz als Grundlage. Dieser Ansatz führt einerseits zum Vorschlag der Petri Net Markup Language. Damit können Petrinetze aller Typen einheitlich beschrieben werden. Andererseits führt derselbe Ansatz zu einer Basis für Petrinetz-Werkzeuge, in der die einzelnen Teile eines Petrinetz-Typs unabhängig voneinander implementiert werden. Der Petrinetz-Kern ist eine derartige Basis mit dessen Hilfe Petrinetz-Werkzeuge gebaut werden. Er implementiert Konzepte, die allen Petrinetzen gemein sind, unabhängig von konkreten Petrinetz-Typen. Gemeinsam mit dem Petrinetz-Hyperwürfel bildet der Petrinetz-Kern ein weiteres Basiswerkzeug für einen parametrisierten Petrinetz-Typ mit einer parametrisierten Schaltregel. Die Petri Net Markup Language und der Petrinetz-Kern sind die wesentlichen Beiträge der vorliegenden Arbeit. Gemeinsam bilden sie ein mächtiges Grundgerüst für Petrinetz-Werkzeuge beliebiger Petrinetz-Typen.

  

• Sibylle Peuker. Halbordnungsbasierte Verfeinerung zur Verifikation verteilter Algorithmen. Dissertation, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, July 2001.

  Abstract: In dieser Arbeit geht es um die schrittweise Verfeinerung verteilter Algorithmen. Dabei wird ein einfacher Algorithmus, der einige gewünschte Eigenschaften hat, Schritt für Schritt zu einem komplexen Algorithmus verfeinert, der konkrete Implementationsanforderungen erfüllt, so daß in jedem Schritt die gewünschten Eigenschaften erhalten bleiben. Wir stellen einen neuen eigenschaftserhaltenden Verfeinerungsbegriff vor, der auf der kausalen Ordnung der Aktionen eines Algorithmus basiert. Diesen Begriff definieren wir als Transitionsverfeinerung für elementare Petrinetze und diskutieren Beweiskriterien. Danach definieren und diskutieren wir die simultane Verfeinerung mehrerer Transitionen. Zur Modellierung komplexer verteilter Algorithmen sind elementare Petrinetze oft nicht adäquat. Wir benutzen deshalb algebraische Petrinetze. Wir definieren Transitionsverfeinerung für algebraische Petrinetze und stellen einen Zusammenhang zur simultanen Verfeinerung von Transitionen in elementaren Petrinetzen her. Transitionsverfeinerung ist besonders für Verfeinerungsschritte geeignet, in denen synchrone Kommunikation zwischen Agenten durch asynchronen Nachrichtenaustausch ersetzt wird. Wir zeigen dies am Beispiel eines komplexen verteilten Algorithmus, zur Berechnung des minimalen spannenden Baumes in einem gewichteten Graphen. Wir zeigen die Korrektheit dieses Algorithmus in mehreren Schritten, von denen einige Schritte Transitionsverfeinerungen sind. In anderen Schritten sind klassische Verfeinerungsbegriffe ausreichend. Wir übertragen deshalb auch einen klassischen Verfeinerungsbegriff in unser formales Modell.

  

• Tobias Vesper. Petrinetze zum Entwurf selbststabilisierender Algorithmen. Dissertation, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, December 2000.

  Abstract: Edsger W. Dijkstra prägte im Jahr 1974 den Begriff Selbststabilisierung (self-stabilization) in der Informatik. Ein System ist selbststabilisierend, wenn es von jedem denkbaren Zustand aus nach einer endlichen Anzahl von Aktionen ein stabiles Verhalten erreicht. Im Mittelpunkt dieser Arbeit steht der Entwurf selbststabilisierender Algorithmen. Wir stellen eine Petrinetz-basierte Methode zum Entwurf selbststabilisierender Algorithmen vor. Wir validieren unsere Methode an mehreren Fallstudien: Ausgehend von algorithmischen Ideen existierender Algorithmen beschreiben wir jeweils die die schrittweise Entwicklung eines neuen Algorithmus. Dazu gehört ein neuer randomisierter selbststabilisierender Algorithmus zur Leader Election in einem Ring von Prozessoren. Dieser Algorithmus ist abgeleitet aus einem publizierten Algorithmus, von dem wir hier erstmals zeigen, daß er fehlerhaft arbeitet. Wir weisen die Speicherminimalität unseres Algorithmus nach. Ein weiteres Ergebnis ist der erste Algorithmus, der ohne Time-Out-Aktionen selbststabilisierenden Tokenaustausch in asynchronen Systemen realisiert. Petrinetze bilden einen einheitlichen formalen Rahmen für die Modellierung und Verifikation dieser Algorithmen.

  

Publikationen in Zeitschriften und Büchern

• Wolfgang Reisig. The Decent Philosophers: An Exercise in Concurrent Behaviour. Fundamenta Informaticae, 80(1-3): 273-281, November 2007.

  Abstract: Concurrent runs reveal more insight into distributed systems than interleaved runs. This is shown by help of Dijkstra's paradigm of five philosophers.

  

• Wilfried Brauer and Wolfgang Reisig. Carl Adam Petri und die ``Petrinetze''. Informatik-Spektrum, 29(5): 369--381, October 2006.

• Wolfgang Reisig, Karsten Schmidt, and Christian Stahl. Kommunizierende Workflow-Services modellieren und analysieren. Informatik - Forschung und Entwicklung, pp 90-101, October 2005.

  Abstract: Zur adäquaten Nutzung von Workflow-Implementierungen kommunizierender Geschäftsprozesse werden Konzepte vorgeschlagen,die von konkreten Implementierungen abstrahieren. Auf der Basis von Petrinetzen werden unterschiedliche Varianten der Bedienbarkeit von Workflows charakterisiert und dafür Entscheidungsalgorithmen vorgestellt. Die Angemessenheit des Ansatzes wird am Beispiel der Semantik von Komponenten der Geschäftsprozess-Modellierungssprache BPEL demonstriert.

  

• Wolfgang Reisig. Petrinetze: Grundfragen, Konzepte, Konsequenzen. Arbeitspapiere der GMD, (497), 1990.

Konferenzbeiträge und Beiträge auf Workshops

• Dirk Fahland. A scenario is a behavioral view - Orchestrating services by scenario integration. In Oliver Kopp and Niels Lohmann, editors, Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, pages 8-14, March 2009. CEUR-WS.org.

  Abstract: The construction of a complex service orchestration is a tedious and error-prone task as multiple service interactions with a single orchestrating service must be specified and combined. We suggest to specify a service orchestration in terms of behavioral scenarios that capture a specific aspect of service interaction, a behavioral view in isolation. By synchronizing the different scenarios, the views get integrated and define the behavior of a complex service orchestration. Our formal model for scenarios and their integration is a class of Petri nets called oclets.

  

• Dirk Fahland. Oclets - scenario-based modeling with Petri nets. In Giuliana Franceschinis and Karsten Wolf, editors, Proceedings of the 30th International Conference on Petri Nets and Other Models Of Concurrency, 22-26 May 2009, volume 5606 of Lecture Notes in Computer Science, Paris, France, pages 223-242, June 2009. Springer-Verlag. Note: (revised version).

  Abstract: We present a novel, operational, formal model for scenario-based modeling with Petri nets. A scenario-based model describes the system behavior in terms of partial runs, called scenarios. This paradigm has been formalized in message sequence charts (MSCs) and live sequence charts (LSCs) which are in industrial and academic use. A particular application for scenarios are process models in disaster management where system behavior has to be adapted frequently, occasionally at run-time. An operational semantics of scenarios would allow to execute and adapt such systems on a formal basis. In this paper, we present a class of Petri nets for specifying and modeling systems with scenarios and anti-scenarios. We provide an operational semantics allowing to iteratively construct partially ordered runs that satisfy a given specification. We prove the correctness of our results.

  

• Dirk Fahland, Cédric Favre, Barbara Jobstmann, Jana Koehler, Niels Lohmann, Hagen Völzer, and Karsten Wolf. Instantaneous Soundness Checking of Industrial Business Process Models. In Umeshwar Dayal, Johann Eder, Jana Koehler, and Hajo Reijers, editors, Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings, volume 5701 of Lecture Notes in Computer Science, September 2009. Springer-Verlag.

• Dirk Fahland, Daniel Lübke, Jan Mendling, Hajo Reijers, Barbara Weber, Matthias Weidlich, and Stefan Zugal. Declarative versus Imperative Process Modeling Languages: The Issue of Understandability. In John Krogstie, Terry Halpin, and Erik Proper, editors, Proceedings of the 14th International Conference on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD'09), volume 29 of Lecture Notes in Business Information Processing, Amsterdam, The Netherlands, pages 353-366, June 2009. Springer-Verlag. Note: (to appear).

  Abstract: Advantages and shortcomings of different process modeling languages are heavily debated, both in academia and industry, but little evidence is presented to support judgements. With this paper we aim to contribute to a more rigorous, theoretical discussion of the topic by drawing a link to well-established research on program comprehension. In particular, we focus on imperative and declarative techniques of modeling a process. Cognitive research has demonstrated that imperative programs deliver sequential information much better while declarative programs offer clear insight into circumstantial information. In this paper we show that in principle this argument can be transferred to respective features of process modeling languages. Our contribution is a pair of propositions that are routed in the cognitive dimensions framework. In future research, we aim to challenge these propositions by an experiment.

  

• Dirk Fahland, Jan Mendling, Hajo Reijers, Barbara Weber, Matthias Weidlich, and Stefan Zugal. Declarative vs. Imperative Process Modeling Languages: The Issue of Maintainability. In Bela Mutschler, Roel Wieringa, and Jan Recker, editors, 1st International Workshop on Empirical Research in Business Process Management (ER-BPM'09), Ulm, Germany, pages 65-76, September 2009. Note: (LNBIP to appear).

  Abstract: The rise of interest in declarative languages for process modeling both justifies and demands empirical investigations into their presumed advantages over more traditional, imperative alternatives. Our concern in this paper is with the ease of maintaining business process models, for example due to changing performance or conformance demands. We aim to contribute to a rigorous, theoretical discussion of this topic by drawing a link to well-established research on maintainability of information artifacts.

  

• Dirk Fahland. Adaptive und Selbststabilisierende Workflows. In Malte Diehl, Henrik Lipskoch, Roland Meyer, and Christian Storm, editors, Proceedings des gemeinsamen Workshops der Graduiertenkollegs, Trustworthy Software Systems, Berlin, pages 55--56, 2008. Gito-Verlag.

• Dirk Fahland. Oclets -- Scenario-Based Modeling with Petri Nets. In Niels Lohmann and Karsten Wolf, editors, Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008, volume 380 of CEUR Workshop Proceedings, pages 1-6, September 2008. CEUR-WS.org.

  Abstract: Scenario-based specifications are used for modeling highly-complex, distributed systems in terms of partial runs (scenarios) the system shall have. But it is difficult to derive an implementing, operational model from a given set of scenarios, especially if concepts like anti-scenarios which must not occur are used. In this paper, we present a novel model for scenario-based specifications with Petri nets including anti-scenarios; we provide an operational semantics for our model.

  

• Dirk Fahland and Heiko Woith. Towards Process Models for Disaster Response. In Business Process Management Workshops, International Workshop on Process Management for Highly Dynamic and Pervasive Scenarios (PM4HDPS), co-located with 6th International Conference on Business Process Management (BPM'08), volume 17 of Lecture Notes in Business Information Processing, Milan, Italy, pages 254-265, September 2008. Springer.

  Abstract: In the immediate aftermath of a disaster routine processes, even if specifically designed for such a situation, are not enacted blindly. Actions and processes rather adapt their behavior based on observations and available information. Attempts to support these processes by technology rely on process models that faithfully capture process execution and adaptation. Based on experiences from actual disaster response settings, we propose to specify an adaptive process as a set of scenarios using a Petri net syntax. Our operational model provides an adaptation operator that synthesizes and adapts the system behavior at run-time based on the given scenarios. An example illustrates our approach.

  

• Dirk Fahland. Modeling and Verifying Declarative Workflows. In Dagstuhl ''zehn plus eins'', Aachen, pages 135, 2007. Verlagshaus Mainz.

• Dirk Fahland. Synthesizing Petri nets from LTL specifications - An engineering approach. In Stephan Philippi and Alexander Pinl, editors, Proceedings 14.Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN), Arbeitsbericht aus dem Fach Informatik, Nr. 25/2007, Universität Koblenz-Landau, D, pages 69--74, September 2007.

  Abstract: In this paper we present a pattern-based approach for synthesizing truly distributed Petri nets from a class of LTL specifications. The synthesis allows for the automatic, correct generation of humanly conceivable Petri nets, thus circumventing a manual construction of nets, or the use of Büuchi automata which are not distributed and often less intuitive to understand.

  

• Dirk Fahland. Towards Analyzing Declarative Workflows. In Jana Koehler, Marco Pistore, Amit P. Sheth, Paolo Traverso, and Martin Wirsing, editors, Autonomous and Adaptive Web Services, number 07061 of Dagstuhl Seminar Proceedings, 2007. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany.

  Abstract: Enacting tasks in a workflow cannot always follow a pre-defined process model. In application domains like disaster management workflows are partially specified and circumstances of their enactment change. There exist various approaches for formal workflow models that are effective in such situations, like declarative specifications instead of operational models for formalizing flexible workflow process. These powerful models leave a gap to existing techniques in the domain of workflow modeling, workflow analysis, and workflow management. In this paper we bridge this gap with a compositional mechanism for translating declarative workflow models to operational workflow models. The mechanism is of a general nature and we reveal its principles as we provide an exemplary definition for translating DecSerFlow models based on LTL to Petri nets. We then demonstrate its use in analyzing and refining declarative models.

  

• Andreas Glausch. Eine Charakterisierung einfacher Petrinetz-Schemata. In Karsten Schmidt and Christian Stahl, editors, 12. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2005), Proceedings, pages 1-6, September 2005. Humboldt-Universität zu Berlin.

  Abstract: Wir untersuchen die Ausdrucksmächtigkeit von Petrinetz-Schemata. Dazuführen wir die Teilklasse der einfachen Petrinetz-Schemata ein und zeigen, welche Systeme sich durch ein einfaches Petrinetz-Schema darstellen lassen und welche nicht. Die hinreichenden und notwendigen Eigenschaften dazu formulieren wir in einem Theorem.

  

• Ekkard Kindler and Tobias Vesper. Automatisch überprüfbare Beweistechniken für algebraische Petrinetze. In Jörg Desel, Ekkard Kindler, and Andreas Oberweis, editors, 3. Workshop Algorithmen und Werkzeuge für Petrinetze, pages 33-38, October 1996. Institut AIFB, Universität Karlsruhe.

Technische Berichte

• Dirk Fahland. Oclets - a formal approach to adaptive systems using scenario-based concepts. Informatik-Berichte 223, Humboldt-Universität zu Berlin, 2008.

  Abstract: Usually, a component in a distributed system has assumptions about the remaining components of the system. A change in one component might require to change other components as well. It may happen that the change has to be performed in the running system. In this paper, we propose a formal model for systems that change their behavior at run-time: An adaptive system is denoted as a set of scenarios using a Petri net syntax. Our operational model provides an adaptation operator that synthesizes and adapts the system behavior as a Petri net branching-process at run-time based on the given scenarios. We show the feasibility of our approach by the help of an example.

  

• Dirk Fahland. Translating UML2 Activity Diagrams Petri Nets for analyzing IBM WebSphere Business Modeler process models. Informatik-Berichte 226, Humboldt-Universität zu Berlin, 2008.

  Abstract: We present a formal semantics for a variant of UML2 Activity Diagrams that is used in the IBM WebSphere Business Modeler for modeling business processes. Business process models created in the IBM WebSphere Business Modeler or with other UML2 modeling tools often constitutes one of the key specification artifacts for building an information system that implements or supports the specified processes. As UML2 Activity Diagrams lack a universally agreed semantics, the step from specification to implementation usually faces a semantical impedance caused by different interpretation of the same diagram. A well-defined formal semantics for the specification language determines the interpretation of a diagram and allows for reasoning about as well as validating and verifying a given specification on common (formal) grounds. We adapt approaches for formalizing semantics of UML2 Activity Diagrams and apply them to the core features of the IBM WebSphere Business Modeler language for purpose of formal verification. We provide a parameterized Petri net pattern for each language concepts. A diagram is translated by instantiating a pattern for each use of a concept; merging the resulting Petri net fragments according to the structure of the original diagram yields a Petri net that specifies the behavioral semantics of the diagram. The resulting Petri net can be verified for control-flow errors using the model checker LoLA. The semantics has been implemented in a tool that is available at http://www.service-technology.org/uml2owfn/.

  

• Bodo Hohberg, Wolfgang Reisig, and Bixia Wu. Entwurf und Verifikation nachrichtenbasierter verteilter Algorithmen durch verteilende Verfeinerung. Informatik-Berichte 216, Humboldt-Universität zu Berlin, 2007.

  Abstract: Um Entwurf und Verifikation komplizierter verteilter Algorithmen leichter und verständlicher zu machen, wird oft eine Verfeinerungsmethode verwendet. Dabei wird ein einfacher Algorithmus, der gewünschte Eigenschaften erfüllt, schrittweise zu einem komplizierten Algorithmus verfeinert. In jedem Schritt sollen die gewünschten Eigenschaften erhalten bleiben. Für nachrichtenbasierte verteilte Algorithmen, die durch Petrinetze modelliert werden, haben wir eine neue Verfeinerungsmethmode entwickelt. Wir beginnen mit einem Anfangsalgorithmus, der Aktionen enthält, die gemeinsame Aufgaben mehrerer Agenten beschreiben. In jedem Schritt verfeinern wir eine dieser Aktionen zu einem Netz, das nur solche Aktionen enthält, die die Aufgaben einzelner Agenten beschreiben. Jeder Schritt ist also eine Verteilung einer unverteilten Aktion, also eine verteilende Verfeinerung. Die Arbeit klärt den Zusammenhang von Eigenschaften des Verfeinerungsnetzes und den bei der Verfeinerung gültig bleibenden Eigenschaften des verfeinerten Algorithmus. Hierbei sind Kausalitäten im Verfeinerungsnetz von entscheidender Bedeutung. Die Anwendung der Methode wird in der Arbeit an anschaulichen Beispielen demonstriert.

  

• Wolfgang Reisig, Karsten Schmidt, and Christian Stahl. Verteilte Geschäftsprozesse modellieren und analysieren. Informatik-Berichte 182, Humboldt-Universität zu Berlin, February 2005.

  Abstract: Verteilte Geschäftsprozesse nutzen das Internet, um auf heterogenen Rechnerstrukturen Dienste auszubieten. Modellierungstechniken und Implementierungssprachen für solche Dienste werfen im Vergleich mit herkömmlichen Rechnern grundlegend neue Fragestellungen auf. Wir diskutieren einige davon und zeigen, wie Petrinetze ihre Beantwortung ermöglichen.

  

• Karsten Schmidt and Christian Stahl. 12. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2005), Proceedings. Informatik-Berichte 192, Humboldt-Universität zu Berlin, September 2005.

• Jörg Desel, Ekkard Kindler, and Andreas Oberweis. Algorithmen und Werkzeuge für Petrinetze, 4. Workshop. Informatik-Berichte 85, Humboldt-Universität zu Berlin, September 1997.

Studien- und Diplomarbeiten

• Daniel Janusz. Implementierung zweier Algorithmen zur Abstraktion von Petrinetzen. Studienarbeit, Humboldt-Universität zu Berlin, April 2008.

• Thomas Pillat. Gegenüberstellung struktureller Reduktionstechniken für Petrinetze. Diplomarbeit, Humboldt-Universität zu Berlin, March 2008.

  Abstract: Petrinetze sind eine formale Methode zur Modellierung und Analyse von Systemen. Ein großes Problem bei der Analyse von Petrinetzen ist die Größe des Zustandsraums. Um dieses Problem abzuschwächen, können Reduktionstechniken eingesetzt werden. Petrinetze sind einer der wenigen Formalismen, die die Möglichkeit bieten, bereits die Struktur des Modells zu reduzieren. Diese strukturellen Reduktionstechniken verändern die Struktur des Netzes und bewahren dabei bestimmte Eigenschaften des ursprünglichen Modells. Es existieren eine Vielzahl wissenschaftlicher Arbeiten, die strukturelle Reduktionstechniken untersuchen. In der vorliegenden Arbeit werden strukturelle Reduktionstechniken einander gegenübergestellt und katalogisiert. Es wird ermittelt, welche Eigenschaften eines ursprünglichen Natzes durch die Anwendung der Reduktionstechnik bewahrt und für welche Netzklasse diese Reduktionstechnik gilt. Die Reduktionstechniken werden miteinander verglichen und die Beziehungen der Regeln zueinander ermittelt. Basierend auf diesen Ergebnissen wird ein Katalog erstellt, der beschreibt, für welche Netzklasse das Anwenden einer Regel welche Eigenschaften bewahrt.

  

• Konstanze Swist. Modellierung des Workflows der Task Force Erdbeben des GFZ mit Petrinetzen. Studienarbeit, Humboldt-Universität zu Berlin, October 2008.

• Manja Wolf. Erstellung einer modellbasierten Laufzeitumgebung für adaptive Prozesse. Diplomarbeit, Humboldt-Universität zu Berlin, September 2008.

  Abstract: Mit der vorliegenden Arbeit wird die Implementation von GRETA - Graphical Runtime EnvironmenT for Adaptive Processes vorgestellt. GRETA ist eine modellbasierte Laufzeitumgebung für dynamische, sich während des Ablaufes anpassende Prozesse. Für die Implementation wurde ein formales Begriffsgebäude aufgebaut, das auf einer noch in der Entwicklung befindlichen Theorie basiert und einen Teil dieser Theorie berücksichtigt. Die Theorie, das vereinfachte Begriffsgebäude und die dafür ausgearbeiteten Algorithmen werden vorgestellt. GRETA wurde als grafischer Editor implementiert, mit dem solche dynamischen Prozesse modelliert werden können und wurde zu einem Simulationswerkzeug erweitert. Mit GRETA ist es möglich, zukünftige Forschungsergebnisse zu der genannten Theorie zu erproben. Das Programm wurde mit dem Eclipse-Framework GMF (Graphical Modeling Framework) erstellt. In dem Dokument gibt es eine Einführung in die Konzepte und die Funktionalittät von GMF. Die für GRETA genutzten Features von GMF werden erläutert.

  

• Jens Kleine. Transformation von offenen Workflow-Netzen zu abstrakten WS-BPEL-Prozessen. Diplomarbeit, Humboldt-Universität zu Berlin, July 2007.

  Abstract: In dieser Arbeit präsentieren wir eine Transformation von offenenWorkflow-Netzen zu abstrakten WS-BPEL-Prozessen. Als Web Services implementierte Geschäftsprozesse sind zunehmend verbreiteter und von größerer finanzieller Bedeutung. Daher müssen sie vor ihrem Einsatz auf wichtige Eigenschaften wie korrekte Terminierung oder Bedienbarkeit überprüft werden. Die häufig eingesetzte Modellierungssprache WS-BPEL ist jedoch auf Grund ihrer fehlenden formalen Semantik nicht analysierbar. Aus diesem Grund existieren Werkzeuge zur Überführung von WS-BPEL-Prozessen in die Petrinetzklasse der offenen Workflow-Netze. Für diese kann auf eine Reihe von Tools zur formalen Analyse von Geschäftsprozessen zurückgegriffen werden. Unsere Transformation ermöglicht es, die Ergebnisse dieser Analysewerkzeuge vollautomatisch in WS-BPEL-Prozesse zurück zu übersetzen. So können unter anderem Beispiele für im Prozess auftretende Fehler und bedienende Partner als WS-BPEL-Code an den Anwender zurückgegeben werden, ohne dass dieser sich dazu mit den, in den Zwischenschritten der Analyse verwendeten, Petrinetzen auskennen muss. Zudem bietet unsere Transformation die Möglichkeit Geschäftsprozesse graphbasiert als offene Workflow-Netze zu modellieren und diese anschließend automatisch in einen abstrakten WS-BPEL-Prozess zu übersetzen.

  

• Jens Kleine. Abstrakte Petrinetzmuster für BPEL unter Bewahrung von Verklemmungen. Studienarbeit, Humboldt-Universität zu Berlin, October 2006.

  Abstract: Wir präsentieren die Reduktion einer Petrinetzsemantik für die Business Process Execution Language for Web Services, die alle Verklemmungen bewahrt und dabei die Petrinetzmuster so stark verkleinert, dass Model-Checking größerer Geschäftsprozesse ermöglicht wird. Dies geschieht, indem wir jedes Petrinetzmuster einzeln betrachten und verkleinern. Bisherige Versuche der computergestützten Analyse scheiterten auf Grund der Größe und Komplexität der entstandenen Petrinetze.

  

• Peter Laufer. Grundlagen für die Anpassung der Petrinetz-Semantik an WS-BPEL 2.0. Studienarbeit, Humboldt-Universität zu Berlin, May 2006.

  Abstract: Die Business Process Execution Language for Web Services (BPEL) ist eine Sprache zur Definitionvon Geschäftsprozessen als Web Services. Um Eigenschaften eines BPEL-Prozesses verifizieren zu können, entwickelte Stahl eine Transformation von BPEL4WS 1.1 in Petrinetze. Als Ergebnis des Standardisierungsprozesses von BPEL wird demnächst die Version WS-BPEL 2.0 verabschiedet werden. Da auch WS-BPEL 2.0 eine textuelle informelle Spezifikation zugrunde liegen wird, wäre eine angepasste Petrinetz-Semantik für Verifikationszwecke weiterhin sehr hilfreich. Ziel dieser Arbeit ist es deshalb, die nderungen von WS-BPEL 2.0 im Vergleich zum Vorgänger BPEL4WS 1.1 zu dokumentieren und Vorschläge in Bezug auf die Anpassung der vorhandenen Petrinetz-Semantik zu geben. Die Betrachtungen beziehen sich dabei auf eine Entwurfsfassung der kommenden Spezifikation von WS-BPEL 2.0 vom 16. März 2006.

  

• Carsten Frenkler. Modellierung und Analyse transaktionaler Geschäftsprozesse. Diplomarbeit, Humboldt-Universität zu Berlin, July 2005.

  Abstract: Die vorliegende Arbeit beschäftigt sich mit zwei wichtigen Aspekten von Geschäftsprozessen. Das ist einerseits die Frage, ob die Funktionalität eines Prozesses genutzt werden kann und andererseits die Frage, ob die Transaktionen eines Prozesses vernünftig verarbeitet werden können. Für die Analyse der beiden Aspekte wird ein geeignetes Modell benötigt. Hierfür werden die auf Petrinetzen basierenden Workflow-Module erweitert, indem transaktionale Eigenschaften in ein Petrinetz übersetzt werden und in das Modul integriert werden. Letztlich liefert die Analyse der Bedienbarkeit des erweiterten Moduls eine Antwort auf beide Fragen.

  

• Sebastian Hinz. Implementierung einer Petrinetz-Semantik für BPEL. Diplomarbeit, Humboldt-Universität zu Berlin, March 2005.

  Abstract: BPEL ist eine Modellierungssprache zur Beschreibung von verteilten Geschäftsprozessen mit Webservices. Um mit formalen Methoden die Sprache selbst und in BPEL modellierte Prozesse verifizieren zu können, wird eine formale Semantik benötigt. Auf der Basis von Petrinetzen wurde bereits eine solche Semantik entwickelt. Um die Analyse eines Prozesses zu ermöglichen wird ein Werkzeug benötigt, das die Transformation des Prozesses in ein Petrinetz übernimmt. In der vorliegenden Arbeit wird ein solches Werkzeug entwickelt, vorgestellt und seine Funktionsweise erläutert.

  

• Elke Salecker and Nora Toussaint. Gegenbeispielgesteuerte Abstraktionsverfeinerung in High-Level-Petrinetzen. Diplomarbeit, Humboldt-Universität zu Berlin, September 2005.

• Carsten Frenkler. BPEL-Boxen. Ein Modell zur Integration von Transaktionskonzepten in Geschäftsprozesse mit Petrinetzen. Studienarbeit, Humboldt-Universität zu Berlin, February 2004.

• Lars Kuhtz. TLDA und Petrinetze. Studienarbeit, Humboldt-Universität zu Berlin, April 2004.

• Christian Stahl. Transformation von BPEL4WS in Petrinetze. Diplomarbeit, Humboldt-Universität zu Berlin, April 2004.

  Abstract: BPEL4WS ist eine Sprache zur Beschreibung verteilter Geschäftsprozesse mit Web Services. Es besteht die Notwendigkeit, die Sprache trotz ihrer Komplexität zu verstehen, um mit ihr im Umfeld von Web Services arbeiten zu können. Mit Hilfe einer formalen Semantik ist es möglich, die Sprache selbst und mit BPEL4WS spezifizierte Geschäftsprozesse zu verifizieren. In der vorliegenden Arbeit wird eine Petrinetz-Semantik für BPEL4WS vorgestellt. Dazu wird gezeigt, dass jedes Konstrukt der Sprache BPEL4WS in ein Petrinetz-Muster übersetzt werden kann. Damit ist es möglich, jeden in der Geschäftsprozesssprache BPEL4WS modellierten Geschäftsprozess in ein Petrinetz zu transformieren. Bei der Entwicklung der Semantik kann auf Forschungsergebnisse aus dem Bereich "Petrinetze als Werkzeug zur Geschäftsprozessmodellierung" zurückgegriffen werden.

  

• Wolf Richter. Spezifikation und Implementation organisationsübergreifender Geschäftsprozesse mit Petrinetzen. Diplomarbeit, Humboldt-Universität zu Berlin, 2002.

• Juliane Dehnert and Ines Schwenzer. Dialogmodellierung mit Petrinetzen - Das FAN-Dialogmodell. Diplomarbeit, Humboldt-Universität zu Berlin, August 1998.

• Jörn Freiheit. Arc-Typed-Petrinetze. Verifikation eines Datenbankmanagementsystems mit Datenreplikation. Diplomarbeit, Humboldt-Universität zu Berlin, May 1997.

• Axel Martens. Software-Engineering von Workflow-Applikationen mit Petrinetzen. Diplomarbeit, Humboldt-Universität zu Berlin, August 1997.

• Michael Weber. unless-Aspekte und ihr Beitrag zur Verifikation von mit Petrinetzen modellierten Systemen. Diplomarbeit, Humboldt-Universität zu Berlin, January 1997.

zurück zur Übersicht