## Publikationen (nach Gebiet sortiert)

### Konferenzbeiträge auf Workshops

• Fahland, Dirk, Weidlich, Matthias
Scenario-based process modeling with Greta
Marcello La Rosa, editors
In Proc. of BPM Demonstration Track 2010, Hoboken, USA, September 14-16, 2010, volume 615 of CEUR-WS.org, Hoboken, USA, September 2010
Designing understandable business process models is one of the key factors to successful business process management. Current modeling practices advocate the use of block-oriented concepts and subprocesses to structure complex process models. However, such guidelines cannot be applied in any case as case studies in process mining have shown. Previously, we proposed the scenario-based paradigm to structure models of complex processes in behavioral fragments, i.e., scenarios. This paper presents GRETA as a tool that supports scenario-based process modeling and execution.
close
close
• Fahland, Dirk
Oclets - scenario-based modeling with Petri nets
Giuliana Franceschinis and Karsten Wolf, editors
In 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, Springer-Verlag, Paris, France, jun 2009
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.
close
close
• Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
John Krogstie and Terry Halpin and Erik Proper, editors
In 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, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
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.
close
close
• Fahland, Dirk, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
Declarative vs. Imperative Process Modeling Languages: The Issue of Maintainability
Stefanie Rinderle-Ma and Shazia Wasim Sadiq and Frank Leymann, editors
In Business Process Management Workshops, BPM 2009 International Workshops, Ulm, Germany, September 7, 2009. Revised Papers, volume 43 of Lecture Notes in Business Information Processing, Springer, Ulm, Germany, sep 2009
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.
close
close
• Fahland, Dirk, Woith, Heiko
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, Springer, Milan, Italy, September 2008
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.
close
close
• Fahland, Dirk
Diehl, Malte and Lipskoch, Henrik and Meyer, Roland and Storm, Christian, editors
In Proceedings des gemeinsamen Workshops der Graduiertenkollegs, Trustworthy Software Systems, Gito-Verlag, Berlin, 2008
close
• Fahland, Dirk
Oclets -- Scenario-Based Modeling with Petri Nets
Niels Lohmann and Karsten Wolf, editors
In 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, CEUR-WS.org, sep 2008
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.
close
close
• Fahland, Dirk
A Formal Approach to Adaptive Processes using Scenario-based Concepts.
Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, Siedlce, Poland, jun 2007
The problem and need for adapting business processes and service behavior to cope with changing circumstances is identified well. Standard models for business processes still rely on a fixed process logic, the change of which is rather hard to achieve. Ad-hoc changes to a standard model are usually considered too dangerous' as they are performed in not well-defined manner. Other models for adaptive processes deviate to some extent from established business process models. This deviation comes at the price of limited understandability and loss in analysis capabilities. We propose a model for adaptive processes based on Petri nets which have successfully been applied in modeling and analyzing business process and web services. Our operator to adapt the behavior of such models is formalized by the help of scenario-based concepts known from live-sequence charts in purely mathematical terms. This combination of concepts allows to write down the result of the adaptation rather than how adaptation shall be performed.
close
close
• Fahland, Dirk
Synthesizing Petri nets from LTL specifications - An engineering approach
Philippi, Stephan and Pinl, Alexander, editors
In , , September 2007
close
close
• Fahland, Dirk
Modeling and Verifying Declarative Workflows
In Dagstuhl ''zehn plus eins'', Verlagshaus Mainz, Aachen, 2007
close
• Fahland, Dirk
Towards Analyzing Declarative Workflows
Jana Koehler and Marco Pistore and Amit P. Sheth and Paolo Traverso and Martin Wirsing, editors
In Autonomous and Adaptive Web Services, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007
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.
close
close
• ### Studien- und Diplomarbeiten

• Wolf, Manja

Diplomarbeit, sep 2008
close
close
• ### Technische Berichte

• Fahland, Dirk
Oclets - a formal approach to adaptive systems using scenario-based concepts
Informatik-Berichte, Humboldt-Universität zu Berlin, 2008
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.
close
close

## Architecture Framework

### Konferenzbeiträge auf Workshops

• Aalst, Wil M. P. van der, Beisiegel, Michael, Hee, Kees M. van, König, Dieter, Stahl, Christian
A SOA-Based Architecture Framework
Frank Leymann and Wolfgang Reisig and Satish R. Thatte and Wil M. P. van der Aalst, editors
In The Role of Business Processes in Service Oriented Architectures, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, nov 2006
In this paper we present first results of a SOA-based architecture framework. The architecture framework is required to be close to industry standards, especially to service component architecture (SCA), language independent (i.e. it is adoptable) and the building blocks of each system, activities and data, are first class citizens. We present a meta model of the architecture framework and discuss its concepts in detail.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Hee, Kees van, Verbeek, Eric, Stahl, Christian, Sidorova, Natalia
A Framework for Linking and Pricing No-Cure-No-Pay Services
Kurt Jensen and Wil M. P. van der Aalst, editors
volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2, Springer-Verlag, mar 2009
In this paper, we present a framework that allows us to orchestrate web services such that the web services involved in this orchestration interact properly. To achieve this, we predefine service interfaces and certain routing constructs. Furthermore, we define a number of rules to incrementally compute the price of such a properly interacting orchestration (i.e. a web service) from the price of its web services. The fact that a web service gets only payed after its service is delivered (no-cure-no-pay) is reflected by considering a probability of success. To determine a safe price that includes the risk a web service takes, we consider the variance of costs.
close
close
• Aalst, Wil M. P. van der, Beisiegel, Michael, Hee, Kees M. van, König, Dieter, Stahl, Christian
An SOA-based architecture framework
volume 2 of International Journal of Business Process Integration and Management (IJBPIM) 2 (2), 2007
We present an Service-Oriented Architecture (SOA)-based architecture framework. The architecture framework is designed to be close to industry standards, especially to the Service ComponentArchitecture (SCA).The framework is language independent and the building blocks of each system, activities and data, are first class citizens.We present a meta model of the architecture framework and discuss its concepts in detail. Through the framework, concepts of an SOA such as wiring, correlation and instantiation can be clarified.
close
close
• ### Technische Berichte

• Hee, Kees M. van, Verbeek, H.M.W., Stahl, Christian, Sidorova, Natalia
A Framework for Linking and Pricing No-Cure-No-Pay Services
Computer Science Report, Technische Universiteit Eindhoven, Eindhoven, The Netherlands, jun 2008
In this paper, we present a framework that allows us to orchestrate web services such that the web services involved in this orchestration interact properly. To achieve this, we predefine service interfaces and certain routing constructs. Furthermore, we define a number of rules to incrementally compute the price of such a properly interacting orchestration (i.e. a web service) from the price of its web services. The fact that a web service gets only payed after its service is delivered (no-cure-no-pay) is reflected by considering a probability of success. To determine a safe price that includes the risk a web service takes, we consider the variance of costs.
close
close
• Hee, Kees M. van, Sidorova, Natalia, Stahl, Christian, Verbeek, H. M. W.
A Price of Service in a Compositional SOA Framework
Computer Science Report, Technische Universiteit Eindhoven, The Netherlands, jul 2007
In this paper we propose a framework for SOA covering such important features as proper termination (soundness) and correct correlation of tasks. Within this framework, we define a method for the calculation of the price of services. Our framework is compositional in the sense that composing a system from subsystems that meet our correctness requirements we obtain a system that still meets these requirements.
close
close
• Aalst, Wil M. P. van der, Beisiegel, Michael, Hee, Kees M. van, König, Dieter, Stahl, Christian
A SOA-Based Architecture Framework
Computer Science Report, Technische Universiteit Eindhoven, The Netherlands, jan 2007
We present a SOA-based architecture framework. The architecture framework is designed to be close to industry standards, especially to the Service Component Architecture (SCA). The framework is language independent and the building blocks of each system, activities and data, are first class citizens. We present a \emphmeta model of the architecture framework and discuss its concepts in detail. Through the framework concepts such as wiring, correlation, and instantiation can be clarified. This allows us to demystify some of the confusion related to SOA.
close
close

## Asm

### Konferenzbeiträge auf Workshops

• A Semantic Characterization of Unbounded-Nondeterministic ASMs
In Proceedings of the 2nd Conference on Algebra and Coalgebra in Computer Science, volume 4624 of Lecture Notes in Computer Science, aug 2007
Universal algebra usually considers and examines algebras as static entities. In the mid 80ies Gurevich proposed Abstract State Machines (ASMs) as a computation model that regards algebras as dynamic: a state of an ASM is represented by a freely chosen algebra which may change during a computation. In 2000, Gurevich characterized the class of sequential ASMs in a purely semantical way by five amazingly general and elegant axioms. Later this result has been extended to bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among unboundedly many (sometimes infinitely many) alternatives. We characterize the class of unbounded-nondeterministic ASMs by an extension of Gurevich's original axioms for sequential ASMs. We apply this result to prove the reversibility of unbounded-nondeterministic ASMs.
close
close
• Glausch, Andreas
A Semantic Characterization of Elementary Wide-Step ASMs
In Proceedings of the 14th International ASM Workshop, jun 2007
close

• ASM-based semantics for BPEL: The negative Control Flow
, editors
In Proceedings of the 12th International Workshop on Abstract State Machines (ASM'05), Paris XII, mar 2005
BPEL is presently the most prominent language to specify and execute business processes, using Web Services as its technological basis. Particular problems arise when activities are faulty: faults have to be propagated, other activities have to be irregularly terminated, etc. We describe the formal semantics of fault handlers and event handlers, demonstrating that ASMs are most adequate for this purpose.
close
close
• Reisig, Wolfgang
The Computable Kernel of ASM
, editors
In Abstract State Machines, Advances in Theory and Practice, 10th International Workshop, ASM 2003, Taormina, Italy, volume 2589 of Lecture Notes in Computer Science, 2003
A rich variety of system models for sequential, deterministic systems has been suggested during recent decades, including automata, process algebras, many versions of Petri Nets, and models to describe the semantics of Programming languages. All models for sequential, deterministic systems assume a set S of states, or configurations, and a next state function $\upsilon: S \rightarrow S$.
close
close
• Reisig, Wolfgang
Towards an ASM Thesis for Unconventional Algorithms
Yuri Gurevich and Philipp W. Kutter and Martin Odersky and Lothar Thiele, editors
In Abstract State Machines, volume 1912 of Lecture Notes in Computer Science, Springer-Verlag, 2000
All descriptions of algorithms, be they formal or informal, employ data structures, operations on them, and some policy to cause operations be applied to data. Gurevich calls a formal description technique for algorithms algorithm universal if it allows for each informally described algorithm a formal representation that would essentially make precise the notions used in the informal description, not employing additional data, operations or steps. Gurevich's ASM thesis claims Abstract State Machines be algorithm universal for conventional, sequential algorithms. Here we are behind properties of formal presentations that are algorithm universal for unconventional, distributed algorithms.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Reisig, Wolfgang
Abstract State Machines for the Classroom - The Basics
Dines Bjorner; Henson, Martin C. (Eds.), editors
volume XXII, 624 p. 69 illus., Hardcover of Monographs in Theoretical Computer Science. An EATCS Series, Logics of Specification Languages XXII, 624 p. 69 illus., Hardcover, 2008
Abstract State Machines (henceforth referred to as just ASM) were introduced as ä computation model that is more powerful and more universal than standard computation models\" by Yuri Gurevich in 1985. Here we provide some intuitive and motivating arguments, and characteristic examples for (the elementary version of) ASM. The intuition of ASM as a formal framework for \"pseudocode\" algorithms is highlightes. Generalizing variants of the fundamental \"sequential small-step\" version of ASM are also considered.
close
close
• Reisig, Wolfgang
The Expressive Power of Abstract State Machines
volume 22 of Computing and Informatics 22 (3), 2003
Conventional computation models assume symbolic representations of states and actions. Gurevich's "Abstract-State Machine" model takes a more liberal position: Any mathematical structure may serve as a state. This results in "a computational model that is more powerful and more universal than standard computation models". We characterize the Abstract-State Machine model as a special class of transition systems that widely extends the class of "computable" transition systems. This characterization is based on a fundamental Theorem of Y. Gurevich.
close
close
• Reisig, Wolfgang
On Gurevich's Theorem on Sequential Algorithms
volume 39 of Acta Informatica 39 (5), Springer-Verlag, 2003
Abstract-State Machines have been introduced as ?a computation model that is more powerful and more universal than standard computation models?, by Yuri Gurevich in 1985 ([Gur85]). ASM gained much attention as a specification method, in particular for the description of the semantics of programming languages, communication protocols, distributed algorithms, etc. Gurevich proved recently that a sequential algorithm must only meet a few, liberal requirements, to be representable as an ASM. We re-formulate Gurevich?s requirements for sequential algorithms, as well as the semantics of ASM-programs and the proof of his main theorem. A couple of examples support and explain intuition and motivation of ASM.
close
close
• ### Studien- und Diplomarbeiten

Diplomarbeit, sep 2005
close
close
• Glausch, Andreas
Varianten des ASM-Theorems
Diplomarbeit, jun 2005
close
close
ASMs und die Struktur und Dynamik von Web Services
Studienarbeit, jan 2005
close
• Fahland, Dirk
Ein Ansatz einer formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines
Studienarbeit, aug 2004
close
close
• Glausch, Andreas
Abstract-State Machines - Eine Sammlung didaktischer Beispiele
Studienarbeit, feb 2003
Diese Studienarbeit versucht durch eine Vielzahl von Beispielen den Begriff Abstract-State Machine und sequenzieller Algorithmus didaktisch sinnvoll darzustellen. Es werden dabei sowohl Beispiele als auch Gegenbeispiele angegeben, um Umfang und Grenzen dieser Begriffe aufzuzeigen.
close
close
• ### Technische Berichte

• Distributed Abstract State Machines and Their Expressive Power
Informatik-Berichte, Humboldt-Universität zu Berlin, jan 2006
Gurevich's sequential Abstract State Machines (ASMs)are taken as a basis for the construction of distributed ASMs as sets of sequential ASMs. A theorem on the expressive power of distributed ASMs is proven in analogy to Gurevich's classical theorem on the expressive power of sequential ASMs.
close
close
• Fahland, Dirk
Complete Abstract Operational Semantics for the Web Service Business Process Execution Language
Informatik-Berichte, , sep 2005
close
close

## Bdd

### Konferenzbeiträge auf Workshops

• Kaschner, Kathrin, Massuthe, Peter, Wolf, Karsten

Daniel Moldt, editors
In , , sep 2006
close
• ### Publikationen in Zeitschriften und Büchern

• Kaschner, Kathrin, Massuthe, Peter, Wolf, Karsten
Symbolic Representation of Operating Guidelines for Services
volume 72 of Petri Net Newsletter 72, apr 2007
close

## Bedienbarkeit

### Konferenzbeiträge auf Workshops

• Reisig, Wolfgang, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela, Wolf, Karsten, Kaschner, Kathrin
Analysis Techniques for Service Models
In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, IEEE Computer Society, nov 2006
The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.
close
close
• Weinberg, Daniela, Schmidt, Karsten
Reduction Rules for Interaction Graphs
Karsten Schmidt and Christian Stahl, editors
In , , sep 2005
The internet today has grown to be more than just being a basisfor exchanging information. It steadily becomes a platform for processing business processes. Many companies distribute their service with the help of web services or integrate other web services into their own workflow. However, before a web service gets published it should be examined well. We will introduce a way of examining the controllability of a web service. We propose the interaction graph of a web service, that is modelled by an open workflow net. To verify whether such a net is controllable or not it is sufficient to construct a reduced interaction graph. We will define reduction rules that minimize the size of the graph greatly. The analysis using the interaction graph as well as the reduction rules are implemented and have been integrated into an analysis tool kit for web services.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Massuthe, Peter, Serebrenik, Alexander, Sidorova, Natalia, Wolf, Karsten
Can I find a Partner? Undecidablity of Partner Existence for Open Nets
volume 108 of Information Processing Letters 108 (6), Nov 2008
close
• Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian
Kommunizierende Workflow-Services modellieren und analysieren
Informatik - Forschung und Entwicklung, Springer-Verlag, oct 2005
close
close
• ### Studien- und Diplomarbeiten

• Strukturelle Analyse von offenen Workflow-Netzen hinsichtlich Bedienbarkeit
Studienarbeit, jan 2007
close
• Schulz, Alexander
Zielgerichtete Strategien
Studienarbeit, jul 2007
close
• Gierds, Christian

Studienarbeit, oct 2007
close
close
• ### Technische Berichte

• Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian

Informatik-Berichte, , feb 2005
close
close
• Martens, Axel, Stahl, Christian, Weinberg, Daniela, Fahland, Dirk, Heidinger, Thomas
Business Process Execution Language for Web services - Semantik, Analyse und Visualisierung
Informatik-Berichte, , jul 2004
close
close

## Bedienungsanleitung

### Dissertationen und Habilitationen

• Stahl, Christian
Service Substitution - A Behavioral Approach Based on Petri Nets
Dissertation, Dec 2009
Service-Oriented Computing is an emerging computing paradigm that supports the modular design of (software) systems. Complex systems are designed by composing less complex systems, called services. Such a (complex) system is a distributed application often involving several cooperating enterprises. As a system usually changes over time, individual services will be substituted by other services. Substituting one service by another one should not affect the correctness of the overall system. Assuring correctness becomes particularly challenging, as the services rely on each other, and each of the involved enterprises only oversees a part of the overall system. In addition, services communicate asynchronously which makes the analysis even more difficult. For this reason, formal methods to support service substitution are indispensable. In this thesis, we study service substitution at the level of service models. Thereby we restrict ourselves to service behavior. As a formalism to model service behavior, we use Petri nets. The first contribution of this thesis is the definition of several substitutability criteria that are suitable in the context of Service-Oriented Computing. Substituting a service S by a service S' should preserve some behavioral properties of the overall system. For each set of behavioral properties and a given service S, there exists a set of behaviorally compatible services for S. A substitutability criterion defines which of these behaviorally compatible services of S have to be preserved by S'. We relate our substitutability criteria to preorders and equivalences known from process theory. The second contribution of this thesis is to present, for each substitutability criterion, a procedure to decide whether a service S' can substitute a service S. The decision requires the comparison of the in general infinite sets of behaviorally compatible services for the services S and S'. Hence, we extend existing work on an abstract representation of all behaviorally compatible services for a given service. For each notion of behavioral compatibility, we present an algorithmic solution to represent all behaviorally compatible services. Based on these representations, we can decide substitutability of a service S by a service S'. The third contribution of this thesis is a method to support the design of a service S' that can substitute a service $S$ according to a substitutability criterion. Our approach is to derive a service S' from the service S by stepwise transformation. To this end, we present several transformation rules. Finally, we formalize and we extend the equivalence notion for services specified in the language WS-BPEL. That way, we demonstrate the applicability of our work.
close
close
• ### Konferenzbeiträge auf Workshops

• Liske, Nannette, Lohmann, Niels, Stahl, Christian, Wolf, Karsten
Another Approach to Service Instance Migration
Luciano Baresi and Chi-Hung Chi and Jun Suzuki, editors
In Service-Oriented Computing - ICSOC 2009, 7th International Conference, Stockholm, Sweden, November 24-27, 2009. Proceedings, Lecture Notes in Computer Science, Springer-Verlag, nov 2009
Services change over time, be it for internal improvements, be it for external requirements such as new legal regulations. For long running services, it may even be necessary to change a service while instances are actually running and interacting with other services. This problem is referred to as instance migration. We present a novel approach to the behavioral (service protocol) aspects of instance migration. We apply techniques for finitely characterizing the set of all correctly interacting partners to a given service. The approach assures that migration does not introduce behavioral problems with any running partner of the original service. Our technique scales up to services with thousands of states, including models of real WS-BPEL processes.
close
close
• Stahl, Christian, Wolf, Karsten
Covering Places and Transitions in Open Nets
Marlon Dumas and Manfred Reichert, editors
In Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, Springer-Verlag, sep 2008
We present a finite representation of all services M where the composition with a given service N is deadlock-free, and a given set of activities of N can be covered (i.e. is not dead). Our representation is an extension of the existing notion of an operating guideline which only cared about deadlock freedom. We further present an algorithm to decide whether a service M matches with the extended operating guideline of N.
close
close
• Reisig, Wolfgang, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela, Wolf, Karsten, Kaschner, Kathrin
Analysis Techniques for Service Models
In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, IEEE Computer Society, nov 2006
The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
volume 53 of The Computer Journal 53 (1), 2010
To implement an interorganizational process between different enterprizes, one needs to agree on the rules of engagement''. These can be specified in terms of a contract that describes the overall intended process and the duties of all parties involved. We propose to use such a process-oriented contract which can be seen as the composition of the public views of all participating parties. Based on this contract each party may locally implement its part of the contract such that the implementation (the private view) agrees on the contract. In this paper, we propose a formal notion for such process-oriented contracts and give a criterion for accordance between a private view and its public view. The public view of a party can be substituted by a private view if and only if the private view accords with the public view. Using the notion of accordance the overall implemented process is guaranteed to be deadlock-free and it is always possible to terminate properly. In addition, we present a technique for automatically checking our accordance criterion. A case study illustrates how our proposed approach can be used in practice.
close
close
• Stahl, Christian, Wolf, Karsten
Deciding Service Composition and Substitutability Using Extended Operating Guidelines
volume 68 of Data Knowl. Eng. 68 (9), 2009
We study the correct interaction between services using the following notion for correctness: there is no deadlock in the interaction of the services, and a given set of activities is not dead, that is, each activity in this set is executed in at least one run. The second condition has not been studied before. An operating guideline of a service P is an operational characterization of all deadlock-free interacting partners of P. In this paper, we present an extension of the concept of an operating guideline to characterize all correctly interacting partners of a service P. This extension can be used for answering at least the following two questions. First, given a service R, does R interact correctly with P? Second, given a service P', can P be substituted by P', that is, is every correctly interacting partner of P a correctly interacting partner of P', too?
close
close

• Deciding Substitutability of Services with Operating Guidelines
Kurt Jensen and Wil M. P. van der Aalst, editors
volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2 (5460), Springer-Verlag, mar 2009
Deciding whether a service S can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of restriction can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
close
close
• ### Studien- und Diplomarbeiten

• Gierds, Christian
Strukturelle Reduktion von Bedienungsanleitungen
Diplomarbeit, jan 2008
close
close
• ### Technische Berichte

• Deciding Substitutability of Services with Operating Guidelines
Informatik-Berichte, Humboldt-Universität zu Berlin, apr 2008
Deciding whether a service $S$ can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of deprecation can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
close
close

## Bpel

### Konferenzbeiträge auf Workshops

• Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
John Krogstie and Terry Halpin and Erik Proper, editors
In 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, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
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.
close
close
• König, Dieter, Lohmann, Niels, Moser, Simon, Stahl, Christian, Wolf, Karsten
Extending the Compatibility Notion for Abstract WS-BPEL Processes
Wei-Ying Ma and Andrew Tomkins and Xiaodong Zhang, editors
In Proceedings of the 17th International Conference on World Wide Web, WWW 2008, Beijing, China, April 21--25, 2008, apr 2008
WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.
close
close
• Lohmann, Niels
A Feature-Complete Petri Net Semantics for WS-BPEL 2.0
Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, jun 2007
We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.
close
close
• Reisig, Wolfgang, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela, Wolf, Karsten, Kaschner, Kathrin
Analysis Techniques for Service Models
In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, IEEE Computer Society, nov 2006
The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.
close
close

• Analyzing Interacting BPEL Processes
In Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings, volume 4102 of Lecture Notes in Computer Science, Springer-Verlag, sep 2006
This paper addresses the problem of analyzing theinteraction between BPEL processes. We present a technology chain that starts out with a BPEL process and transforms it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). A case study demonstrates the value of this technology chain.
close
close

• ASM-based semantics for BPEL: The negative Control Flow
, editors
In Proceedings of the 12th International Workshop on Abstract State Machines (ASM'05), Paris XII, mar 2005
BPEL is presently the most prominent language to specify and execute business processes, using Web Services as its technological basis. Particular problems arise when activities are faulty: faults have to be propagated, other activities have to be irregularly terminated, etc. We describe the formal semantics of fault handlers and event handlers, demonstrating that ASMs are most adequate for this purpose.
close
close
• Martens, Axel
Simulation and Equivalence between BPEL Process Models
In Proceedings of the Design, Analysis, and Simulation of Distributed Systems Symposium (DASD'05), Part of the 2005 Spring Simulation Multiconference (SpringSim'05), San Diego, California, apr 2005
The integration of business process across the boundaries of individual enterprises or business units is becoming increasingly important. In this scenario, process models play an all-important role. On the one hand, the interaction between the participating companies often is specified globally, for example by means of multiple abstract process models - one for each partner. On the other hand, each partner defines its local process autonomously in terms of an executable process model. The important question is whether such an executable model is consistent to the predefined abstract model. This paper defines a simulation relation between BPEL process models, and presents a method to verify consistency automatically, on top of it.
close
close
• Hinz, Sebastian, Schmidt, Karsten, Stahl, Christian
Transforming BPEL to Petri Nets
Wil M. P. van der Aalst and B. Benatallah and F. Casati and F. Curbera, editors
In Proceedings of the Third International Conference on Business Process Management (BPM 2005), volume 3649 of Lecture Notes in Computer Science, Springer-Verlag, Nancy, France, sep 2005
We present a Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation). The semantics is implemented as a parser that translates BPEL specifications into the input language of the Petri net model checking tool LoLA. We demonstrate that the semantics is well suited for computer aided verification purposes.
close
close
• Schmidt, Karsten, Stahl, Christian
A Petri net semantic for BPEL4WS - validation and application
Ekkart Kindler, editors
In Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN'04), , oct 2004
We translated a small business process into a recently defined Petri net semantic. Then we used the tool LoLA for validating the semantic as well as for proving relevant properties of the particular process.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Lohmann, Niels, Verbeek, Eric, Ouyang, Chun, Stahl, Christian
Comparing and Evaluating Petri Net Semantics for BPEL
volume 4 of International Journal of Business Process Integration and Management (IJBPIM) 4 (1), 2009
We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modelling decisions. These decisions together with their consequences are discussed. We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.
close
close

• Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation
volume 64 of Data Knowl. Eng. 64 (1), jan 2008
We address the problem of analyzing the interaction between WS-BPEL processes. We present a technology chain that starts out with a WS-BPEL process and translates it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). To manage processes of realistic size, we present a concept of a \emphflexible model generation which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.
close
close
• Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian
Kommunizierende Workflow-Services modellieren und analysieren
Informatik - Forschung und Entwicklung, Springer-Verlag, oct 2005
close
close
• Vidal, Jose M., Buhler, Paul, Stahl, Christian
Multiagent Systems with Workflows
volume 8 of IEEE Internet Computing 8 (1), feb 2004
Industry and researchers have two different visions for the future of Web services. Industry wants to capitalize on Web service technology to automate business processes via centralized workflow enactment. Researchers are interested in the dynamic composition of Web services. The authors show how these two visions are points in a continuum and discuss a possible path for bridging the gap between them.
close
close
• ### Studien- und Diplomarbeiten

• Diplomarbeit, mar 2008
close
close
• Kleine, Jens

Studienarbeit, oct 2006
close
close
• Laufer, Peter

Studienarbeit, may 2006
close
close
• Hinz, Sebastian

Diplomarbeit, mar 2005
close
close
• Fahland, Dirk
Ein Ansatz einer formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines
Studienarbeit, aug 2004
close
close
• Frenkler, Carsten

Studienarbeit, feb 2004
close
• Stahl, Christian
Transformation von BPEL4WS in Petrinetze
Diplomarbeit, apr 2004
close
close
• Heidinger, Thomas
Statische Analyse von BPEL4WS-Prozessmodellen
Studienarbeit, dec 2003
close
• Weinberg, Daniela

Studienarbeit, aug 2003
close
• ### Technische Berichte

• Lohmann, Niels, Verbeek, H. M. W., Ouyang, Chun, Stahl, Christian, Aalst, Wil M. P. van der
Comparing and Evaluating Petri Net Semantics for BPEL
Computer Science Report, Technische Universiteit Eindhoven, The Netherlands, aug 2007
We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modeling decisions. These decisions together with their consequences are discussed.We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.
close
close
• König, Dieter, Lohmann, Niels, Moser, Simon, Stahl, Christian, Wolf, Karsten
Extending the Compatibility Notion for Abstract WS-BPEL Processes
Preprint, Universität Rostock, Rostock, Germany, nov 2007
WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.
close
close
• Lohmann, Niels
A Feature-Complete Petri Net Semantics for WS-BPEL 2.0 and its Compiler BPEL2oWFN
Informatik-Berichte, Humboldt-Universität zu Berlin, aug 2007
We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification. This technical report is the extended version of the papers [1, 2] and can be seen as the sequel of [3].
close
close
• Fahland, Dirk
Complete Abstract Operational Semantics for the Web Service Business Process Execution Language
Informatik-Berichte, , sep 2005
close
close
• Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian

Informatik-Berichte, , feb 2005
close
close
• Stahl, Christian
A Petri Net Semantics for BPEL
Informatik-Berichte, , jul 2005
We present a pattern-based Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics is complete - it covers the standard behaviour of BPEL as well as the exceptional behav-iour (e.g. faults, events, compensation). Therefore every business process specified in BPEL can be transformed into a Petri net.
close
close
• Martens, Axel, Stahl, Christian, Weinberg, Daniela, Fahland, Dirk, Heidinger, Thomas
Business Process Execution Language for Web services - Semantik, Analyse und Visualisierung
Informatik-Berichte, , jul 2004
close
close

## Bpel-semantik

### Konferenzbeiträge auf Workshops

• König, Dieter, Lohmann, Niels, Moser, Simon, Stahl, Christian, Wolf, Karsten
Extending the Compatibility Notion for Abstract WS-BPEL Processes
Wei-Ying Ma and Andrew Tomkins and Xiaodong Zhang, editors
In Proceedings of the 17th International Conference on World Wide Web, WWW 2008, Beijing, China, April 21--25, 2008, apr 2008
WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.
close
close
• Lohmann, Niels
A Feature-Complete Petri Net Semantics for WS-BPEL 2.0
Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, jun 2007
We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.
close
close

• Analyzing Interacting BPEL Processes
In Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings, volume 4102 of Lecture Notes in Computer Science, Springer-Verlag, sep 2006
This paper addresses the problem of analyzing theinteraction between BPEL processes. We present a technology chain that starts out with a BPEL process and transforms it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). A case study demonstrates the value of this technology chain.
close
close
• Hinz, Sebastian, Schmidt, Karsten, Stahl, Christian
Transforming BPEL to Petri Nets
Wil M. P. van der Aalst and B. Benatallah and F. Casati and F. Curbera, editors
In Proceedings of the Third International Conference on Business Process Management (BPM 2005), volume 3649 of Lecture Notes in Computer Science, Springer-Verlag, Nancy, France, sep 2005
We present a Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation). The semantics is implemented as a parser that translates BPEL specifications into the input language of the Petri net model checking tool LoLA. We demonstrate that the semantics is well suited for computer aided verification purposes.
close
close

• ASM-based semantics for BPEL: The negative Control Flow
, editors
In Proceedings of the 12th International Workshop on Abstract State Machines (ASM'05), Paris XII, mar 2005
BPEL is presently the most prominent language to specify and execute business processes, using Web Services as its technological basis. Particular problems arise when activities are faulty: faults have to be propagated, other activities have to be irregularly terminated, etc. We describe the formal semantics of fault handlers and event handlers, demonstrating that ASMs are most adequate for this purpose.
close
close
• Schmidt, Karsten, Stahl, Christian
A Petri net semantic for BPEL4WS - validation and application
Ekkart Kindler, editors
In Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN'04), , oct 2004
We translated a small business process into a recently defined Petri net semantic. Then we used the tool LoLA for validating the semantic as well as for proving relevant properties of the particular process.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Lohmann, Niels, Verbeek, Eric, Ouyang, Chun, Stahl, Christian
Comparing and Evaluating Petri Net Semantics for BPEL
volume 4 of International Journal of Business Process Integration and Management (IJBPIM) 4 (1), 2009
We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modelling decisions. These decisions together with their consequences are discussed. We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.
close
close

• Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation
volume 64 of Data Knowl. Eng. 64 (1), jan 2008
We address the problem of analyzing the interaction between WS-BPEL processes. We present a technology chain that starts out with a WS-BPEL process and translates it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). To manage processes of realistic size, we present a concept of a \emphflexible model generation which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.
close
close
• ### Studien- und Diplomarbeiten

• Laufer, Peter

Studienarbeit, may 2006
close
close
• Kleine, Jens

Studienarbeit, oct 2006
close
close
• Hinz, Sebastian

Diplomarbeit, mar 2005
close
close
• Fahland, Dirk
Ein Ansatz einer formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines
Studienarbeit, aug 2004
close
close
• Stahl, Christian
Transformation von BPEL4WS in Petrinetze
Diplomarbeit, apr 2004
close
close
• ### Technische Berichte

• Lohmann, Niels, Verbeek, H. M. W., Ouyang, Chun, Stahl, Christian, Aalst, Wil M. P. van der
Comparing and Evaluating Petri Net Semantics for BPEL
Computer Science Report, Technische Universiteit Eindhoven, The Netherlands, aug 2007
We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modeling decisions. These decisions together with their consequences are discussed.We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.
close
close
• Lohmann, Niels
A Feature-Complete Petri Net Semantics for WS-BPEL 2.0 and its Compiler BPEL2oWFN
Informatik-Berichte, Humboldt-Universität zu Berlin, aug 2007
We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification. This technical report is the extended version of the papers [1, 2] and can be seen as the sequel of [3].
close
close
• Fahland, Dirk
Complete Abstract Operational Semantics for the Web Service Business Process Execution Language
Informatik-Berichte, , sep 2005
close
close
• Stahl, Christian
A Petri Net Semantics for BPEL
Informatik-Berichte, , jul 2005
We present a pattern-based Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics is complete - it covers the standard behaviour of BPEL as well as the exceptional behav-iour (e.g. faults, events, compensation). Therefore every business process specified in BPEL can be transformed into a Petri net.
close
close
• Martens, Axel, Stahl, Christian, Weinberg, Daniela, Fahland, Dirk, Heidinger, Thomas
Business Process Execution Language for Web services - Semantik, Analyse und Visualisierung
Informatik-Berichte, , jul 2004
close
close

## Dawn

### Konferenzbeiträge auf Workshops

• Baar, Thomas, Kindler, Ekkart,
Verifying Intuition - ILF Checks DAWN Proofs
In Application and Theory of Petri Nets, 20th International Conference, ICATPN '99, Proceedings, volume 1639 of Lecture Notes in Computer Science, Springer-Verlag, 1999
The DAWN approach allows to model and verify distributed algorithms in an intuitive way. At a first glance, a DAWN proof may appear to be informal. In this paper, we argue that DAWN proofs are formal and can be checked for correctness fully automatically by automated theorem provers. The basic technique are proof rules which generate proof obligations. For the definition of the proof rules we adopt assertions and we introduce conflict formulas for algebraic Petri nets. Experiments show that the generated proof obligations can be automatically checked by theorem provers.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Baar, Thomas, Kindler, Ekkart
ILF and DAWN for verifying distributed algorithms - an idea for a tool
volume 37 of Fundamenta Informaticae 37 (3), feb 1999
close
• ### Studien- und Diplomarbeiten

• Abdourahaman
DAWN-ILF Tool. Modelchecking Anwendung
Diplomarbeit, sep 2000
close
• Unger, S.

Diplomarbeit, oct 1999
close
• ### Technische Berichte

• Baar, Thomas, Kindler, Ekkart
Einsatz von ILF und DAWN zur Verifikation verteilter Algorithmen - Eine Vorstudie
Informatik-Berichte, , mar 1998
close

• DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen
Informatik-Berichte, , dec 1997
close

## Deklarative Modelle

### Konferenzbeiträge auf Workshops

• Fahland, Dirk, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
Declarative vs. Imperative Process Modeling Languages: The Issue of Maintainability
Stefanie Rinderle-Ma and Shazia Wasim Sadiq and Frank Leymann, editors
In Business Process Management Workshops, BPM 2009 International Workshops, Ulm, Germany, September 7, 2009. Revised Papers, volume 43 of Lecture Notes in Business Information Processing, Springer, Ulm, Germany, sep 2009
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.
close
close
• Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
John Krogstie and Terry Halpin and Erik Proper, editors
In 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, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
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.
close
close
• Fahland, Dirk
Modeling and Verifying Declarative Workflows
In Dagstuhl ''zehn plus eins'', Verlagshaus Mainz, Aachen, 2007
close
• Fahland, Dirk
Synthesizing Petri nets from LTL specifications - An engineering approach
Philippi, Stephan and Pinl, Alexander, editors
In , , September 2007
close
close
• Fahland, Dirk
Towards Analyzing Declarative Workflows
Jana Koehler and Marco Pistore and Amit P. Sheth and Paolo Traverso and Martin Wirsing, editors
In Autonomous and Adaptive Web Services, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007
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.
close
close

## Exchangeability

### Dissertationen und Habilitationen

• Stahl, Christian
Service Substitution - A Behavioral Approach Based on Petri Nets
Dissertation, Dec 2009
Service-Oriented Computing is an emerging computing paradigm that supports the modular design of (software) systems. Complex systems are designed by composing less complex systems, called services. Such a (complex) system is a distributed application often involving several cooperating enterprises. As a system usually changes over time, individual services will be substituted by other services. Substituting one service by another one should not affect the correctness of the overall system. Assuring correctness becomes particularly challenging, as the services rely on each other, and each of the involved enterprises only oversees a part of the overall system. In addition, services communicate asynchronously which makes the analysis even more difficult. For this reason, formal methods to support service substitution are indispensable. In this thesis, we study service substitution at the level of service models. Thereby we restrict ourselves to service behavior. As a formalism to model service behavior, we use Petri nets. The first contribution of this thesis is the definition of several substitutability criteria that are suitable in the context of Service-Oriented Computing. Substituting a service S by a service S' should preserve some behavioral properties of the overall system. For each set of behavioral properties and a given service S, there exists a set of behaviorally compatible services for S. A substitutability criterion defines which of these behaviorally compatible services of S have to be preserved by S'. We relate our substitutability criteria to preorders and equivalences known from process theory. The second contribution of this thesis is to present, for each substitutability criterion, a procedure to decide whether a service S' can substitute a service S. The decision requires the comparison of the in general infinite sets of behaviorally compatible services for the services S and S'. Hence, we extend existing work on an abstract representation of all behaviorally compatible services for a given service. For each notion of behavioral compatibility, we present an algorithmic solution to represent all behaviorally compatible services. Based on these representations, we can decide substitutability of a service S by a service S'. The third contribution of this thesis is a method to support the design of a service S' that can substitute a service $S$ according to a substitutability criterion. Our approach is to derive a service S' from the service S by stepwise transformation. To this end, we present several transformation rules. Finally, we formalize and we extend the equivalence notion for services specified in the language WS-BPEL. That way, we demonstrate the applicability of our work.
close
close
• ### Konferenzbeiträge auf Workshops

• Parnjai, Jarungjit, Stahl, Christian, Wolf, Karsten
A finite representation of all substitutable services and its applications
Oliver Kopp and Niels Lohmann, editors
In Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, mar 2009
We present a finite representation of all substitutable services P' of a given service P. We show that our approach can be used for at least two applications: (1) given a finite set of services \mathcalP = P1, ..., Pn, we provide a representation of all services P' that can substitute every Pi \in \mathcalP, and (2) given a service P'' that cannot substitute a service P, we find the most similar service P* to P'' that can substitute P.
close
close
• Aalst, Wil M. P. van der, Mooij, Arjan J., Stahl, Christian, Wolf, Karsten
Service Interaction: Patterns, Formalization, and Analysis
Marco Bernardo and Luca Padovani and Gianluigi Zavattaro, editors
In Formal Methods for Web Services (SFM 2009), volume 5569 of Springer-Verlag, apr 2009
As systems become more service oriented and processes increasingly cross organizational boundaries, interaction becomes more important. New technologies support the development of such systems. However, the paradigm shift towards service orientation, requires a fundamentally different way of looking at processes. This survey aims to provide some foundational notions related to service interaction. A set of service interaction patterns is given to illustrate the challenges in this domain. Moreover, key results are given for three of these challenges: (1) How to expose a service?, (2) How to replace and refine services?, and (3) How to generate service adapters? These challenges will be addressed in a Petri net setting. However, the results extend to other languages used in this domain.
close
close
• Liske, Nannette, Lohmann, Niels, Stahl, Christian, Wolf, Karsten
Another Approach to Service Instance Migration
Luciano Baresi and Chi-Hung Chi and Jun Suzuki, editors
In Service-Oriented Computing - ICSOC 2009, 7th International Conference, Stockholm, Sweden, November 24-27, 2009. Proceedings, Lecture Notes in Computer Science, Springer-Verlag, nov 2009
Services change over time, be it for internal improvements, be it for external requirements such as new legal regulations. For long running services, it may even be necessary to change a service while instances are actually running and interacting with other services. This problem is referred to as instance migration. We present a novel approach to the behavioral (service protocol) aspects of instance migration. We apply techniques for finitely characterizing the set of all correctly interacting partners to a given service. The approach assures that migration does not introduce behavioral problems with any running partner of the original service. Our technique scales up to services with thousands of states, including models of real WS-BPEL processes.
close
close
• König, Dieter, Lohmann, Niels, Moser, Simon, Stahl, Christian, Wolf, Karsten
Extending the Compatibility Notion for Abstract WS-BPEL Processes
Wei-Ying Ma and Andrew Tomkins and Xiaodong Zhang, editors
In Proceedings of the 17th International Conference on World Wide Web, WWW 2008, Beijing, China, April 21--25, 2008, apr 2008
WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.
close
close
• Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
From Public Views to Private Views -- Correctness-by-Design for Services
Marlon Dumas and Reiko Heckel, editors
In Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, Springer-Verlag, 2008
Service orientation is a means for integrating across diverse systems. Each resource, whether an application, system, or trading partner, can be accessed as a service. The resulting architecture, often referred to as SOA, has been an important enabler for interorganizational processes. Apart from technological issues that need to be addressed, it is important that all parties involved in such processes agree on the "rules of engagement". Therefore, we propose to use a contract that specifies the composition of the public views of all participating parties. Each party may then implement its part of the contract such that the implementation (i.e., the private view) accords with the contract. In this paper, we define a suitable notion of accordance inspired by the asynchronous nature of services. Moreover, we present several transformation rules for incrementally building a private view such that accordance with the contract is guaranteed by construction. These rules include adding internal tasks as well as the reordering of messages and are therefore much more powerful than existing correctness-preserving construction rules.
close
close
• Reisig, Wolfgang, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela, Wolf, Karsten, Kaschner, Kathrin
Analysis Techniques for Service Models
In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, IEEE Computer Society, nov 2006
The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
volume 53 of The Computer Journal 53 (1), 2010
To implement an interorganizational process between different enterprizes, one needs to agree on the rules of engagement''. These can be specified in terms of a contract that describes the overall intended process and the duties of all parties involved. We propose to use such a process-oriented contract which can be seen as the composition of the public views of all participating parties. Based on this contract each party may locally implement its part of the contract such that the implementation (the private view) agrees on the contract. In this paper, we propose a formal notion for such process-oriented contracts and give a criterion for accordance between a private view and its public view. The public view of a party can be substituted by a private view if and only if the private view accords with the public view. Using the notion of accordance the overall implemented process is guaranteed to be deadlock-free and it is always possible to terminate properly. In addition, we present a technique for automatically checking our accordance criterion. A case study illustrates how our proposed approach can be used in practice.
close
close
• Mooij, Arjan J., Stahl, Christian, Voorhoeve, Marc
Relating Fair Testing and Accordance for Service Replaceability
Journal of Logic and Algebraic Programming, 2010
The accordance pre-order describes whether a service can safely be replaced by another service. That is, all partners for the original service should be partners for the new service. Partners for a service interact with the service in such a way that always a certain common goal can be reached. We relate the accordance pre-order to the pre-orders known from the linear-branching time spectrum, notably fair testing. The differences between accordance and fair testing include the modeling of termination and success, and the parts of the services that cannot be used reliably by any partner. Apart from the theoretical results, we address the practical relevance of the introduced concepts.
close
close
• Stahl, Christian, Wolf, Karsten
Deciding Service Composition and Substitutability Using Extended Operating Guidelines
volume 68 of Data Knowl. Eng. 68 (9), 2009
We study the correct interaction between services using the following notion for correctness: there is no deadlock in the interaction of the services, and a given set of activities is not dead, that is, each activity in this set is executed in at least one run. The second condition has not been studied before. An operating guideline of a service P is an operational characterization of all deadlock-free interacting partners of P. In this paper, we present an extension of the concept of an operating guideline to characterize all correctly interacting partners of a service P. This extension can be used for answering at least the following two questions. First, given a service R, does R interact correctly with P? Second, given a service P', can P be substituted by P', that is, is every correctly interacting partner of P a correctly interacting partner of P', too?
close
close

• Deciding Substitutability of Services with Operating Guidelines
Kurt Jensen and Wil M. P. van der Aalst, editors
volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2 (5460), Springer-Verlag, mar 2009
Deciding whether a service S can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of restriction can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
close
close
• ### Technische Berichte

• Deciding Substitutability of Services with Operating Guidelines
Informatik-Berichte, Humboldt-Universität zu Berlin, apr 2008
Deciding whether a service $S$ can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of deprecation can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
close
close
• König, Dieter, Lohmann, Niels, Moser, Simon, Stahl, Christian, Wolf, Karsten
Extending the Compatibility Notion for Abstract WS-BPEL Processes
Preprint, Universität Rostock, Rostock, Germany, nov 2007
WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.
close
close
• Aalst, Wil M. P. van der, Massuthe, Peter, Mooij, Arjan J., Stahl, Christian, Wolf, Karsten
Erratum -- Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
Informatik-Berichte, Humboldt-Universität zu Berlin, jun 2007
close
• Aalst, Wil M. P. van der, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
Informatik-Berichte, Humboldt-Universität zu Berlin, jun 2007
A contract specifies an interorganizational process together with a distribution of responsibilities for the activities among the parties involved. In this paper, we formally show how a party can implement its part of the contract such that the implementation accords with the contract. We propose a formal notion of a contract and give a criterion for accordance between a local implementation and a contract such that, if all local implementations accord with the contract, the overall process is deadlock-free and it is always possible to terminate properly. Then, we sketch a technique for automatically checking the proposed accordance criterion. Finally, we present accordance-preserving transformation rules. These rules can be used to implement a part of the contract while preserving the accordance criterion.
close
close

## Gals

### Konferenzbeiträge auf Workshops

• Grass, Eckhard, Winkler, Frank, Krstic, Milos, Julius, Alexandra, Stahl, Christian, Piz, Maxim
Enhanced GALS Techniques for Datapath Applications
Vassilis Paliouras and Johan Vounckx and Diederik Verkest, editors
In Integrated Circuit and System Design: 15th International Workshop, PATMOS 2005, Leuven, Belgium, September 20-23, 2005, volume 3728 of Lecture Notes in Computer Science, Springer-Verlag, aug 2005
Based on a previously reported request driven technique for Globally-Asynchronous Locally-Synchronous (GALS) circuits this paper presents two significant enhancements. Firstly, the previously required local ring oscillators are avoided. Instead, an external clock with arbitrary phase for each GALS block is used. Details of the required wrapper circuitry, the proposed design flow and performance are provided. Secondly, to reduce supply noise, a novel approach applying individual clock jitter for GALS blocks is proposed. A simulation using the jitter technique shows that for a typical GALS system, the power spectrum of the supply current can be reduced by about 15 dB.
close
close
• Stahl, Christian, Reisig, Wolfgang, Krstic, Milos
Hazard Detection in a GALS Wrapper: A Case Study
, editors
In Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD'05), IEEE Computer Society, St. Malo, France, jun 2005
An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion two techniques to reduce the model's state space are presented. By use of these techniques we detected several potential hazards and a deadlock in the wrapper.
close
close
• Krstic, Milos, Grass, Eckhard, Stahl, Christian
Request-Driven GALS Technique for Wireless Communication System
In Proceedings of the 11th International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 2005), IEEE Computer Society, New York, NY, USA, mar 2005
A Globally Asynchronous - Locally Synchronous (GALS) technique for application in wireless communication systems is proposed and evaluated. The GALS wrappers are based on a request-driven operation with an embedded time-out function. A formally verified GALS wrapper is deployed for the ?GALSification? of a baseband processor for WLAN. Details of the GALS partitioning, implementation and the design-flow are discussed. Furthermore, a test strategy based on built-in self-test (BIST) is suggested. The described baseband processor was fabricated and successfully tested. The GALS design is compared with a clock-gated, synchronous version. Advantages for system integration are achieved along with a 1% reduction in dynamic power consumption, a 30% reduction in peak power supply current, and 5 dB reduction in spectral noise.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Krsti\'c, Milo\vs, Grass, Eckhard, Stahl, Christian, Piz, Maxim
System Integration by Request-driven GALS Design
volume 153 of IEE Proc. Computers \& Digital Techniques 153 (5), September 2006
A novel request-driven globally asynchronous locally synchronous (GALS) technique for the system integration of complex digital blocks is proposed. For this new GALS technique, an asynchronous wrapper compliant is developed and evaluated. This proposed GALS technique is applied to a baseband processor compatible with the wireless LAN standard IEEE 802.11a. The developed GALS baseband processor chip is fabricated and measured. Besides improvements of the system integration process, a 5 dB reduction in electromagnetic interference, 30\% reduction in instantaneous supply current variation, and similar dynamic power consumption as in the synchronous baseband processor is achieved.
close
close
• ### Studien- und Diplomarbeiten

• Julius, Alexandra

Diplomarbeit, may 2007
close
close
• Bretschneider, Jan
Modellierung und Synthese eines geschwindigkeitsinvarianten GALS-Wrappers
Studienarbeit, feb 2006
close
close
• Julius, Alexandra
Entwurf und VHDL-Modellierung von mesochronen GALS-Schaltungen
Studienarbeit, dec 2005
close
close
• ### Technische Berichte

• Stahl, Christian, Reisig, Wolfgang, Krstic, Milos
Hazard Detection in a GALS Wrapper: a Case study
Informatik-Berichte, , feb 2005
An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion three techniques to reduce the model?s state space are presented. By use of these techniques we detected several potential hazards in the wrapper.
close
close

## Interaktionsgraph

### Studien- und Diplomarbeiten

• Strukturelle Analyse von offenen Workflow-Netzen hinsichtlich Bedienbarkeit
Studienarbeit, jan 2007
close

## Lola

### Konferenzbeiträge auf Workshops

• Stahl, Christian, Reisig, Wolfgang, Krstic, Milos
Hazard Detection in a GALS Wrapper: A Case Study
, editors
In Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD'05), IEEE Computer Society, St. Malo, France, jun 2005
An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion two techniques to reduce the model's state space are presented. By use of these techniques we detected several potential hazards and a deadlock in the wrapper.
close
close
• ### Technische Berichte

• Fahland, Dirk
Translating UML2 Activity Diagrams Petri Nets for analyzing IBM WebSphere Business Modeler process models
Informatik-Berichte, Humboldt-Universität zu Berlin, 2008
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/.
close
close
• Stahl, Christian, Reisig, Wolfgang, Krstic, Milos
Hazard Detection in a GALS Wrapper: a Case study
Informatik-Berichte, , feb 2005
An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion three techniques to reduce the model?s state space are presented. By use of these techniques we detected several potential hazards in the wrapper.
close
close

## Matching

### Konferenzbeiträge auf Workshops

• Wolf, Karsten, Stahl, Christian, Ott, Janine, Danitz, Robert
Verifying Livelock Freedom in an SOA Scenario
Stephen Edwards and Walter Vogler, editors
In Proceedings of the Ninth International Conference on Application of Concurrency to System Design (ACSD'09), IEEE Computer Society, Augsburg, Germany, jul 2009
In a service-oriented architecture (SOA), a service broker assigns a previously published service (stored in a service registry) to a service requester. It is desirable for the composition of the requesting and the assigned service to interact properly. While proper interaction is often reduced to deadlock freedom of the composed system, we additionally consider livelock freedom as a desirable property for the interaction of services. In principle, deadlock- and livelock freedom can be verified by inspecting the state space of the composition of (public views of) the involved services. The contribution of this paper is to propose a methodology to build that state space from pre-computed fragments which are computed upon publishing a service. That way, we shift computation time from the time critical request phase of service brokerage to the less critical publish phase. Interestingly, our setting enables state space reduction methods that are intrinsically different from traditional state space reductions.
close
close
• Aalst, Wil M. P. van der, Mooij, Arjan J., Stahl, Christian, Wolf, Karsten
Service Interaction: Patterns, Formalization, and Analysis
Marco Bernardo and Luca Padovani and Gianluigi Zavattaro, editors
In Formal Methods for Web Services (SFM 2009), volume 5569 of Springer-Verlag, apr 2009
As systems become more service oriented and processes increasingly cross organizational boundaries, interaction becomes more important. New technologies support the development of such systems. However, the paradigm shift towards service orientation, requires a fundamentally different way of looking at processes. This survey aims to provide some foundational notions related to service interaction. A set of service interaction patterns is given to illustrate the challenges in this domain. Moreover, key results are given for three of these challenges: (1) How to expose a service?, (2) How to replace and refine services?, and (3) How to generate service adapters? These challenges will be addressed in a Petri net setting. However, the results extend to other languages used in this domain.
close
close
• Stahl, Christian, Wolf, Karsten
Covering Places and Transitions in Open Nets
Marlon Dumas and Manfred Reichert, editors
In Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, Springer-Verlag, sep 2008
We present a finite representation of all services M where the composition with a given service N is deadlock-free, and a given set of activities of N can be covered (i.e. is not dead). Our representation is an extension of the existing notion of an operating guideline which only cared about deadlock freedom. We further present an algorithm to decide whether a service M matches with the extended operating guideline of N.
close
close

• Analyzing Interacting BPEL Processes
In Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings, volume 4102 of Lecture Notes in Computer Science, Springer-Verlag, sep 2006
This paper addresses the problem of analyzing theinteraction between BPEL processes. We present a technology chain that starts out with a BPEL process and transforms it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). A case study demonstrates the value of this technology chain.
close
close
• Kaschner, Kathrin, Massuthe, Peter, Wolf, Karsten

Daniel Moldt, editors
In , , sep 2006
close
• Massuthe, Peter, Wolf, Karsten
An Algorithm for Matching Nondeterministic Services with Operating Guidelines
Frank Leymann and Wolfgang Reisig and Satish R. Thatte and Wil M. P. van der Aalst, editors
In The Role of Business Processes in Service Oriented Architectures, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2006
Interorganizational cooperation is more and more organized by the paradigm of services. Service-oriented architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester, and the service broker, together with the three operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artifact to realize the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free communication. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Stahl, Christian, Wolf, Karsten
Deciding Service Composition and Substitutability Using Extended Operating Guidelines
volume 68 of Data Knowl. Eng. 68 (9), 2009
We study the correct interaction between services using the following notion for correctness: there is no deadlock in the interaction of the services, and a given set of activities is not dead, that is, each activity in this set is executed in at least one run. The second condition has not been studied before. An operating guideline of a service P is an operational characterization of all deadlock-free interacting partners of P. In this paper, we present an extension of the concept of an operating guideline to characterize all correctly interacting partners of a service P. This extension can be used for answering at least the following two questions. First, given a service R, does R interact correctly with P? Second, given a service P', can P be substituted by P', that is, is every correctly interacting partner of P a correctly interacting partner of P', too?
close
close

• Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation
volume 64 of Data Knowl. Eng. 64 (1), jan 2008
We address the problem of analyzing the interaction between WS-BPEL processes. We present a technology chain that starts out with a WS-BPEL process and translates it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). To manage processes of realistic size, we present a concept of a \emphflexible model generation which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.
close
close
• Massuthe, Peter, Wolf, Karsten
An Algorithm for Matching Non-deterministic Services with Operating Guidelines
volume 2 of International Journal of Business Process Integration and Management (IJBPIM) 2 (2), 2007
Interorganisational cooperation is more and more organised by the paradigm of services. Service-Oriented Architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester and the service broker, together with the three operations publish, find and bind. We provide a formal method based on non-deterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artefact to realise the publish operation. In our approach, the find operation reduces to a matching problem between the requesters service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free interaction. In this paper, matching of deterministic as well as non-deterministic automata with operating guidelines is presented.
close
close
• ### Technische Berichte

• Massuthe, Peter, Wolf, Karsten
An Algorithm for Matching Nondeterministic Services with Operating Guidelines
Informatik-Berichte, , 2006
Interorganizational cooperation is more and more organizedby the paradigm of services. Service-oriented architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester, and the service broker, together with the three operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artifact to realize the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlockfree communication. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.
close
close
• Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
Operating Guidelines for Finite-State Services
Informatik-Berichte, , dec 2006
We introduce the concept of an operating guideline for an arbitrary finite-state service P, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to correctly (in this paper: deadlock-free) communicate with P. It can further be executed or used for service discovery. An operating guideline for P is a particular service S that is enriched with annotations. S communicates deadlock-free with P and is able to simulate every other service that communicates deadlock-free with P. The attached annotations give complete information about whether or not a simulated service is deadlock-free, too.
close
close
• Massuthe, Peter, Schmidt, Karsten
Matching Nondeterministic Services with Operating Guidelines
Informatik-Berichte, , jun 2005
Abstract Interorganizational cooperation is more and more organizedby the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester?s service and operating guidelines. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.
close
close

## Offene Workflownetze

### Dissertationen und Habilitationen

• Stahl, Christian
Service Substitution - A Behavioral Approach Based on Petri Nets
Dissertation, Dec 2009
Service-Oriented Computing is an emerging computing paradigm that supports the modular design of (software) systems. Complex systems are designed by composing less complex systems, called services. Such a (complex) system is a distributed application often involving several cooperating enterprises. As a system usually changes over time, individual services will be substituted by other services. Substituting one service by another one should not affect the correctness of the overall system. Assuring correctness becomes particularly challenging, as the services rely on each other, and each of the involved enterprises only oversees a part of the overall system. In addition, services communicate asynchronously which makes the analysis even more difficult. For this reason, formal methods to support service substitution are indispensable. In this thesis, we study service substitution at the level of service models. Thereby we restrict ourselves to service behavior. As a formalism to model service behavior, we use Petri nets. The first contribution of this thesis is the definition of several substitutability criteria that are suitable in the context of Service-Oriented Computing. Substituting a service S by a service S' should preserve some behavioral properties of the overall system. For each set of behavioral properties and a given service S, there exists a set of behaviorally compatible services for S. A substitutability criterion defines which of these behaviorally compatible services of S have to be preserved by S'. We relate our substitutability criteria to preorders and equivalences known from process theory. The second contribution of this thesis is to present, for each substitutability criterion, a procedure to decide whether a service S' can substitute a service S. The decision requires the comparison of the in general infinite sets of behaviorally compatible services for the services S and S'. Hence, we extend existing work on an abstract representation of all behaviorally compatible services for a given service. For each notion of behavioral compatibility, we present an algorithmic solution to represent all behaviorally compatible services. Based on these representations, we can decide substitutability of a service S by a service S'. The third contribution of this thesis is a method to support the design of a service S' that can substitute a service $S$ according to a substitutability criterion. Our approach is to derive a service S' from the service S by stepwise transformation. To this end, we present several transformation rules. Finally, we formalize and we extend the equivalence notion for services specified in the language WS-BPEL. That way, we demonstrate the applicability of our work.
close
close
• ### Konferenzbeiträge auf Workshops

• Stahl, Christian, Wolf, Karsten
Covering Places and Transitions in Open Nets
Marlon Dumas and Manfred Reichert, editors
In Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, Springer-Verlag, sep 2008
We present a finite representation of all services M where the composition with a given service N is deadlock-free, and a given set of activities of N can be covered (i.e. is not dead). Our representation is an extension of the existing notion of an operating guideline which only cared about deadlock freedom. We further present an algorithm to decide whether a service M matches with the extended operating guideline of N.
close
close
• Reisig, Wolfgang, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela, Wolf, Karsten, Kaschner, Kathrin
Analysis Techniques for Service Models
In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, IEEE Computer Society, nov 2006
The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
volume 53 of The Computer Journal 53 (1), 2010
To implement an interorganizational process between different enterprizes, one needs to agree on the rules of engagement''. These can be specified in terms of a contract that describes the overall intended process and the duties of all parties involved. We propose to use such a process-oriented contract which can be seen as the composition of the public views of all participating parties. Based on this contract each party may locally implement its part of the contract such that the implementation (the private view) agrees on the contract. In this paper, we propose a formal notion for such process-oriented contracts and give a criterion for accordance between a private view and its public view. The public view of a party can be substituted by a private view if and only if the private view accords with the public view. Using the notion of accordance the overall implemented process is guaranteed to be deadlock-free and it is always possible to terminate properly. In addition, we present a technique for automatically checking our accordance criterion. A case study illustrates how our proposed approach can be used in practice.
close
close
• Stahl, Christian, Wolf, Karsten
Deciding Service Composition and Substitutability Using Extended Operating Guidelines
volume 68 of Data Knowl. Eng. 68 (9), 2009
We study the correct interaction between services using the following notion for correctness: there is no deadlock in the interaction of the services, and a given set of activities is not dead, that is, each activity in this set is executed in at least one run. The second condition has not been studied before. An operating guideline of a service P is an operational characterization of all deadlock-free interacting partners of P. In this paper, we present an extension of the concept of an operating guideline to characterize all correctly interacting partners of a service P. This extension can be used for answering at least the following two questions. First, given a service R, does R interact correctly with P? Second, given a service P', can P be substituted by P', that is, is every correctly interacting partner of P a correctly interacting partner of P', too?
close
close

## Open Workflow Nets

### Konferenzbeiträge auf Workshops

• Aalst, Wil M. P. van der, Mooij, Arjan J., Stahl, Christian, Wolf, Karsten
Service Interaction: Patterns, Formalization, and Analysis
Marco Bernardo and Luca Padovani and Gianluigi Zavattaro, editors
In Formal Methods for Web Services (SFM 2009), volume 5569 of Springer-Verlag, apr 2009
As systems become more service oriented and processes increasingly cross organizational boundaries, interaction becomes more important. New technologies support the development of such systems. However, the paradigm shift towards service orientation, requires a fundamentally different way of looking at processes. This survey aims to provide some foundational notions related to service interaction. A set of service interaction patterns is given to illustrate the challenges in this domain. Moreover, key results are given for three of these challenges: (1) How to expose a service?, (2) How to replace and refine services?, and (3) How to generate service adapters? These challenges will be addressed in a Petri net setting. However, the results extend to other languages used in this domain.
close
close

## Operating Guidelines

### Konferenzbeiträge auf Workshops

• Parnjai, Jarungjit, Stahl, Christian, Wolf, Karsten
A finite representation of all substitutable services and its applications
Oliver Kopp and Niels Lohmann, editors
In Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, mar 2009
We present a finite representation of all substitutable services P' of a given service P. We show that our approach can be used for at least two applications: (1) given a finite set of services \mathcalP = P1, ..., Pn, we provide a representation of all services P' that can substitute every Pi \in \mathcalP, and (2) given a service P'' that cannot substitute a service P, we find the most similar service P* to P'' that can substitute P.
close
close
• Wolf, Karsten, Stahl, Christian, Ott, Janine, Danitz, Robert
Verifying Livelock Freedom in an SOA Scenario
Stephen Edwards and Walter Vogler, editors
In Proceedings of the Ninth International Conference on Application of Concurrency to System Design (ACSD'09), IEEE Computer Society, Augsburg, Germany, jul 2009
In a service-oriented architecture (SOA), a service broker assigns a previously published service (stored in a service registry) to a service requester. It is desirable for the composition of the requesting and the assigned service to interact properly. While proper interaction is often reduced to deadlock freedom of the composed system, we additionally consider livelock freedom as a desirable property for the interaction of services. In principle, deadlock- and livelock freedom can be verified by inspecting the state space of the composition of (public views of) the involved services. The contribution of this paper is to propose a methodology to build that state space from pre-computed fragments which are computed upon publishing a service. That way, we shift computation time from the time critical request phase of service brokerage to the less critical publish phase. Interestingly, our setting enables state space reduction methods that are intrinsically different from traditional state space reductions.
close
close
• Aalst, Wil M. P. van der, Mooij, Arjan J., Stahl, Christian, Wolf, Karsten
Service Interaction: Patterns, Formalization, and Analysis
Marco Bernardo and Luca Padovani and Gianluigi Zavattaro, editors
In Formal Methods for Web Services (SFM 2009), volume 5569 of Springer-Verlag, apr 2009
As systems become more service oriented and processes increasingly cross organizational boundaries, interaction becomes more important. New technologies support the development of such systems. However, the paradigm shift towards service orientation, requires a fundamentally different way of looking at processes. This survey aims to provide some foundational notions related to service interaction. A set of service interaction patterns is given to illustrate the challenges in this domain. Moreover, key results are given for three of these challenges: (1) How to expose a service?, (2) How to replace and refine services?, and (3) How to generate service adapters? These challenges will be addressed in a Petri net setting. However, the results extend to other languages used in this domain.
close
close
• König, Dieter, Lohmann, Niels, Moser, Simon, Stahl, Christian, Wolf, Karsten
Extending the Compatibility Notion for Abstract WS-BPEL Processes
Wei-Ying Ma and Andrew Tomkins and Xiaodong Zhang, editors
In Proceedings of the 17th International Conference on World Wide Web, WWW 2008, Beijing, China, April 21--25, 2008, apr 2008
WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.
close
close
• Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
From Public Views to Private Views -- Correctness-by-Design for Services
Marlon Dumas and Reiko Heckel, editors
In Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, Springer-Verlag, 2008
Service orientation is a means for integrating across diverse systems. Each resource, whether an application, system, or trading partner, can be accessed as a service. The resulting architecture, often referred to as SOA, has been an important enabler for interorganizational processes. Apart from technological issues that need to be addressed, it is important that all parties involved in such processes agree on the "rules of engagement". Therefore, we propose to use a contract that specifies the composition of the public views of all participating parties. Each party may then implement its part of the contract such that the implementation (i.e., the private view) accords with the contract. In this paper, we define a suitable notion of accordance inspired by the asynchronous nature of services. Moreover, we present several transformation rules for incrementally building a private view such that accordance with the contract is guaranteed by construction. These rules include adding internal tasks as well as the reordering of messages and are therefore much more powerful than existing correctness-preserving construction rules.
close
close

• Analyzing Interacting BPEL Processes
In Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings, volume 4102 of Lecture Notes in Computer Science, Springer-Verlag, sep 2006
This paper addresses the problem of analyzing theinteraction between BPEL processes. We present a technology chain that starts out with a BPEL process and transforms it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). A case study demonstrates the value of this technology chain.
close
close
• Massuthe, Peter, Wolf, Karsten
An Algorithm for Matching Nondeterministic Services with Operating Guidelines
Frank Leymann and Wolfgang Reisig and Satish R. Thatte and Wil M. P. van der Aalst, editors
In The Role of Business Processes in Service Oriented Architectures, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2006
Interorganizational cooperation is more and more organized by the paradigm of services. Service-oriented architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester, and the service broker, together with the three operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artifact to realize the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free communication. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.
close
close
• Kaschner, Kathrin, Massuthe, Peter, Wolf, Karsten

Daniel Moldt, editors
In , , sep 2006
close
• Massuthe, Peter, Schmidt, Karsten
Operating Guidelines - an Automata-Theoretic Foundation for the Service-Oriented Architecture
Kai-Yuan Cai and Atsushi Ohnishi and M.F. Lau, editors
In Proceedings of the Fifth International Conference on Quality Software (QSIC 2005), IEEE Computer Society, Melbourne, Australia, sep 2005
In the service-oriented architecture (SOA), we distinguish three roles of service owners: service providers, service requesters, and service brokers. Each service provider publishes information to the broker about how requesters can interact with its service. Thus, the broker can assign a fitting service provider to a querying requester. We propose the information published to the broker to be operating guidelines. Operating guidelines are essentially communication instructions for the service requester. We present an automata-theoretic approach that is centered around operating guidelines and is capable of implementing all tasks arising in the SOA.
close
close
• Massuthe, Peter, Schmidt, Karsten
Operating Guidelines for Services
Karsten Schmidt and Christian Stahl, editors
In , , sep 2005
In the service-oriented architecture (SOA), we distinguish three roles of service owners:service providers, service requesters, and service brokers, and the three standard operations publish, find, and bind. We provide a formal method based on Petri nets to model services. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation
volume 64 of Data Knowl. Eng. 64 (1), jan 2008
We address the problem of analyzing the interaction between WS-BPEL processes. We present a technology chain that starts out with a WS-BPEL process and translates it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). To manage processes of realistic size, we present a concept of a \emphflexible model generation which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.
close
close
• Massuthe, Peter, Wolf, Karsten
An Algorithm for Matching Non-deterministic Services with Operating Guidelines
volume 2 of International Journal of Business Process Integration and Management (IJBPIM) 2 (2), 2007
Interorganisational cooperation is more and more organised by the paradigm of services. Service-Oriented Architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester and the service broker, together with the three operations publish, find and bind. We provide a formal method based on non-deterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artefact to realise the publish operation. In our approach, the find operation reduces to a matching problem between the requesters service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free interaction. In this paper, matching of deterministic as well as non-deterministic automata with operating guidelines is presented.
close
close
• Kaschner, Kathrin, Massuthe, Peter, Wolf, Karsten
Symbolic Representation of Operating Guidelines for Services
volume 72 of Petri Net Newsletter 72, apr 2007
close
• Massuthe, Peter, Wolf, Karsten
Operating Guidelines for Services
volume 70 of Petri Net Newsletter 70, apr 2006
In the service-oriented architecture (SOA), we distinguish three roles of service owners: service providers, service requesters, and service brokers, and the three standard operations publish, find, and bind. We provide a formal method based on Petri nets to model services. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester's service and the operating guideline.
close
close
• Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
An Operating Guideline Approach to the SOA
volume 1 of Annals of Mathematics, Computing \& Teleinformatics 1 (3), 2005
Interorganizational cooperation is more andmore organized by the paradigm of services. The serviceoriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester's and provider's services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester's service and the operating guideline. Binding of a requester's and a provider's service is therefore guaranteed to result in a well-behaving cooperating service. At this time, the approach is limited to acyclic Petri nets.
close
close
• ### Studien- und Diplomarbeiten

• Bretschneider, Jan
Produktbedienungsanleitungen zur Charakterisierung austauschbarer Services
Diplomarbeit, mar 2007
close
close
• Laufer, Peter
Public-View-Generierung
Diplomarbeit, nov 2007
close
close
• ### Technische Berichte

• Aalst, Wil M. P. van der, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
Informatik-Berichte, Humboldt-Universität zu Berlin, jun 2007
A contract specifies an interorganizational process together with a distribution of responsibilities for the activities among the parties involved. In this paper, we formally show how a party can implement its part of the contract such that the implementation accords with the contract. We propose a formal notion of a contract and give a criterion for accordance between a local implementation and a contract such that, if all local implementations accord with the contract, the overall process is deadlock-free and it is always possible to terminate properly. Then, we sketch a technique for automatically checking the proposed accordance criterion. Finally, we present accordance-preserving transformation rules. These rules can be used to implement a part of the contract while preserving the accordance criterion.
close
close
• Aalst, Wil M. P. van der, Massuthe, Peter, Mooij, Arjan J., Stahl, Christian, Wolf, Karsten
Erratum -- Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
Informatik-Berichte, Humboldt-Universität zu Berlin, jun 2007
close
• Massuthe, Peter, Wolf, Karsten
An Algorithm for Matching Nondeterministic Services with Operating Guidelines
Informatik-Berichte, , 2006
Interorganizational cooperation is more and more organizedby the paradigm of services. Service-oriented architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester, and the service broker, together with the three operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artifact to realize the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlockfree communication. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.
close
close
• Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
Operating Guidelines for Finite-State Services
Informatik-Berichte, , dec 2006
We introduce the concept of an operating guideline for an arbitrary finite-state service P, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to correctly (in this paper: deadlock-free) communicate with P. It can further be executed or used for service discovery. An operating guideline for P is a particular service S that is enriched with annotations. S communicates deadlock-free with P and is able to simulate every other service that communicates deadlock-free with P. The attached annotations give complete information about whether or not a simulated service is deadlock-free, too.
close
close
• Massuthe, Peter, Schmidt, Karsten
Operating Guidelines - an Alternative to Public View
Informatik-Berichte, , 2005
We propose operating guidelines as artifacts for publishing information about how to communicate with a business process that is intended to be provided as a service. We present an approach to compute operating guidelines fully automatically. We compare operating guidelines with the concept of public view.
close
close
• Massuthe, Peter, Schmidt, Karsten
Matching Nondeterministic Services with Operating Guidelines
Informatik-Berichte, , jun 2005
Abstract Interorganizational cooperation is more and more organizedby the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester?s service and operating guidelines. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.
close
close
• Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
An Operating Guideline Approach to the SOA
Informatik-Berichte, , 2005
Interorganizational cooperation is more and more organized by the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester?s and provider?s services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline. Binding of a requester?s and a provider?s service is therefore guaranteed to result in a well-behaving cooperating service.
close
close

## Owfn

### Studien- und Diplomarbeiten

• Liske, Nanette
Laufzeitersetzung offener Workflownetze
Diplomarbeit, jul 2008
close

## Owfns

### Konferenzbeiträge auf Workshops

• Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
From Public Views to Private Views -- Correctness-by-Design for Services
Marlon Dumas and Reiko Heckel, editors
In Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, Springer-Verlag, 2008
Service orientation is a means for integrating across diverse systems. Each resource, whether an application, system, or trading partner, can be accessed as a service. The resulting architecture, often referred to as SOA, has been an important enabler for interorganizational processes. Apart from technological issues that need to be addressed, it is important that all parties involved in such processes agree on the "rules of engagement". Therefore, we propose to use a contract that specifies the composition of the public views of all participating parties. Each party may then implement its part of the contract such that the implementation (i.e., the private view) accords with the contract. In this paper, we define a suitable notion of accordance inspired by the asynchronous nature of services. Moreover, we present several transformation rules for incrementally building a private view such that accordance with the contract is guaranteed by construction. These rules include adding internal tasks as well as the reordering of messages and are therefore much more powerful than existing correctness-preserving construction rules.
close
close
• Lohmann, Niels
A Feature-Complete Petri Net Semantics for WS-BPEL 2.0
Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, jun 2007
We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.
close
close
• Fahland, Dirk
A Formal Approach to Adaptive Processes using Scenario-based Concepts.
Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, Siedlce, Poland, jun 2007
close
close
• Weinberg, Daniela, Schmidt, Karsten
Reduction Rules for Interaction Graphs
Karsten Schmidt and Christian Stahl, editors
In , , sep 2005
The internet today has grown to be more than just being a basisfor exchanging information. It steadily becomes a platform for processing business processes. Many companies distribute their service with the help of web services or integrate other web services into their own workflow. However, before a web service gets published it should be examined well. We will introduce a way of examining the controllability of a web service. We propose the interaction graph of a web service, that is modelled by an open workflow net. To verify whether such a net is controllable or not it is sufficient to construct a reduced interaction graph. We will define reduction rules that minimize the size of the graph greatly. The analysis using the interaction graph as well as the reduction rules are implemented and have been integrated into an analysis tool kit for web services.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Massuthe, Peter, Serebrenik, Alexander, Sidorova, Natalia, Wolf, Karsten
Can I find a Partner? Undecidablity of Partner Existence for Open Nets
volume 108 of Information Processing Letters 108 (6), Nov 2008
close
• Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian
Kommunizierende Workflow-Services modellieren und analysieren
Informatik - Forschung und Entwicklung, Springer-Verlag, oct 2005
close
close
• Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
An Operating Guideline Approach to the SOA
volume 1 of Annals of Mathematics, Computing \& Teleinformatics 1 (3), 2005
Interorganizational cooperation is more andmore organized by the paradigm of services. The serviceoriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester's and provider's services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester's service and the operating guideline. Binding of a requester's and a provider's service is therefore guaranteed to result in a well-behaving cooperating service. At this time, the approach is limited to acyclic Petri nets.
close
close
• ### Studien- und Diplomarbeiten

• Synthese offener Workflownetze aus Serviceautomaten
Diplomarbeit, jan 2008
close
close

• Strukturelle Analyse von offenen Workflow-Netzen hinsichtlich Bedienbarkeit
Studienarbeit, jan 2007
close
• Schulz, Alexander
Zielgerichtete Strategien
Studienarbeit, jul 2007
close
• Gierds, Christian

Studienarbeit, oct 2007
close
close
• ### Technische Berichte

• Aalst, Wil M. P. van der, Massuthe, Peter, Mooij, Arjan J., Stahl, Christian, Wolf, Karsten
Erratum -- Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
Informatik-Berichte, Humboldt-Universität zu Berlin, jun 2007
close
• Aalst, Wil M. P. van der, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
Informatik-Berichte, Humboldt-Universität zu Berlin, jun 2007
A contract specifies an interorganizational process together with a distribution of responsibilities for the activities among the parties involved. In this paper, we formally show how a party can implement its part of the contract such that the implementation accords with the contract. We propose a formal notion of a contract and give a criterion for accordance between a local implementation and a contract such that, if all local implementations accord with the contract, the overall process is deadlock-free and it is always possible to terminate properly. Then, we sketch a technique for automatically checking the proposed accordance criterion. Finally, we present accordance-preserving transformation rules. These rules can be used to implement a part of the contract while preserving the accordance criterion.
close
close
• Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian

Informatik-Berichte, , feb 2005
close
close
• Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
An Operating Guideline Approach to the SOA
Informatik-Berichte, , 2005
Interorganizational cooperation is more and more organized by the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester?s and provider?s services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline. Binding of a requester?s and a provider?s service is therefore guaranteed to result in a well-behaving cooperating service.
close
close

## Petri Net Analysis; Inductive Invariants; Linear Inequalities; Stable Properties; Traps; Co-traps; Invariants

### Publikationen in Zeitschriften und Büchern

• Characterizing Stable Inequalities of Petri Nets
Devillers, Raymond and Valmari, Antti, editors
In Application and Theory of Petri Nets and Concurrency, volume 9115 of Lecture Notes in Computer Science, Springer International Publishing, 2015
close

## Petri Net Kernel

### Dokumentationen

• The Petri Net Kernel - Documentation of the application interface
jan 1999
This document is a combined tutorial and reference guide to the Petri Net Kernel version 2.0 (PNK 2.0 for short). It extends the English short version of the documentation of the PNK 1.1. Due to many request from outside Germany, we have decided not to carry on the German documentation but to provide a full English documentation from version 2.0 on. We hope that German users are not too unhappy about that. In the PNK 2.0, we have extended the interface and slightly improved the editor which is delivered with the PNK. In particular, we have extended the net type interface for defining extensions for any net element: places, transitions, and arcs. With PNK 2.0, we have reached a stable interface for application programmers. Of course, there are ideas for improving the PNK. These ideas, however, do not concern the application interface but will provide more flexible and user definable graphics - including a more appealing graphical user interface and editor functionality. We hope that you enjoy using the Petri Net Kernel and we are grateful for any feedback - positive or negative.
close
close
• ### Konferenzbeiträge auf Workshops

• The Petri Net Kernel
Hartmut Ehrig and Wolfgang Reisig and Grzegorz Rozenberg and Herbert Weber, editors
In Petri Net Technology for Communication-Based Systems, volume 2472 of Lecture Notes in Computer Science, Springer-Verlag, 2003
The Petri Net Kernel (PNK) is an infrastructure for building Petri net tools. It relieves the programmer of a Petri net tool of implementing standard functionality on Petri nets. Moreover, it allows users to customize and to extend a PNK based tool according to their needs. In this paper, we discuss the goals, the concepts, and the realization of the Petri Net Kernel.
close
close
• Ermel, Claudia, Weber, Michael
Implementation of Parameterized Net Classes with the Petri Net Kernel of the Petri Net Baukasten
Hartmut Ehrig and Gabriel Juhas and Julia Padberg and Grzegorz Rozenberg, editors
In Unifying Petri Nets, Advances in Petri Nets, volume 2128 of Lecture Notes in Computer Science, Springer-Verlag, 2001
We show in this paper how the formalism of Parameterized Net Classes is realized with the Petri Net Kernel. Parameterized Net Classes are an notion of Petri nets using formal parameters to express Petri net type characteristics. This formalism allows the abstract formulation of formal concepts for a large variety of Petri net types. The Petri Net Kernel is a tool infrastructure supporting an easy implementation of Petri net algorithms. Moreover, the Petri Net Kernel is not restricted to a fixed Petri net type. Instead, only the net type has to be implemented as ?net type specification?. It is then used as basis for implemented application algorithms. In our paper we describe an implementation of the formal net type parameters via an interface such that the parameter implementation can be transformed to a net type specification for the Petri Net Kernel. This allows on the one hand a simple change of the net type by selecting a different combination of the actual net type parameters. On the other hand, applications (like simulation or analysis algorithms) can be developed generically, i.e. independently of the Petri net type, thus supporting rapid prototyping for Petri net tools. The implementation is embedded in the development of the Petri Net Baukasten and is therefore closely related to the contributions [3, 8, 24] in this volume.
close
close
• Weber, Michael
The new Petri Net Kernel
In Tool Demonstrations, 22nd ICATPN, Newcastle upon Tyne, U.K., jun 2001
close

• The Petri Net Kernel
, editors
In Tool Demonstrations, 21. ICATPN, , jun 2000
close
• Weber, Michael

J. Desel, A. Oberweis, editors
In , , oct 1999
close

• E. Schnieder, editors
In Entwicklung und Betrieb komplexer Automatisierungssysteme, 6. Fachtagung, Band II, may 1999
close

• The Petri Net Kernel - An Infrastructure for Building Petri Net Tools
In 20th International Conference on Application and Theory of Petri Nets - Petri Net Tool Presentations, College of William and Mary, Williamsburg, Virginia, USA, jun 1999
The Petri Net Kernel is an infrastructure for building Petri net tools. It relieves the programmer of a Petri net tool from implementing standard functionality on Petri nets. In this paper, we briefly discuss the motivation, the concepts, and the realization of the Petri Net Kernel.
close
close
• Kindler, Ekkart
Der Petrinetz-Kern: Ein Traum wird wahr
1997
close

• Der Traum von einem universellen Petrinetz-Werkzeug - Der Petrinetz-Kern
, editors
In , , oct 1996
close
• ### Publikationen in Zeitschriften und Büchern

• The Petri Net Kernel - An Infrastructure for Building Petri Net Tools
volume 3 of International Journal on Software Tools for Technology Transfer (STTT) 3 (4), sep 2001
The Petri Net Kernel is an infrastructure for building Petri net tools. It relieves the programmer of a Petri net tool from implementing standard operations on Petri nets and a graphical user interface. In this paper, we discuss the motivation, the concepts, and the implementation of the Petri Net Kernel.
close
close
• ### Studien- und Diplomarbeiten

• Gabriel, Yvonne
Anbindung externer Werkzeuge an den Petrinetz-Kern am Beispiel des Integrated Net Analyser
Studienarbeit, apr 2004
close
• ### Technische Berichte

• Hauptmann, Jens, Hohberg, Bodo, Kindler, Ekkart, Schwenzer, Ines, Weber, Michael
Der Petrinetz-Kern - Dokumentation der Anwendungs-Schnittstelle
Informatik-Berichte, , feb 1998
close

## Petrinetze

### Konferenzbeiträge auf Workshops

• Fahland, Dirk, Weidlich, Matthias
Scenario-based process modeling with Greta
Marcello La Rosa, editors
In Proc. of BPM Demonstration Track 2010, Hoboken, USA, September 14-16, 2010, volume 615 of CEUR-WS.org, Hoboken, USA, September 2010
Designing understandable business process models is one of the key factors to successful business process management. Current modeling practices advocate the use of block-oriented concepts and subprocesses to structure complex process models. However, such guidelines cannot be applied in any case as case studies in process mining have shown. Previously, we proposed the scenario-based paradigm to structure models of complex processes in behavioral fragments, i.e., scenarios. This paper presents GRETA as a tool that supports scenario-based process modeling and execution.
close
close
• Fahland, Dirk
Oclets - scenario-based modeling with Petri nets
Giuliana Franceschinis and Karsten Wolf, editors
In 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, Springer-Verlag, Paris, France, jun 2009
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.
close
close
• Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
John Krogstie and Terry Halpin and Erik Proper, editors
In 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, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
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.
close
close
• Fahland, Dirk, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
Declarative vs. Imperative Process Modeling Languages: The Issue of Maintainability
Stefanie Rinderle-Ma and Shazia Wasim Sadiq and Frank Leymann, editors
In Business Process Management Workshops, BPM 2009 International Workshops, Ulm, Germany, September 7, 2009. Revised Papers, volume 43 of Lecture Notes in Business Information Processing, Springer, Ulm, Germany, sep 2009
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.
close
close
• Fahland, Dirk
A scenario is a behavioral view - Orchestrating services by scenario integration
Oliver Kopp and Niels Lohmann, editors
In Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, mar 2009
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.
close
close
• Fahland, Dirk, Favre, C\'edric, Jobstmann, Barbara, Koehler, Jana, Lohmann, Niels, Völzer, Hagen, Wolf, Karsten
Instantaneous Soundness Checking of Industrial Business Process Models
Umeshwar Dayal and Johann Eder and Jana Koehler and Hajo Reijers, editors
In Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings, volume 5701 of Lecture Notes in Computer Science, Springer-Verlag, sep 2009
close
• Fahland, Dirk, Woith, Heiko
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, Springer, Milan, Italy, September 2008
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.
close
close
• Fahland, Dirk
Diehl, Malte and Lipskoch, Henrik and Meyer, Roland and Storm, Christian, editors
In Proceedings des gemeinsamen Workshops der Graduiertenkollegs, Trustworthy Software Systems, Gito-Verlag, Berlin, 2008
close
• Fahland, Dirk
Oclets -- Scenario-Based Modeling with Petri Nets
Niels Lohmann and Karsten Wolf, editors
In 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, CEUR-WS.org, sep 2008
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.
close
close
• Fahland, Dirk
Towards Analyzing Declarative Workflows
Jana Koehler and Marco Pistore and Amit P. Sheth and Paolo Traverso and Martin Wirsing, editors
In Autonomous and Adaptive Web Services, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007
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.
close
close
• Fahland, Dirk
Synthesizing Petri nets from LTL specifications - An engineering approach
Philippi, Stephan and Pinl, Alexander, editors
In , , September 2007
close
close
• Fahland, Dirk
Modeling and Verifying Declarative Workflows
In Dagstuhl ''zehn plus eins'', Verlagshaus Mainz, Aachen, 2007
close
• Glausch, Andreas
Eine Charakterisierung einfacher Petrinetz-Schemata
Karsten Schmidt and Christian Stahl, editors
In , , sep 2005
close
close
• ### Publikationen in Zeitschriften und Büchern

• Reisig, Wolfgang
The Decent Philosophers: An Exercise in Concurrent Behaviour
volume 80 of Fundamenta Informaticae 80 (1-3), nov 2007
Concurrent runs reveal more insight into distributed systems than interleaved runs. This is shown by help of Dijkstra's paradigm of five philosophers.
close
close
• Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian
Kommunizierende Workflow-Services modellieren und analysieren
Informatik - Forschung und Entwicklung, Springer-Verlag, oct 2005
close
close
• ### Studien- und Diplomarbeiten

• Swist, Konstanze
Modellierung des Workflows der Task Force Erdbeben des GFZ mit Petrinetzen
Studienarbeit, oct 2008
close
• Wolf, Manja

Diplomarbeit, sep 2008
close
close
• Pillat, Thomas

Diplomarbeit, mar 2008
close
close
• ### Technische Berichte

• Fahland, Dirk
Translating UML2 Activity Diagrams Petri Nets for analyzing IBM WebSphere Business Modeler process models
Informatik-Berichte, Humboldt-Universität zu Berlin, 2008
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/.
close
close
• Fahland, Dirk
Oclets - a formal approach to adaptive systems using scenario-based concepts
Informatik-Berichte, Humboldt-Universität zu Berlin, 2008
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.
close
close
• Schmidt, Karsten, Stahl, Christian

Informatik-Berichte, , sep 2005
close
• Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian

Informatik-Berichte, , feb 2005
close
close

## Sca

### Konferenzbeiträge auf Workshops

• Aalst, Wil M. P. van der, Beisiegel, Michael, Hee, Kees M. van, König, Dieter, Stahl, Christian
A SOA-Based Architecture Framework
Frank Leymann and Wolfgang Reisig and Satish R. Thatte and Wil M. P. van der Aalst, editors
In The Role of Business Processes in Service Oriented Architectures, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, nov 2006
In this paper we present first results of a SOA-based architecture framework. The architecture framework is required to be close to industry standards, especially to service component architecture (SCA), language independent (i.e. it is adoptable) and the building blocks of each system, activities and data, are first class citizens. We present a meta model of the architecture framework and discuss its concepts in detail.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Aalst, Wil M. P. van der, Beisiegel, Michael, Hee, Kees M. van, König, Dieter, Stahl, Christian
An SOA-based architecture framework
volume 2 of International Journal of Business Process Integration and Management (IJBPIM) 2 (2), 2007
We present an Service-Oriented Architecture (SOA)-based architecture framework. The architecture framework is designed to be close to industry standards, especially to the Service ComponentArchitecture (SCA).The framework is language independent and the building blocks of each system, activities and data, are first class citizens.We present a meta model of the architecture framework and discuss its concepts in detail. Through the framework, concepts of an SOA such as wiring, correlation and instantiation can be clarified.
close
close
• ### Technische Berichte

• Aalst, Wil M. P. van der, Beisiegel, Michael, Hee, Kees M. van, König, Dieter, Stahl, Christian
A SOA-Based Architecture Framework
Computer Science Report, Technische Universiteit Eindhoven, The Netherlands, jan 2007
We present a SOA-based architecture framework. The architecture framework is designed to be close to industry standards, especially to the Service Component Architecture (SCA). The framework is language independent and the building blocks of each system, activities and data, are first class citizens. We present a \emphmeta model of the architecture framework and discuss its concepts in detail. Through the framework concepts such as wiring, correlation, and instantiation can be clarified. This allows us to demystify some of the confusion related to SOA.
close
close

## Serviceautomat

### Konferenzbeiträge auf Workshops

• Parnjai, Jarungjit, Stahl, Christian, Wolf, Karsten
A finite representation of all substitutable services and its applications
Oliver Kopp and Niels Lohmann, editors
In Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, mar 2009
We present a finite representation of all substitutable services P' of a given service P. We show that our approach can be used for at least two applications: (1) given a finite set of services \mathcalP = P1, ..., Pn, we provide a representation of all services P' that can substitute every Pi \in \mathcalP, and (2) given a service P'' that cannot substitute a service P, we find the most similar service P* to P'' that can substitute P.
close
close
• Liske, Nannette, Lohmann, Niels, Stahl, Christian, Wolf, Karsten
Another Approach to Service Instance Migration
Luciano Baresi and Chi-Hung Chi and Jun Suzuki, editors
In Service-Oriented Computing - ICSOC 2009, 7th International Conference, Stockholm, Sweden, November 24-27, 2009. Proceedings, Lecture Notes in Computer Science, Springer-Verlag, nov 2009
Services change over time, be it for internal improvements, be it for external requirements such as new legal regulations. For long running services, it may even be necessary to change a service while instances are actually running and interacting with other services. This problem is referred to as instance migration. We present a novel approach to the behavioral (service protocol) aspects of instance migration. We apply techniques for finitely characterizing the set of all correctly interacting partners to a given service. The approach assures that migration does not introduce behavioral problems with any running partner of the original service. Our technique scales up to services with thousands of states, including models of real WS-BPEL processes.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Deciding Substitutability of Services with Operating Guidelines
Kurt Jensen and Wil M. P. van der Aalst, editors
volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2 (5460), Springer-Verlag, mar 2009
Deciding whether a service S can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of restriction can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
close
close
• ### Studien- und Diplomarbeiten

• Gierds, Christian
Strukturelle Reduktion von Bedienungsanleitungen
Diplomarbeit, jan 2008
close
close
• ### Technische Berichte

• Deciding Substitutability of Services with Operating Guidelines
Informatik-Berichte, Humboldt-Universität zu Berlin, apr 2008
Deciding whether a service $S$ can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of deprecation can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
close
close

## Services

### Dissertationen und Habilitationen

• Stahl, Christian
Service Substitution - A Behavioral Approach Based on Petri Nets
Dissertation, Dec 2009
Service-Oriented Computing is an emerging computing paradigm that supports the modular design of (software) systems. Complex systems are designed by composing less complex systems, called services. Such a (complex) system is a distributed application often involving several cooperating enterprises. As a system usually changes over time, individual services will be substituted by other services. Substituting one service by another one should not affect the correctness of the overall system. Assuring correctness becomes particularly challenging, as the services rely on each other, and each of the involved enterprises only oversees a part of the overall system. In addition, services communicate asynchronously which makes the analysis even more difficult. For this reason, formal methods to support service substitution are indispensable. In this thesis, we study service substitution at the level of service models. Thereby we restrict ourselves to service behavior. As a formalism to model service behavior, we use Petri nets. The first contribution of this thesis is the definition of several substitutability criteria that are suitable in the context of Service-Oriented Computing. Substituting a service S by a service S' should preserve some behavioral properties of the overall system. For each set of behavioral properties and a given service S, there exists a set of behaviorally compatible services for S. A substitutability criterion defines which of these behaviorally compatible services of S have to be preserved by S'. We relate our substitutability criteria to preorders and equivalences known from process theory. The second contribution of this thesis is to present, for each substitutability criterion, a procedure to decide whether a service S' can substitute a service S. The decision requires the comparison of the in general infinite sets of behaviorally compatible services for the services S and S'. Hence, we extend existing work on an abstract representation of all behaviorally compatible services for a given service. For each notion of behavioral compatibility, we present an algorithmic solution to represent all behaviorally compatible services. Based on these representations, we can decide substitutability of a service S by a service S'. The third contribution of this thesis is a method to support the design of a service S' that can substitute a service $S$ according to a substitutability criterion. Our approach is to derive a service S' from the service S by stepwise transformation. To this end, we present several transformation rules. Finally, we formalize and we extend the equivalence notion for services specified in the language WS-BPEL. That way, we demonstrate the applicability of our work.
close
close
• ### Konferenzbeiträge auf Workshops

• Liske, Nannette, Lohmann, Niels, Stahl, Christian, Wolf, Karsten
Another Approach to Service Instance Migration
Luciano Baresi and Chi-Hung Chi and Jun Suzuki, editors
In Service-Oriented Computing - ICSOC 2009, 7th International Conference, Stockholm, Sweden, November 24-27, 2009. Proceedings, Lecture Notes in Computer Science, Springer-Verlag, nov 2009
Services change over time, be it for internal improvements, be it for external requirements such as new legal regulations. For long running services, it may even be necessary to change a service while instances are actually running and interacting with other services. This problem is referred to as instance migration. We present a novel approach to the behavioral (service protocol) aspects of instance migration. We apply techniques for finitely characterizing the set of all correctly interacting partners to a given service. The approach assures that migration does not introduce behavioral problems with any running partner of the original service. Our technique scales up to services with thousands of states, including models of real WS-BPEL processes.
close
close
• Fahland, Dirk
A scenario is a behavioral view - Orchestrating services by scenario integration
Oliver Kopp and Niels Lohmann, editors
In Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, mar 2009
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.
close
close
• Parnjai, Jarungjit, Stahl, Christian, Wolf, Karsten
A finite representation of all substitutable services and its applications
Oliver Kopp and Niels Lohmann, editors
In Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, mar 2009
We present a finite representation of all substitutable services P' of a given service P. We show that our approach can be used for at least two applications: (1) given a finite set of services \mathcalP = P1, ..., Pn, we provide a representation of all services P' that can substitute every Pi \in \mathcalP, and (2) given a service P'' that cannot substitute a service P, we find the most similar service P* to P'' that can substitute P.
close
close
• Wolf, Karsten, Stahl, Christian, Ott, Janine, Danitz, Robert
Verifying Livelock Freedom in an SOA Scenario
Stephen Edwards and Walter Vogler, editors
In Proceedings of the Ninth International Conference on Application of Concurrency to System Design (ACSD'09), IEEE Computer Society, Augsburg, Germany, jul 2009
In a service-oriented architecture (SOA), a service broker assigns a previously published service (stored in a service registry) to a service requester. It is desirable for the composition of the requesting and the assigned service to interact properly. While proper interaction is often reduced to deadlock freedom of the composed system, we additionally consider livelock freedom as a desirable property for the interaction of services. In principle, deadlock- and livelock freedom can be verified by inspecting the state space of the composition of (public views of) the involved services. The contribution of this paper is to propose a methodology to build that state space from pre-computed fragments which are computed upon publishing a service. That way, we shift computation time from the time critical request phase of service brokerage to the less critical publish phase. Interestingly, our setting enables state space reduction methods that are intrinsically different from traditional state space reductions.
close
close
• Stahl, Christian, Wolf, Karsten
Covering Places and Transitions in Open Nets
Marlon Dumas and Manfred Reichert, editors
In Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, Springer-Verlag, sep 2008
We present a finite representation of all services M where the composition with a given service N is deadlock-free, and a given set of activities of N can be covered (i.e. is not dead). Our representation is an extension of the existing notion of an operating guideline which only cared about deadlock freedom. We further present an algorithm to decide whether a service M matches with the extended operating guideline of N.
close
close
• Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
From Public Views to Private Views -- Correctness-by-Design for Services
Marlon Dumas and Reiko Heckel, editors
In Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, Springer-Verlag, 2008
Service orientation is a means for integrating across diverse systems. Each resource, whether an application, system, or trading partner, can be accessed as a service. The resulting architecture, often referred to as SOA, has been an important enabler for interorganizational processes. Apart from technological issues that need to be addressed, it is important that all parties involved in such processes agree on the "rules of engagement". Therefore, we propose to use a contract that specifies the composition of the public views of all participating parties. Each party may then implement its part of the contract such that the implementation (i.e., the private view) accords with the contract. In this paper, we define a suitable notion of accordance inspired by the asynchronous nature of services. Moreover, we present several transformation rules for incrementally building a private view such that accordance with the contract is guaranteed by construction. These rules include adding internal tasks as well as the reordering of messages and are therefore much more powerful than existing correctness-preserving construction rules.
close
close
• Lohmann, Niels
A Feature-Complete Petri Net Semantics for WS-BPEL 2.0
Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, jun 2007
We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.
close
close
• Massuthe, Peter, Wolf, Karsten
An Algorithm for Matching Nondeterministic Services with Operating Guidelines
Frank Leymann and Wolfgang Reisig and Satish R. Thatte and Wil M. P. van der Aalst, editors
In The Role of Business Processes in Service Oriented Architectures, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2006
Interorganizational cooperation is more and more organized by the paradigm of services. Service-oriented architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester, and the service broker, together with the three operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artifact to realize the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free communication. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.
close
close
• Kaschner, Kathrin, Massuthe, Peter, Wolf, Karsten

Daniel Moldt, editors
In , , sep 2006
close

• Analyzing Interacting BPEL Processes
In Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings, volume 4102 of Lecture Notes in Computer Science, Springer-Verlag, sep 2006
This paper addresses the problem of analyzing theinteraction between BPEL processes. We present a technology chain that starts out with a BPEL process and transforms it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). A case study demonstrates the value of this technology chain.
close
close
• Reisig, Wolfgang, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela, Wolf, Karsten, Kaschner, Kathrin
Analysis Techniques for Service Models
In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, IEEE Computer Society, nov 2006
The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.
close
close
• Massuthe, Peter, Schmidt, Karsten
Operating Guidelines - an Automata-Theoretic Foundation for the Service-Oriented Architecture
Kai-Yuan Cai and Atsushi Ohnishi and M.F. Lau, editors
In Proceedings of the Fifth International Conference on Quality Software (QSIC 2005), IEEE Computer Society, Melbourne, Australia, sep 2005
In the service-oriented architecture (SOA), we distinguish three roles of service owners: service providers, service requesters, and service brokers. Each service provider publishes information to the broker about how requesters can interact with its service. Thus, the broker can assign a fitting service provider to a querying requester. We propose the information published to the broker to be operating guidelines. Operating guidelines are essentially communication instructions for the service requester. We present an automata-theoretic approach that is centered around operating guidelines and is capable of implementing all tasks arising in the SOA.
close
close
• Massuthe, Peter, Schmidt, Karsten
Operating Guidelines for Services
Karsten Schmidt and Christian Stahl, editors
In , , sep 2005
In the service-oriented architecture (SOA), we distinguish three roles of service owners:service providers, service requesters, and service brokers, and the three standard operations publish, find, and bind. We provide a formal method based on Petri nets to model services. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
volume 53 of The Computer Journal 53 (1), 2010
To implement an interorganizational process between different enterprizes, one needs to agree on the rules of engagement''. These can be specified in terms of a contract that describes the overall intended process and the duties of all parties involved. We propose to use such a process-oriented contract which can be seen as the composition of the public views of all participating parties. Based on this contract each party may locally implement its part of the contract such that the implementation (the private view) agrees on the contract. In this paper, we propose a formal notion for such process-oriented contracts and give a criterion for accordance between a private view and its public view. The public view of a party can be substituted by a private view if and only if the private view accords with the public view. Using the notion of accordance the overall implemented process is guaranteed to be deadlock-free and it is always possible to terminate properly. In addition, we present a technique for automatically checking our accordance criterion. A case study illustrates how our proposed approach can be used in practice.
close
close

• Deciding Substitutability of Services with Operating Guidelines
Kurt Jensen and Wil M. P. van der Aalst, editors
volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2 (5460), Springer-Verlag, mar 2009
Deciding whether a service S can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of restriction can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
close
close
• Stahl, Christian, Wolf, Karsten
Deciding Service Composition and Substitutability Using Extended Operating Guidelines
volume 68 of Data Knowl. Eng. 68 (9), 2009
We study the correct interaction between services using the following notion for correctness: there is no deadlock in the interaction of the services, and a given set of activities is not dead, that is, each activity in this set is executed in at least one run. The second condition has not been studied before. An operating guideline of a service P is an operational characterization of all deadlock-free interacting partners of P. In this paper, we present an extension of the concept of an operating guideline to characterize all correctly interacting partners of a service P. This extension can be used for answering at least the following two questions. First, given a service R, does R interact correctly with P? Second, given a service P', can P be substituted by P', that is, is every correctly interacting partner of P a correctly interacting partner of P', too?
close
close

• Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation
volume 64 of Data Knowl. Eng. 64 (1), jan 2008
We address the problem of analyzing the interaction between WS-BPEL processes. We present a technology chain that starts out with a WS-BPEL process and translates it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). To manage processes of realistic size, we present a concept of a \emphflexible model generation which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.
close
close
• Massuthe, Peter, Serebrenik, Alexander, Sidorova, Natalia, Wolf, Karsten
Can I find a Partner? Undecidablity of Partner Existence for Open Nets
volume 108 of Information Processing Letters 108 (6), Nov 2008
close
• Kaschner, Kathrin, Massuthe, Peter, Wolf, Karsten
Symbolic Representation of Operating Guidelines for Services
volume 72 of Petri Net Newsletter 72, apr 2007
close
• Massuthe, Peter, Wolf, Karsten
An Algorithm for Matching Non-deterministic Services with Operating Guidelines
volume 2 of International Journal of Business Process Integration and Management (IJBPIM) 2 (2), 2007
Interorganisational cooperation is more and more organised by the paradigm of services. Service-Oriented Architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester and the service broker, together with the three operations publish, find and bind. We provide a formal method based on non-deterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artefact to realise the publish operation. In our approach, the find operation reduces to a matching problem between the requesters service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free interaction. In this paper, matching of deterministic as well as non-deterministic automata with operating guidelines is presented.
close
close
• Massuthe, Peter, Wolf, Karsten
Operating Guidelines for Services
volume 70 of Petri Net Newsletter 70, apr 2006
In the service-oriented architecture (SOA), we distinguish three roles of service owners: service providers, service requesters, and service brokers, and the three standard operations publish, find, and bind. We provide a formal method based on Petri nets to model services. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester's service and the operating guideline.
close
close
• Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
An Operating Guideline Approach to the SOA
volume 1 of Annals of Mathematics, Computing \& Teleinformatics 1 (3), 2005
Interorganizational cooperation is more andmore organized by the paradigm of services. The serviceoriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester's and provider's services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester's service and the operating guideline. Binding of a requester's and a provider's service is therefore guaranteed to result in a well-behaving cooperating service. At this time, the approach is limited to acyclic Petri nets.
close
close
• ### Studien- und Diplomarbeiten

• Schulz, Alexander
Zielgerichtete Strategien
Studienarbeit, jul 2007
close
• Gierds, Christian

Studienarbeit, oct 2007
close
close
• Laufer, Peter
Public-View-Generierung
Diplomarbeit, nov 2007
close
close
• ### Technische Berichte

• Hee, Kees M. van, Verbeek, H.M.W., Stahl, Christian, Sidorova, Natalia
A Framework for Linking and Pricing No-Cure-No-Pay Services
Computer Science Report, Technische Universiteit Eindhoven, Eindhoven, The Netherlands, jun 2008
In this paper, we present a framework that allows us to orchestrate web services such that the web services involved in this orchestration interact properly. To achieve this, we predefine service interfaces and certain routing constructs. Furthermore, we define a number of rules to incrementally compute the price of such a properly interacting orchestration (i.e. a web service) from the price of its web services. The fact that a web service gets only payed after its service is delivered (no-cure-no-pay) is reflected by considering a probability of success. To determine a safe price that includes the risk a web service takes, we consider the variance of costs.
close
close

• Deciding Substitutability of Services with Operating Guidelines
Informatik-Berichte, Humboldt-Universität zu Berlin, apr 2008
Deciding whether a service $S$ can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of deprecation can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
close
close
• Aalst, Wil M. P. van der, Massuthe, Peter, Mooij, Arjan J., Stahl, Christian, Wolf, Karsten
Erratum -- Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
Informatik-Berichte, Humboldt-Universität zu Berlin, jun 2007
close
• Aalst, Wil M. P. van der, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
Informatik-Berichte, Humboldt-Universität zu Berlin, jun 2007
A contract specifies an interorganizational process together with a distribution of responsibilities for the activities among the parties involved. In this paper, we formally show how a party can implement its part of the contract such that the implementation accords with the contract. We propose a formal notion of a contract and give a criterion for accordance between a local implementation and a contract such that, if all local implementations accord with the contract, the overall process is deadlock-free and it is always possible to terminate properly. Then, we sketch a technique for automatically checking the proposed accordance criterion. Finally, we present accordance-preserving transformation rules. These rules can be used to implement a part of the contract while preserving the accordance criterion.
close
close
• Massuthe, Peter, Wolf, Karsten
An Algorithm for Matching Nondeterministic Services with Operating Guidelines
Informatik-Berichte, , 2006
Interorganizational cooperation is more and more organizedby the paradigm of services. Service-oriented architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester, and the service broker, together with the three operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artifact to realize the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlockfree communication. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.
close
close
• Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
Operating Guidelines for Finite-State Services
Informatik-Berichte, , dec 2006
We introduce the concept of an operating guideline for an arbitrary finite-state service P, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to correctly (in this paper: deadlock-free) communicate with P. It can further be executed or used for service discovery. An operating guideline for P is a particular service S that is enriched with annotations. S communicates deadlock-free with P and is able to simulate every other service that communicates deadlock-free with P. The attached annotations give complete information about whether or not a simulated service is deadlock-free, too.
close
close
• Massuthe, Peter, Schmidt, Karsten
Operating Guidelines - an Alternative to Public View
Informatik-Berichte, , 2005
We propose operating guidelines as artifacts for publishing information about how to communicate with a business process that is intended to be provided as a service. We present an approach to compute operating guidelines fully automatically. We compare operating guidelines with the concept of public view.
close
close
• Massuthe, Peter, Schmidt, Karsten
Matching Nondeterministic Services with Operating Guidelines
Informatik-Berichte, , jun 2005
Abstract Interorganizational cooperation is more and more organizedby the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester?s service and operating guidelines. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.
close
close
• Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
An Operating Guideline Approach to the SOA
Informatik-Berichte, , 2005
Interorganizational cooperation is more and more organized by the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester?s and provider?s services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline. Binding of a requester?s and a provider?s service is therefore guaranteed to result in a well-behaving cooperating service.
close
close

## Soa

### Dissertationen und Habilitationen

• Stahl, Christian
Service Substitution - A Behavioral Approach Based on Petri Nets
Dissertation, Dec 2009
Service-Oriented Computing is an emerging computing paradigm that supports the modular design of (software) systems. Complex systems are designed by composing less complex systems, called services. Such a (complex) system is a distributed application often involving several cooperating enterprises. As a system usually changes over time, individual services will be substituted by other services. Substituting one service by another one should not affect the correctness of the overall system. Assuring correctness becomes particularly challenging, as the services rely on each other, and each of the involved enterprises only oversees a part of the overall system. In addition, services communicate asynchronously which makes the analysis even more difficult. For this reason, formal methods to support service substitution are indispensable. In this thesis, we study service substitution at the level of service models. Thereby we restrict ourselves to service behavior. As a formalism to model service behavior, we use Petri nets. The first contribution of this thesis is the definition of several substitutability criteria that are suitable in the context of Service-Oriented Computing. Substituting a service S by a service S' should preserve some behavioral properties of the overall system. For each set of behavioral properties and a given service S, there exists a set of behaviorally compatible services for S. A substitutability criterion defines which of these behaviorally compatible services of S have to be preserved by S'. We relate our substitutability criteria to preorders and equivalences known from process theory. The second contribution of this thesis is to present, for each substitutability criterion, a procedure to decide whether a service S' can substitute a service S. The decision requires the comparison of the in general infinite sets of behaviorally compatible services for the services S and S'. Hence, we extend existing work on an abstract representation of all behaviorally compatible services for a given service. For each notion of behavioral compatibility, we present an algorithmic solution to represent all behaviorally compatible services. Based on these representations, we can decide substitutability of a service S by a service S'. The third contribution of this thesis is a method to support the design of a service S' that can substitute a service $S$ according to a substitutability criterion. Our approach is to derive a service S' from the service S by stepwise transformation. To this end, we present several transformation rules. Finally, we formalize and we extend the equivalence notion for services specified in the language WS-BPEL. That way, we demonstrate the applicability of our work.
close
close
• ### Konferenzbeiträge auf Workshops

• Wolf, Karsten, Stahl, Christian, Ott, Janine, Danitz, Robert
Verifying Livelock Freedom in an SOA Scenario
Stephen Edwards and Walter Vogler, editors
In Proceedings of the Ninth International Conference on Application of Concurrency to System Design (ACSD'09), IEEE Computer Society, Augsburg, Germany, jul 2009
In a service-oriented architecture (SOA), a service broker assigns a previously published service (stored in a service registry) to a service requester. It is desirable for the composition of the requesting and the assigned service to interact properly. While proper interaction is often reduced to deadlock freedom of the composed system, we additionally consider livelock freedom as a desirable property for the interaction of services. In principle, deadlock- and livelock freedom can be verified by inspecting the state space of the composition of (public views of) the involved services. The contribution of this paper is to propose a methodology to build that state space from pre-computed fragments which are computed upon publishing a service. That way, we shift computation time from the time critical request phase of service brokerage to the less critical publish phase. Interestingly, our setting enables state space reduction methods that are intrinsically different from traditional state space reductions.
close
close
• Aalst, Wil M. P. van der, Mooij, Arjan J., Stahl, Christian, Wolf, Karsten
Service Interaction: Patterns, Formalization, and Analysis
Marco Bernardo and Luca Padovani and Gianluigi Zavattaro, editors
In Formal Methods for Web Services (SFM 2009), volume 5569 of Springer-Verlag, apr 2009
As systems become more service oriented and processes increasingly cross organizational boundaries, interaction becomes more important. New technologies support the development of such systems. However, the paradigm shift towards service orientation, requires a fundamentally different way of looking at processes. This survey aims to provide some foundational notions related to service interaction. A set of service interaction patterns is given to illustrate the challenges in this domain. Moreover, key results are given for three of these challenges: (1) How to expose a service?, (2) How to replace and refine services?, and (3) How to generate service adapters? These challenges will be addressed in a Petri net setting. However, the results extend to other languages used in this domain.
close
close
• Stahl, Christian, Wolf, Karsten
Covering Places and Transitions in Open Nets
Marlon Dumas and Manfred Reichert, editors
In Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, Springer-Verlag, sep 2008
We present a finite representation of all services M where the composition with a given service N is deadlock-free, and a given set of activities of N can be covered (i.e. is not dead). Our representation is an extension of the existing notion of an operating guideline which only cared about deadlock freedom. We further present an algorithm to decide whether a service M matches with the extended operating guideline of N.
close
close
• Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
From Public Views to Private Views -- Correctness-by-Design for Services
Marlon Dumas and Reiko Heckel, editors
In Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, Springer-Verlag, 2008
Service orientation is a means for integrating across diverse systems. Each resource, whether an application, system, or trading partner, can be accessed as a service. The resulting architecture, often referred to as SOA, has been an important enabler for interorganizational processes. Apart from technological issues that need to be addressed, it is important that all parties involved in such processes agree on the "rules of engagement". Therefore, we propose to use a contract that specifies the composition of the public views of all participating parties. Each party may then implement its part of the contract such that the implementation (i.e., the private view) accords with the contract. In this paper, we define a suitable notion of accordance inspired by the asynchronous nature of services. Moreover, we present several transformation rules for incrementally building a private view such that accordance with the contract is guaranteed by construction. These rules include adding internal tasks as well as the reordering of messages and are therefore much more powerful than existing correctness-preserving construction rules.
close
close
• Reisig, Wolfgang, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela, Wolf, Karsten, Kaschner, Kathrin
Analysis Techniques for Service Models
In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, IEEE Computer Society, nov 2006
The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.
close
close
• Aalst, Wil M. P. van der, Beisiegel, Michael, Hee, Kees M. van, König, Dieter, Stahl, Christian
A SOA-Based Architecture Framework
Frank Leymann and Wolfgang Reisig and Satish R. Thatte and Wil M. P. van der Aalst, editors
In The Role of Business Processes in Service Oriented Architectures, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, nov 2006
In this paper we present first results of a SOA-based architecture framework. The architecture framework is required to be close to industry standards, especially to service component architecture (SCA), language independent (i.e. it is adoptable) and the building blocks of each system, activities and data, are first class citizens. We present a meta model of the architecture framework and discuss its concepts in detail.
close
close
• ### Publikationen in Zeitschriften und Büchern

• Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
volume 53 of The Computer Journal 53 (1), 2010
To implement an interorganizational process between different enterprizes, one needs to agree on the rules of engagement''. These can be specified in terms of a contract that describes the overall intended process and the duties of all parties involved. We propose to use such a process-oriented contract which can be seen as the composition of the public views of all participating parties. Based on this contract each party may locally implement its part of the contract such that the implementation (the private view) agrees on the contract. In this paper, we propose a formal notion for such process-oriented contracts and give a criterion for accordance between a private view and its public view. The public view of a party can be substituted by a private view if and only if the private view accords with the public view. Using the notion of accordance the overall implemented process is guaranteed to be deadlock-free and it is always possible to terminate properly. In addition, we present a technique for automatically checking our accordance criterion. A case study illustrates how our proposed approach can be used in practice.
close
close
• Mooij, Arjan J., Stahl, Christian, Voorhoeve, Marc
Relating Fair Testing and Accordance for Service Replaceability
Journal of Logic and Algebraic Programming, 2010
The accordance pre-order describes whether a service can safely be replaced by another service. That is, all partners for the original service should be partners for the new service. Partners for a service interact with the service in such a way that always a certain common goal can be reached. We relate the accordance pre-order to the pre-orders known from the linear-branching time spectrum, notably fair testing. The differences between accordance and fair testing include the modeling of termination and success, and the parts of the services that cannot be used reliably by any partner. Apart from the theoretical results, we address the practical relevance of the introduced concepts.
close
close
• Hee, Kees van, Verbeek, Eric, Stahl, Christian, Sidorova, Natalia
A Framework for Linking and Pricing No-Cure-No-Pay Services
Kurt Jensen and Wil M. P. van der Aalst, editors
volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2, Springer-Verlag, mar 2009
In this paper, we present a framework that allows us to orchestrate web services such that the web services involved in this orchestration interact properly. To achieve this, we predefine service interfaces and certain routing constructs. Furthermore, we define a number of rules to incrementally compute the price of such a properly interacting orchestration (i.e. a web service) from the price of its web services. The fact that a web service gets only payed after its service is delivered (no-cure-no-pay) is reflected by considering a probability of success. To determine a safe price that includes the risk a web service takes, we consider the variance of costs.
close
close

• Deciding Substitutability of Services with Operating Guidelines
Kurt Jensen and Wil M. P. van der Aalst, editors
volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2 (5460), Springer-Verlag, mar 2009
Deciding whether a service S can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of restriction can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
close
close
• Aalst, Wil M. P. van der, Beisiegel, Michael, Hee, Kees M. van, König, Dieter, Stahl, Christian
An SOA-based architecture framework
volume 2 of International Journal of Business Process Integration and Management (IJBPIM) 2 (2), 2007
We present an Service-Oriented Architecture (SOA)-based architecture framework. The architecture framework is designed to be close to industry standards, especially to the Service ComponentArchitecture (SCA).The framework is language independent and the building blocks of each system, activities and data, are first class citizens.We present a meta model of the architecture framework and discuss its concepts in detail. Through the framework, concepts of an SOA such as wiring, correlation and instantiation can be clarified.
close
close
• ### Studien- und Diplomarbeiten

• Laufer, Peter
Public-View-Generierung
Diplomarbeit, nov 2007
close
close
• ### Technische Berichte

• Deciding Substitutability of Services with Operating Guidelines
Informatik-Berichte, Humboldt-Universität zu Berlin, apr 2008
Deciding whether a service $S$ can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of deprecation can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
close
close
• Hee, Kees M. van, Verbeek, H.M.W., Stahl, Christian, Sidorova, Natalia
A Framework for Linking and Pricing No-Cure-No-Pay Services
Computer Science Report, Technische Universiteit Eindhoven, Eindhoven, The Netherlands, jun 2008
In this paper, we present a framework that allows us to orchestrate web services such that the web services involved in this orchestration interact properly. To achieve this, we predefine service interfaces and certain routing constructs. Furthermore, we define a number of rules to incrementally compute the price of such a properly interacting orchestration (i.e. a web service) from the price of its web services. The fact that a web service gets only payed after its service is delivered (no-cure-no-pay) is reflected by considering a probability of success. To determine a safe price that includes the risk a web service takes, we consider the variance of costs.
close
close
• König, Dieter, Lohmann, Niels, Moser, Simon, Stahl, Christian, Wolf, Karsten
Extending the Compatibility Notion for Abstract WS-BPEL Processes
Preprint, Universität Rostock, Rostock, Germany, nov 2007
WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.
close
close
• Hee, Kees M. van, Sidorova, Natalia, Stahl, Christian, Verbeek, H. M. W.
A Price of Service in a Compositional SOA Framework
Computer Science Report, Technische Universiteit Eindhoven, The Netherlands, jul 2007
In this paper we propose a framework for SOA covering such important features as proper termination (soundness) and correct correlation of tasks. Within this framework, we define a method for the calculation of the price of services. Our framework is compositional in the sense that composing a system from subsystems that meet our correctness requirements we obtain a system that still meets these requirements.
close
close
• Aalst, Wil M. P. van der, Beisiegel, Michael, Hee, Kees M. van, König, Dieter, Stahl, Christian
A SOA-Based Architecture Framework
Computer Science Report, Technische Universiteit Eindhoven, The Netherlands, jan 2007
We present a SOA-based architecture framework. The architecture framework is designed to be close to industry standards, especially to the Service Component Architecture (SCA). The framework is language independent and the building blocks of each system, activities and data, are first class citizens. We present a \emphmeta model of the architecture framework and discuss its concepts in detail. Through the framework concepts such as wiring, correlation, and instantiation can be clarified. This allows us to demystify some of the confusion related to SOA.
close
close

## Soundness

### Konferenzbeiträge auf Workshops

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

## Szenario-basierte Modelle

### Konferenzbeiträge auf Workshops

• Fahland, Dirk, Weidlich, Matthias
Scenario-based process modeling with Greta
Marcello La Rosa, editors
In Proc. of BPM Demonstration Track 2010, Hoboken, USA, September 14-16, 2010, volume 615 of CEUR-WS.org, Hoboken, USA, September 2010
Designing understandable business process models is one of the key factors to successful business process management. Current modeling practices advocate the use of block-oriented concepts and subprocesses to structure complex process models. However, such guidelines cannot be applied in any case as case studies in process mining have shown. Previously, we proposed the scenario-based paradigm to structure models of complex processes in behavioral fragments, i.e., scenarios. This paper presents GRETA as a tool that supports scenario-based process modeling and execution.
close
close
• Fahland, Dirk
Oclets - scenario-based modeling with Petri nets
Giuliana Franceschinis and Karsten Wolf, editors
In 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, Springer-Verlag, Paris, France, jun 2009
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.
close
close
• Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
John Krogstie and Terry Halpin and Erik Proper, editors
In 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, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
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.
close
close
• Fahland, Dirk
A scenario is a behavioral view - Orchestrating services by scenario integration
Oliver Kopp and Niels Lohmann, editors
In Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, mar 2009
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.
close
close
• Fahland, Dirk, Woith, Heiko
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, Springer, Milan, Italy, September 2008
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.
close
close
• Fahland, Dirk
Oclets -- Scenario-Based Modeling with Petri Nets
Niels Lohmann and Karsten Wolf, editors
In 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, CEUR-WS.org, sep 2008
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.
close
close
• Fahland, Dirk
Diehl, Malte and Lipskoch, Henrik and Meyer, Roland and Storm, Christian, editors
In Proceedings des gemeinsamen Workshops der Graduiertenkollegs, Trustworthy Software Systems, Gito-Verlag, Berlin, 2008
close
• Fahland, Dirk
Modeling and Verifying Declarative Workflows
In Dagstuhl ''zehn plus eins'', Verlagshaus Mainz, Aachen, 2007
close
• Fahland, Dirk
A Formal Approach to Adaptive Processes using Scenario-based Concepts.
Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, Siedlce, Poland, jun 2007
close
close
• ### Studien- und Diplomarbeiten

• Wolf, Manja

Diplomarbeit, sep 2008
close
close
• ### Technische Berichte

• Fahland, Dirk
Oclets - a formal approach to adaptive systems using scenario-based concepts
Informatik-Berichte, Humboldt-Universität zu Berlin, 2008
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.
close
close

## Temporale Logik

### Konferenzbeiträge auf Workshops

• Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
John Krogstie and Terry Halpin and Erik Proper, editors
In 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, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
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.
close
close
• Fahland, Dirk
Modeling and Verifying Declarative Workflows
In Dagstuhl ''zehn plus eins'', Verlagshaus Mainz, Aachen, 2007
close
• Fahland, Dirk
Synthesizing Petri nets from LTL specifications - An engineering approach
Philippi, Stephan and Pinl, Alexander, editors
In , , September 2007
close
close
• Fahland, Dirk
Towards Analyzing Declarative Workflows
Jana Koehler and Marco Pistore and Amit P. Sheth and Paolo Traverso and Martin Wirsing, editors
In Autonomous and Adaptive Web Services, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007
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.
close
close
Compositional Temporal Logic Based on Partial Order
In 11th International Symposium on Temporal Representation and Reasoning (TIME'04), IEEE Computer Society, 2004
The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. The logic supports a compositional design of systems: subsystems can be specified separately and then be integrated into one system. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.
close
close
Logic of Involved Variables - System Specification with Temporal Logic of Distributed Actions
In Proc. of the 3rd International Conference on Application of Concurrency to System Design (ACSD'03), Guimaraes, Portugal , IEEE Computer Society, jun 2003
The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA can be syntactically viewed as a slight extension of TLA. We propose a different semantical model based on partial order which evidently increases the expressiveness of the logic. Local variable updates in a system are explicitly modeled and expressed by TLDA formulas. Consequently, we can distinguish between concurrency and nondeterministic choice. All valuable features of TLA (composition is conjunction, implementation is implication) are retained. In addition, we are able to describe some important phenomena and properties typical for distributed systems.
close
close
• ### Studien- und Diplomarbeiten

• Lohmann, Niels

Diplomarbeit, sep 2005
close
close
• Lohmann, Niels

Studienarbeit, jun 2005
close
close
• Kuhtz, Lars
TLDA und Petrinetze
Studienarbeit, apr 2004
close
• Massuthe, Peter
Verfeinerungstechniken der Temporal Logic of Distributed Actions TLDA
Diplomarbeit, mar 2004
close
close
• Massuthe, Peter
Parallele Komposition in TLA
Studienarbeit, sep 2003
close
close
• ### Technische Berichte

A Temporal Logic of Distributed Actions (TLDA)
Informatik-Berichte, , 2000
close

## Tlda

### Konferenzbeiträge auf Workshops

Compositional Temporal Logic Based on Partial Order
In 11th International Symposium on Temporal Representation and Reasoning (TIME'04), IEEE Computer Society, 2004
The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. The logic supports a compositional design of systems: subsystems can be specified separately and then be integrated into one system. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.
close
close
Logic of Involved Variables - System Specification with Temporal Logic of Distributed Actions
In Proc. of the 3rd International Conference on Application of Concurrency to System Design (ACSD'03), Guimaraes, Portugal , IEEE Computer Society, jun 2003
The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA can be syntactically viewed as a slight extension of TLA. We propose a different semantical model based on partial order which evidently increases the expressiveness of the logic. Local variable updates in a system are explicitly modeled and expressed by TLDA formulas. Consequently, we can distinguish between concurrency and nondeterministic choice. All valuable features of TLA (composition is conjunction, implementation is implication) are retained. In addition, we are able to describe some important phenomena and properties typical for distributed systems.
close
close
• ### Studien- und Diplomarbeiten

• Lohmann, Niels

Diplomarbeit, sep 2005
close
close
• Lohmann, Niels

Studienarbeit, jun 2005
close
close
• Kuhtz, Lars
TLDA und Petrinetze
Studienarbeit, apr 2004
close
• Massuthe, Peter
Verfeinerungstechniken der Temporal Logic of Distributed Acti