## Acu, Baver

### 2006

• Compensation in Workflow Nets
Susanna Donatelli and P. S. Thiagarajan, editors
In Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, Springer, 2006
close

## Bretschneider, Jan

### 2009

• 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
• ### 2008

• 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
• ### 2007

• Services as a Paradigm of Computation
Cliff B. Jones and Zhiming Liu and Jim Woodcock, editors
In Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj\orner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, volume 4700 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.
close
close
• Bretschneider, Jan
Produktbedienungsanleitungen zur Charakterisierung austauschbarer Services
Diplomarbeit, mar 2007
close
close
• Reisig, Wolfgang, Wolf, Karsten, Bretschneider, Jan, Kaschner, Kathrin, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
Challenges in a Service-Oriented World
volume 70 of ERCIM News 70, jul 2007
Interacting services raise a number of new software engineering challenges. To meet these challenges, the behaviour of the involved services must be considered. We present results regarding the behaviour of services in isolation, the interaction of services in choreographies, the exchangeability of a service, and the synthesis of desired partner services.
close
close
• ### 2006

• Bretschneider, Jan
Modellierung und Synthese eines geschwindigkeitsinvarianten GALS-Wrappers
Studienarbeit, feb 2006
close
close

## Fahland, Dirk

### 2013

• Analyzing and Completing Middleware Designs for Enterprise Integration Using Coloured Petri Nets
In CAiSE, 2013
close

• Discovering Pattern-Based Mediator Services from Communication Logs
In WESOA, 2013
close
• ### 2012

• Using Petri Nets for Modeling Enterprise Integration Patterns
bpmcenter.org, 2012
close

• Data and Abstraction for Scenario-Based Modeling with Petri Nets
In Petri Nets, 2012
close
• ### 2010

• Pinggera, Jakob, Zugal, Stefan, Weber, Barbara, Fahland, Dirk, Weidlich, Matthias, Mendling, Jan, Reijers, Hajo
How the Structuring of Domain Knowledge Can Help Casual Process Modelers
In ER 2010, 2010
close
close
• Weidlich, Matthias, Zugal, Stefan, Pinggera, Jakob, Fahland, Dirk, Weber, Barbara, Reijers, Hajo, Mendling, Jan
The Impact of Sequential and Circumstantial Changes on Process Models
Bela Mutschler and Jan Recker and Roel Wieringa, editors
In Proc. ER-POIS 2010, held in conjunction with CAiSE 2010, volume 603 of CEUR-WS, 2010
While process modeling has become important for documenting business operations and automating workflow execution, there are serious issues with efficiently and effectively creating and modifying process models. While prior research has mainly investigated process model comprehension, there is hardly any work on maintainability of process models. Cognitive research into software program comprehension has demonstrated that imperative programs are strong in conveying sequential information while obfuscating circumstantial information. This paper addresses the question whether these findings can be transferred to process model maintenance. In particular, it investigates whether it is easier to incorporate sequential change requirements in imperative process models compared to circumstantial change requirements. To address this question this paper presents results from a controlled experiment providing evidence that the type of change (sequential versus circumstantial) has an effect on the accuracy of process models. For performance indicators modeling speed, correctness, and cognitive load no statistically significant differences could be identified.
close
close
• 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
• ### 2009

• 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, 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, 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
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
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
• ### 2008

• 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, 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
Adaptive und Selbststabilisierende Workflows
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 - 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
• 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
• ### 2007

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

• Services as a Paradigm of Computation
Cliff B. Jones and Zhiming Liu and Jim Woodcock, editors
In Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj\orner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, volume 4700 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.
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
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
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, , Quilitz, Bastian, , Leser, Ulf
HUODINI - Flexible Information Integration for Disaster Management
In 4th International Conference on Information Systems for Crisis Response and Management (ISCRAM), Delft, NL, 2007
Fast and effective disaster management requires access to a multitude of heterogeneous, distributed, and quickly changing data sets, such as maps, satellite images, or governmental databases. In the last years, also the information created by affected persons on web sites such as flickr.com or blogger.com became an important and very quickly adapting source of information. We developed HUODINI, a prototype system for the flexible integration and visualization of heterogeneous data sources for disaster management. HUODINI is based on Semantic Web technologies, and in particular RDF, to offer maximal flexibility in the types of data sources it can integrate. It supports a hybrid push/pull approach to cater for the requirements of fast-changing sources, such as news feeds, and maximum performance for querying the integrated data set. In this paper, we describe the design goals underlying our approach, its architecture, and report on first experiences with the system.
close
close
• ### 2006

• 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
• Fahland, Dirk
Unfoldings for Timed Automata
Diplomarbeit, July 2006
In this thesis we develop a state space reduction technique for networks of timed automata based on unfoldings to alleviate the state space explosion problem due to concurrently enabled actions. For the purpose of verifying a system, standard model checking techniques construct its sequential state space that suffers an exponential growth when applied to distributed systems because of concurrently enabled, independent actions: during the construction of the state space these actions are ordered arbitrarily to simulate concurrency in the sequential model. For untimed systems, state space reduction techniques like stubborn sets that omit the construction of redundant information, and unfoldings that represent concurrent events in a partial order have successfully been applied to alleviate the exponential growth. These techniques apply a simple syntactical criterion to identify independent actions. This criterion is not applicable to networks of timed automata as simple examples show, which renders the existing techniques unapplicable. But networks of timed automata face the state space explosion problem as well which raises the demand for a specific reduction technique for these systems. In this thesis, we consider a special, but practically relevant class of networks of timed automata as a formal model for discrete, distributed, timed systems. We develop a novel technique that constructs a complete, finite representation of such a system's state space. This representation is the complete, finite prefix of an unfolding in which concurrently enabled actions are partially ordered. We show that this technique is capable of reducing the size of the state space by magnitude. We are presently not aware of any state space reduction technique for timed automata with similar results.
close
close
• ### 2005

• Fahland, Dirk
Complete Abstract Operational Semantics for the Web Service Business Process Execution Language
Informatik-Berichte, , sep 2005
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
• ### 2004

• Fahland, Dirk
Ein Ansatz einer formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines
Studienarbeit, aug 2004
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

## Fichte, Johannes Klaus

### 2009

• Atserias, Albert, Fichte, Johannes Klaus, Thurley, Marc
Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
In SAT, 2009
close

## Görlach, Katharina

### 2007

• Moser, Simon, Martens, Axel, Görlach, Katharina, Amme, Wolfram, Godlinski, Artur
Advanced Verification of Distributed WS-BPEL Business Processes Incorporating CSSA-based Data Flow Analysis
In IEEE International Conference on Services Computing (SCC 2007), 2007
The Business Process Execution Language for Web Services WS-BPEL provides an technology to aggregate encapsulated functionalities for defining high-value Web services. For a distributed application in a B2B interaction, the partners simply need to expose their provided functionality as BPEL processes and compose them. Verifying such distributed web service based systems has been a huge topic in the research community lately - cf. [4] for a good overview. However, in most of the work on analyzing properties of interacting Web Services, especially when backed by stateful implementations like WS-BPEL, the data flow present in the implementation is widely neglected, and the analysis focusses on control flow only. This might lead to false-positive analysis results when searching for design weaknesses and errors, e.g. analyzing the controllability [14] of a given BPEL process. In this paper, we present a method to extract data flow information by constructing a CSSA representation and detecting data dependencies that effect communication behavior. Those discovered dependencies are used to construct a more precise formal model of the given BPEL process and hence to improve the quality of analysis results.
close
close

## Gierds, Christian

### 2013

• Analyzing and Completing Middleware Designs for Enterprise Integration Using Coloured Petri Nets
In CAiSE, 2013
close

• Discovering Pattern-Based Mediator Services from Communication Logs
In WESOA, 2013
close
• ### 2012

• Using Petri Nets for Modeling Enterprise Integration Patterns
bpmcenter.org, 2012
close
• Gierds, Christian, Mooij, Arjan J., Wolf, Karsten
Reducing Adapter Synthesis to Controller Synthesis
volume 5 of IEEE T. Services Computing 5 (1), 2012
close
• ### 2010

• Estimating costs of a service
Christian Gierds and Jan Sürmeli, editors
In Proceedings of the 2nd Central-European Workshop on Services and their Composition, ZEUS 2010, Berlin, Germany, February 25--26, 2010, volume 563 of CEUR Workshop Proceedings, CEUR-WS.org, 2010
When designing a publicly available Web service, a service designer has to take care of costs and revenue caused by this services. In the very beginning possible partners might only be vaguely known, or the service behavior contains arbitrary repetitions. Then the estimation of costs for running this service is difficult and decisions based on them can hardly be made. We propose a static analysis of the service's behavior. We over-approximate possible runs and therefore costs of the service. Our approach provides a basis for reasoning about nonfunctional properties as shown for costs.
close
close

• A Graphical User Interface for Service Adaptation
Martin Schwarick and Monika Heiner, editors
In Proceedings of the 17th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2010, Cottbus, Germany, October 07-08, 2010, volume 643 of CEUR Workshop Proceedings, CEUR-WS.org, oct 2010
close
• ### 2008

• Gierds, Christian
Strukturelle Reduktion von Bedienungsanleitungen
Diplomarbeit, jan 2008
close
close
• Gierds, Christian, Mooij, Arjan J., Wolf, Karsten
Specifying and generating behavioral service adapter based on transformation rules
Preprint, Universität Rostock, Rostock, Germany, aug 2008
Behavioral adapters are a way to establish proper interaction between services that have been developed independently. We present a novel approach for specifying such adapters, based on domain-specific transformation rules that reflect the elementary operations that adapters can perform. We show how complex adapters that adhere to these rules can be generated using existing controller generation algorithms. We discuss some example applications, including real-world business processes.
close
close
• Gierds, Christian
Finding Cost-Efficient Adapters
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
close
• ### 2007

• Gierds, Christian

Studienarbeit, oct 2007
close
close

## Glausch, Andreas

### 2007

• 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

• An ASM-Characterization of a Class of Distributed Algorithms
In Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis, Festschrift volume of Lecture Notes in Computer Science, Springer, 2007
close
• Glausch, Andreas
A Semantic Characterization of Elementary Wide-Step ASMs
In Proceedings of the 14th International ASM Workshop, jun 2007
close
• ### 2006

• 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

• How Expressive are Petri Net Schemata?
Susanna Donatelli and P. S. Thiagarajan, editors
In Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, Springer, 2006
Petri net schemata are an intuitive and expressive approach to describe high-level Petri nets. A Petri net schema is a Petri net with edges and transitions inscribed by terms and Boolean expressions, respectively. A concrete high-level net is gained by interpreting the symbols in the inscriptions by a structure. Its semantics can then be described in terms of a transition system. Therefore, the semantics of a Petri Net schema can be conceived as a family of transition systems indexed by structures. In this paper we characterize the expressive power of a general version of Petri net schemata. For that purpose we examine families of transition systems in general and characterize the families as generated by Petri net schemata. It turns out that these families of transition systems can be characterized by simple and intuitive requirements.
close
close

• On the Expressive Power of Unbounded-Nondeterministic Abstract State Machines
Informatik-Berichte, , dec 2006
Conventional computational models assume a symbolical representation of states. Gurevich's Abstract State Machines (ASMs) take a more liberal position: any mathematical structure may serve as a state. Gurevich characterizes the expressive power of sequential ASMs in a non-trivial theorem: he defines the class of \emphsequential algorithms by help of only a few, amazingly general requirements and proves this class to be equivalent to sequential ASMs. Later, this result has been extended to the class of bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among infinitely many alternatives. We define the class of unbounded-nondeterministic algorithms by a conservative extension of Gurevich's original requirements to sequential algorithms. We show that this class is equivalent to unbounded-nondeterministic ASMs.
close
close
• Glausch, Andreas
Distributed Abstract State Machines - Status Report of a Doctoral Thesis
, editors
In Proceedings of the Doctoral Consortium ACSD \& PetriNets 2006, , Turku, Finland, jun 2006
In 1985, Gurevich introduced Abstract State Machines (ASMs) as a computational model more powerful and universal than classical computational models. Since then ASMs have been applied successfully both in theory and practice: On the theoretical side, ASMs evolved to a general basis for the study of different classes of algorithms and their expressive power. On the practical side, ASMs have been extended to a full-fledged design methodology, applied successfully in industry for the specification and analysis of real-world systems. In my doctoral thesis I examine the class of distributed ASMs and study their expressive power. I also intend to develop basic notions of refinement and composition for distributed ASMs.
close
close
• ### 2005

• Glausch, Andreas
Eine Charakterisierung einfacher Petrinetz-Schemata
Karsten Schmidt and Christian Stahl, editors
In , , sep 2005
close
close
• Glausch, Andreas
Varianten des ASM-Theorems
Diplomarbeit, jun 2005
close
close
• ### 2003

• 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

## Kindler, Ekkart

### 2003

• 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

• The Petri Net Markup Language
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 Markup Language (PNML) is an XML-based interchange format for Petri nets. PNML supports any version of Petri net since new Petri net types can be defined by so-called Petri Net Type Definitions (PNTD). In this paper, we present the syntax and the semantics of PNML as well as the principles underlying its design. Moreover, we present an extension called modular PNML, which is a type independent module concept for Petri nets.
close
close
• ### 2001

• Modules in Pictures
volume 61 of Petri Net Newsletter 61, oct 2001
close

• A universal module Concept for Petri nets
Gabriel Juhas und Robert Lorenz, editors
In Proceedings des 8. Workshops AWPN, , oct 2001
close

• 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
• Kindler, Ekkart
Systematische Spezifikation und Verifikation von Konsistenzprotokollen
Habilitationsschrift, aug 2001
close

• A Universal Module Concept for Petri Nets - An Implementation-Oriented Approach
Informatik-Berichte, , apr 2001
close
• ### 2000

• Kindler, Ekkart, Shasha, Dennis
Verifying a Design Pattern for the Fault-Tolerant Execution of Parallel Programs
Technical Report, New York University, Courant Institute of Mathematical Sciences, Computer Science Department, jun 2000
close

• The Petri Net Kernel
, editors
In Tool Demonstrations, 21. ICATPN, , jun 2000
close
• Kindler, Ekkart
Consistency, Causality, Petri Nets, and Automata
Hans-Dieter Burkhard and Ludwik Czaja and Andrzej Skowron and Peter H. Starke, editors
In Workshop Concurrency, Specification \& Programming (CS\&P 2000), oct 2000
close

• Towards a Generic Interchange Format for Petri Nets
Remi Bastide and Jonathan Billington and Ekkart Kindler and Fabrice Kordon and Kjeld H. Mortensen, editors
In Meeting on XML/SGML based Interchange Formats for Petri Nets, 21. ICATPN, , jun 2000
close

• The Petri Net Markup Language
S. Philippi, editors
In , , jun 2000
close

• Cross-talk revisited - What's the problem?
volume 58 of Petri Net Newsletter 58, 2000
close

• Inter-operability of Workshop Applications - Local Criteria for Global Soundness
, editors
In Business Process Management, volume 1806 of Lecture Notes in Computer Science, Springer-Verlag, 2000
close

• Algebraic Nets with Flexible Arcs
Theoretical Computer Science, 2000
close
• Kindler, Ekkart
Serializability, concurrency control and replication control
, editors
In Transactions and Database Dynamics, Proceedings of the 8th International Workshop on Foundations of Models and Languages for Data and Objects, Selected Papers, volume 1773 of Lecture Notes in Computer Science, Springer-Verlag, 2000
close
• ### 1999

• 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

• , editors
In , , jun 1999
close
• Kindler, Ekkart
Serializability, concurrency control and replication control
, editors
In Transactions and Database Dynamics, Proceedings of the Eighth International Workshop on Foundations of Models and Languages for Data and Objects, sep 1999
close
• Kindler, Ekkart
A classification of consistency models
Technical Report, , oct 1999
close

• E. Schnieder, editors
In Entwicklung und Betrieb komplexer Automatisierungssysteme, 6. Fachtagung, Band II, may 1999
close
• Kindler, Ekkart, Aalst, Wil M. P. van der
Liveness, Fairness, and Recurrence
Technical Report, University of Georgia, Department of Computer Science, Athens, USA, apr 1999
close
• 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

• 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
• 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

• Integrating distributed algorithms into distributed systems
volume 37 of Fundamenta Informaticae 37 (3), feb 1999
close

• Application-oriented verification scenarios
1999
close
• ### 1998

• ESTL: A Temporal Logic for Events and States
, editors
In Application and Theory of Petri Nets, 19th International Conference, ICATPN '98, Proceedings, volume 1420 of Lecture Notes in Computer Science, Springer-Verlag, jun 1998
close
• Kindler, Ekkart
The interplay of transaction models and memory models
, editors
In Proceedings of the Third International Conference on Integrated Design and Process Technology, volume 2 of IDPT, Society for Design and Process Science, jul 1998
close

• Flexibility in Algebraic Nets
, editors
In Application and Theory of Petri Nets, 19th International Conference, ICATPN '98, Proceedings, volume 1420 of Lecture Notes in Computer Science, Springer-Verlag, jun 1998
close
• Kindler, Ekkart
Database theory - Petri net theory - Workflow theory
Informatik-Berichte, , may 1998
close
• Baar, Thomas, Kindler, Ekkart
Einsatz von ILF und DAWN zur Verifikation verteilter Algorithmen - Eine Vorstudie
Informatik-Berichte, , mar 1998
close

• Proving Correctness of Distributed Algorithms Using High-Level Petri Nets - A Case Study
In First International Conference on Application of Concurrency to System Design (ACSD'98), IEEE Computer Society Press, Fukushima, Japan, mar 1998
close
• Hauptmann, Jens, Hohberg, Bodo, Kindler, Ekkart, Schwenzer, Ines, Weber, Michael
Der Petrinetz-Kern - Dokumentation der Anwendungs-Schnittstelle
Informatik-Berichte, , feb 1998
close
• ### 1997

• Kindler, Ekkart
Inhibitor arcs: A philosophical view
volume 53 of Petri Net Newsletter 53, oct 1997
close

• A temporal logic for events and states in Petri nets
B. Farwer and D. Moldt and M.-O. Stehr, editors
In Petri Nets in System Engineering (PNSE'97) Modelling, Verification, and Validation, Fachberichte, , sep 1997
close

• ESTL: A temporal logic for events and states
Informatik-Berichte, , nov 1997
close

• Flexibility in algebraic nets
Informatik-Berichte, , nov 1997
close

• DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen
Informatik-Berichte, , dec 1997
close
• , Kindler, Ekkart, Oberweis, Andreas

Informatik-Berichte, , sep 1997
close
• Kindler, Ekkart
A compositional partial order semantics for Petri net components
, editors
In Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN '97, Proceedings, volume 1248 of Lecture Notes in Computer Science, Springer-Verlag, jun 1997
close

• Verification of Distributed Algorithms with Algebraic Petri Nets
, editors
In Foundations of Computer Science: Potential - Theory - Cognition, volume 1337 of Lecture Notes in Computer Science, Springer-Verlag, 1997
close
• Kindler, Ekkart
Der Petrinetz-Kern: Ein Traum wird wahr
1997
close

• Petri Net Based Verification of Distributed Algorithms: An Example
volume 9 of Formal Aspects of Computing 9 (4), Springer-Verlag, 1997
close

• Mutex Needs Fairness
volume 62 of Information Processing Letters 62 (1), ELSEVIER, 1997
close

• Proving correctness of distributed algorithms: A Petrinet approach
Bericht, , feb 1997
close
• Fricke, Olaf, Borusan, Alexander, Vesper, Tobias, Kindler, Ekkart
Verifikation im Vorgehensmodell anhand eines Beispiels
1997
close
• ### 1996

• Memorandum: Petrinetzmodelle zur Verifikation verteilter Algorithmen
Informatik-Berichte, , aug 1996
close

• Der Traum von einem universellen Petrinetz-Werkzeug - Der Petrinetz-Kern
, editors
In , , oct 1996
close

• , editors
In , , oct 1996
close

• Algebraic System Nets for Modelling Distributed Algorithms
volume 51 of Petri Net Newsletter 51, nov 1996
close
• Kindler, Ekkart
A Specification and Verification Method for Caching Protocols
, editors
In Formal Methods for Concurrency, GI-Kolloquium, Fachberichte der TU Dresden, , jul 1996
close

• Arc-Typed Petri Nets
J. Billington and Wolfgang Reisig, editors
In Application and Theory of Petri Nets 1996, volume 1091 of Lecture Notes in Computer Science, Springer-Verlag, jun 1996
close
• Kindler, Ekkart
A Compositional Partial Order Semantics for Petri Net Components
SFB-Bericht, , mar 1996
close
• Kindler, Ekkart, Listl, Andreas, Walter, Rolf
A Specification Method for Transaction Models with Data Replication
Informatik-Berichte, , mar 1996
close

• Petri Net Based Verification of Distributed Algorithms: An Example
Informatik-Berichte, , may 1996
close

• Distributed Algorithms for Networks of Agents.
In Petri Nets (2), 1996
close

## Lohmann, Niels

### 2010

• 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

• A Graphical User Interface for Service Adaptation
Martin Schwarick and Monika Heiner, editors
In Proceedings of the 17th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2010, Cottbus, Germany, October 07-08, 2010, volume 643 of CEUR Workshop Proceedings, CEUR-WS.org, oct 2010
close
• ### 2009

• 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
• 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
• 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
• Lohmann, Niels, Verbeek, Eric, Dijkman, Remco
Petri Net Transformations for Business Processes -- A Survey
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 Process-Aware Information Systems, business processes are often modeled in an explicit way. Roughly spoken, the available business process modeling languages can be divided into two groups. Languages from the first group are preferred by academic people but shunned by business people, and include Petri nets and process algebras. These academic languages have a proper formal semantics, which allows the corresponding academic models to be verified in a formal way. Languages from the second group are preferred by business people but disliked by academic people, and include BPEL, BPMN, and EPCs. These business languages often lack any proper semantics, which often leads to debates on how to interpret certain business models. Nevertheless, business models are used in practice, whereas academic models are hardly used. To be able to use, for example, the abundance of Petri net verification techniques on business models, we need to be able to transform these models to Petri nets. In this paper, we investigate a number of Petri net transformations that already exist. For every transformation, we investigate the transformation itself, the constructs in the business models that are problematic for the transformation and the main applications for the transformation.
close
close
• ### 2008

• Lohmann, Niels, Kleine, Jens
Fully-automatic Translation of Open Workflow Net Models into Human-readable Abstract BPEL Processes
Thomas Kühne and Wolfgang Reisig and Friedrich Steimann, editors
In Modellierung 2008, 12.-14. März 2008, Berlin, Proceedings, volume P-127 of Lecture Notes in Informatics (LNI), GI, mar 2008
On the one hand, Petri net models have a successful history in the modeling, simulation, and verification of workflows and business processes. On the other hand, BPEL is the de facto standard for describing executable Web service-based business processes. With abstract BPEL processes, BPEL can also be used as modeling language. However, being a complicated language with many syntactic constraints, abstract BPEL processes impede a straightforward modeling. In this paper, we introduce a fully-automatic translation of Petri net models into abstract BPEL processes which can be refined to executable BPEL processes. This approach combines strengths of Petri nets in modeling and verification with the ability to execute BPEL processes. Furthermore, it completes the Tools4BPEL framework to synthesize BPEL processes which are correct by design.
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
• 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
Correcting Deadlocking Service Choreographies Using a Simulation-Based Graph Edit Distance
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
Many work has been conducted to analyze service choreographies to assert manyfold correctness criteria. While errors can be detected automatically, the correction of defective services is usually done manually. This paper introduces a graph-based approach to calculate the minimal edit distance between a given defective service and synthesized correct services. This edit distance helps to automatically fix found errors while keeping the rest of the service untouched. A prototypic implementation shows that the approach is applicable to real-life services.
close
close
• Lohmann, Niels
Why does my service have no partners?
Roberto Bruni and Karsten Wolf, editors
In Web Services and Formal Methods, Fifth International Workshop, WS-FM 2008, Milan, Italy, September 4-5, 2008, Proceedings, Lecture Notes in Computer Science, Springer-Verlag, sep 2008
Controllability is a fundamental correctness criterion for interacting service models. A service model is controllable if there exists a partner service such that their composition is free of deadlocks and livelocks. Whereas controllability can be automatically decided, the existing decision algorithm gives no information about the reasons of why a service model is uncontrollable. This paper introduces a diagnosis framework to find these reasons which can help to fix uncontrollable service models.
close
close
• Lohmann, Niels
A Feature-Complete Petri Net Semantics for WS-BPEL 2.0
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
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
• 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
Decompositional Calculation of Operating Guidelines Using Free Choice Conflicts
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
close
• Lohmann, Niels, Kopp, Oliver, Leymann, Frank, Reisig, Wolfgang
Analyzing BPEL4Chor: Verification and Participant Synthesis
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
Choreographies offer means to capture global interactions between business processes of different partners. BPEL4Chor has been introduced to describe these interactions using BPEL. Currently, there are no formal methods available to verify BPEL4Chor choreographies. In this paper, we present how BPEL4Chor choreographies can be completely verified using Petri nets. A case study undermines that our verification techniques scale. Additionally, we show how the verification techniques can be used to generate a stub process for a partner taking part in a choreography. This is especially useful when the behavior of one participant is intended to follow the corresponding requirements of the other participants. Thus, the missing participant behavior can be generated and the error-prone design of that participant can be skipped.
close
close
• ### 2007

• Services as a Paradigm of Computation
Cliff B. Jones and Zhiming Liu and Jim Woodcock, editors
In Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj\orner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, volume 4700 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.
close
close
• 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
• Reisig, Wolfgang, Wolf, Karsten, Bretschneider, Jan, Kaschner, Kathrin, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
Challenges in a Service-Oriented World
volume 70 of ERCIM News 70, jul 2007
Interacting services raise a number of new software engineering challenges. To meet these challenges, the behaviour of the involved services must be considered. We present results regarding the behaviour of services in isolation, the interaction of services in choreographies, the exchangeability of a service, and the synthesis of desired partner services.
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
• Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
Operating Guidelines for Finite-State Services
Jetty Kleijn and Alex Yakovlev, editors
In 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007, Proceedings, volume 4546 of Lecture Notes in Computer Science, Springer-Verlag, 2007
We study services modeled as open workflow nets (oWFN) and describe their behavior as service automata. Based on service automata, we introduce the concept of an operating guideline, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to properly interact (in this paper: deadlock-freely and with limited communication) with an oWFN N. It can be executed thus forming a properly interacting partner of N, or it can be used to support service discovery. An operating guideline for N is a particular service automaton S that is enriched with Boolean annotations. S interacts properly with the service automaton Prov, representing the behavior of N , and is able to simulate every other service that interacts properly with Prov . The attached annotations give complete information about whether or not a simulated service interacts properly with Prov, too.
close
close
• Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
Behavioral Constraints for Services
Informatik-Berichte, Humboldt-Universität zu Berlin, may 2007
Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be filtered'' yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.
close
close
• Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
Behavioral Constraints for Services
Gustavo Alonso and Peter Dadam and Michael Rosemann, editors
In Business Process Management, 5th International Conference, BPM 2007, Brisbane, Australia, September 24-28, 2007, Proceedings, volume 4714 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be "filtered" yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.
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
• ### 2006

• 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
• Kopp, Oliver, Frenkler, Carsten, Lohmann, Niels

In Forschungsoffensive ''Software Engineering 2006'', Statuskonferenz, 26.-28. Juni 2006, , jul 2006
close
• Lohmann, Niels
A Local Cut-off Criterion for Unfoldings of Safe Petri Nets
, editors
In Proceedings of the Doctoral Consortium ACSD \& Petri Nets 2006, , Turku, Finland, jun 2006
Finite prefixes of branching processes are a compact way to represent the state space of finite safe systems. McMillan in [1] formulated a cut-off criterion stating under which conditions the (usually infinite) maximal branching process can be truncated without loosing reachable markings. However, this criterion depends on the reachable markings itself and thus suffers the state explosion problem. In this work, we propose local cut-off criteria that base on partial markings.
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
• 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
• ### 2005

• Lohmann, Niels

Diplomarbeit, sep 2005
close
close
• Lohmann, Niels

Studienarbeit, jun 2005
close
close

## Müller, Richard

### 2014

• Duske, Kristian, Müller, Richard, Prüfer, Robert, Stöhr, Daniel
A BPMN Model of the Charite Stroke Treatment Process
Informatik-Berichte, Humboldt-Universität zu Berlin, 2014
close
• ### 2013

• Müller, Richard, Stahl, Christian, Aalst, Wil M. P. van der, Westergaard, Michael
Service Discovery from Observed Behavior while Guaranteeing Deadlock Freedom in Collaborations
Basu, Samik and Pautasso, Cesare and Zhang, Liang and Fu, Xiang, editors
In Service-Oriented Computing, volume 8274 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2013
close
• Müller, Richard, Stahl, Christian, Vogler, Walter
Undecidability of accordance for open systems with unbounded message queues
BPM Center Report, BPMcenter.org, 2013
close
• Vogler, Walter, Stahl, Christian, Müller, Richard
Trace- and Failure-Based Semantics for Bounded Responsiveness
Canal, Carlos and Villari, Massimo, editors
In Advances in Service-Oriented and Cloud Computing, volume 393 of Communications in Computer and Information Science, Springer Berlin Heidelberg, 2013
close
• Vogler, Walter, Stahl, Christian, Müller, Richard
Trace- and Failure-Based Semantics for Responsiveness
BPM Center Report, BPMcenter.org, 2013
close
• Müller, Richard, Stahl, Christian, Aalst, Wil M. P. van der, Westergaard, Michael
Service Discovery from Observed Behavior While Guaranteeing Deadlock Freedom in Collaborations
BPM Center Report, BPMcenter.org, 2013
close
• ### 2012

• Duske, Kristian, Müller, Richard
A Survey on Approaches for Timed Services
Andreas Schönberger and Oliver Kopp and Niels Lohmann, editors
In Proceedings of the 4th Central-European Workshop on Services and their Composition, ZEUS-2012, Bamberg, Germany, February 23-24, 2012, volume 847 of CEUR Workshop Proceedings, CEUR-WS.org, 2012
close
• Müller, Richard, Aalst, Wil M. P. van der, Stahl, Christian
Conformance Checking of Services Using the Best Matching Private View
In Proceedings of the 9th International Workshop on Web Services and Formal Methods, WS-FM 2012 September 6-7, 2012, Tallinn, Estonia, 2012
close
• Vogler, Walter, Stahl, Christian, Müller, Richard
A Trace-Based Semantics for Responsiveness
Jens Brandt and Keijo Heljanko, editors
In Proceedings of the 12th International Conference on Application of Concurrency to System Design, ACSD 2012, Hamburg, Germany, June 27-29, 2012, IEEE, 2012
close

• Deciding the Precongruence for Deadlock Freedom Using Operating Guidelines
, editors
In Proceedings of the 2nd International Workshop on Petri Nets Compositions, CompoNet'12, Hamburg, Germany, June 25-26, 2012, volume 853 of CEUR Workshop Proceedings, CEUR-WS.org, jun 2012
close
• ### 2011

• Müller, Richard, Rogge-Solti, Andreas
BPMN for Healthcare Processes
Daniel Eichhorn and Agnes Koschmider and Huayu Zhang, editors
In Proceedings of the 3rd Central-European Workshop on Services and their Composition, ZEUS 2011, Karlsruhe, Germany, February 21--22, 2011, volume 705 of CEUR Workshop Proceedings, CEUR-WS.org, 2011
close
• ### 2010

• Müller, Richard
Formal Characterisation of Partners of an Open Net
Diplomarbeit, jun 2010
close
• Müller, Richard
On the Notion of Deadlocks in Open Nets
Martin Schwarick and Monika Heiner, editors
In Proceedings of the 17th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2010, Cottbus, Germany, October 07-08, 2010, volume 643 of CEUR Workshop Proceedings, CEUR-WS.org, oct 2010
close
• ### 2009

• Müller, Richard
Strukturelle Reduktion von Verhaltensadaptern
Studienarbeit, dec 2009
close

## Martens, Axel

### 2007

• Moser, Simon, Martens, Axel, Görlach, Katharina, Amme, Wolfram, Godlinski, Artur
Advanced Verification of Distributed WS-BPEL Business Processes Incorporating CSSA-based Data Flow Analysis
In IEEE International Conference on Services Computing (SCC 2007), 2007
The Business Process Execution Language for Web Services WS-BPEL provides an technology to aggregate encapsulated functionalities for defining high-value Web services. For a distributed application in a B2B interaction, the partners simply need to expose their provided functionality as BPEL processes and compose them. Verifying such distributed web service based systems has been a huge topic in the research community lately - cf. [4] for a good overview. However, in most of the work on analyzing properties of interacting Web Services, especially when backed by stateful implementations like WS-BPEL, the data flow present in the implementation is widely neglected, and the analysis focusses on control flow only. This might lead to false-positive analysis results when searching for design weaknesses and errors, e.g. analyzing the controllability [14] of a given BPEL process. In this paper, we present a method to extract data flow information by constructing a CSSA representation and detecting data dependencies that effect communication behavior. Those discovered dependencies are used to construct a more precise formal model of the given BPEL process and hence to improve the quality of analysis results.
close
close
• ### 2005

• Martens, Axel
Process Oriented Discovery of Business Partners
In Proceedings of 7th Intl. Conference on Enterprise Information Systems (ICEIS'05), Vol 3, INSTICC, Miami, Florida, may 2005
Emerging technologies and industrial standards in the field of Web services enable a much faster and easier cooperation of distributed partners. With the increasing number of enterprises that offer specific functionality in terms of Web services, discovery of matching partners becomes a serious issue. At the moment, discovery of Web services generally is based on meta-information (e. g. name, business category) and some technical aspects (e. g. interface, protocols). But, this selection might be to coarse grained for dynamic application integration, and there is much more information available. This paper describes a method to discover business partners based on the comparison of their behavior ? specified in terms of their published Web service process models.
close
close
• Martens, Axel
Analyzing Web Service based Business Processes
Maura Cerioli, editors
In Proceedings of Intl. Conference on Fundamental Approaches to Software Engineering (FASE'05), Part of the 2005 European Joint Conferences on Theory and Practice of Software (ETAPS'05), volume 3442 of Lecture Notes in Computer Science, Springer-Verlag, Edinburgh, Scotland, apr 2005
This paper is concerned with the application of Web services to distributed, cross-organizational business processes. In this scenario, it is crucial to answer the following questions: Do two Web services fit together in a way such that the composed system is deadlock-free? - the question of compatibility. Can one Web service be replaced by another while the remaining components stay untouched? - the question of equivalence. Can we reason about the soundness of one given Web service without considering the actual environment it will by used in? This paper defines the notion of usability - an intuitive and locally provable soundness criterion for a given Web services. Based on this notion, this paper demonstrates how the other questions could be answered. The presented method is based on Petri nets, because this formalism is widely used for modeling and analyzing business processes. Due to the existing Petri net semantics for BPEL4WS - a language that is in the very act of becoming the industrial standard for Web service based business processes - the results are directly applicable to real world examples.
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
• Schlingloff, Bernd-Holger, Martens, Axel, Schmidt, Karsten
Modeling and Model Checking Web Services
volume 126 of Electronic Notes in Theoretical Computer Science: Issue on Logic and Communication in Multi-Agent Systems 126, Elsevier, mar 2005
We give an overview on web services and the web service technology stack. We then show how to build Petri net models of web services formulated in the specification language BPEL4WS. We define an abstract correctness criterion for these models and study the automated verification according to this criterion. Finally, we relate correctness of web service models to the model checking problem for alternating temporal logics.
close
close
• Martens, Axel
Consistency between Executable and Abstract Processes
In Proceedings of Intl. IEEE Conference on e-Technology, e-Commerce, and e-Services (EEE'05), IEEE Computer Society Press, Hong Kong, mar 2005
Process models play an all-important role in the development of cross-organizational business processes. 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 describes an approach to prove this property automatically.
close
close
• ### 2004

• 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
• Martens, Axel
Analysis and re-engineering of Web Services
In Proceedings of 6th International Conference on Enterprise Information Systems (ICEIS'04), Porto, Portugal, 2004
To an increasing extend software systems are integrated across the borders of individual enterprises. The Web Service approach provides group of technologies to describe components and their composition, based on well established protocols. Focused on business processes, one Web Service implements a local subprocess. A distributed business processes is implemented by the composition a set of communicating Web Services. At the moment, there are various modeling languages under development to describe the internal structure of one Web Service (e. g. Business Process Execution Language for Web Services BPEL4WS (BEA et al., 2002a)) and the choreography of a set of Web Services (e. g. Web Service Choreography Interface WSCI (BEA et al., 2002b)). Nevertheless, there is a need for methods for stepwise construction and verification of such components. This paper abstracts from concrete syntax of any proposed language definition. Instead, we apply Petri nets to model Web Services. Thus, we are able to reason about essential properties, e. g. usability of a Web Service - our notion of a quality criterion. Based on this framework, we present an algorithm to analyze a given Web Service and to transfer a complex process model into a appropriate model of a Web Service.
close
close
• ### 2003

• Martens, Axel
Compatibility of Web Services
In , sep 2003
To an increasing extend business processes run across the borders of individual enterprises. Thus, there is a need to map each local subprocess into a self-contained component; a distributed business process arises from composition of such component via standardized communication protocols. The Web service approach provides a standardized, platform independent and widely accepted concept of components and composition for distributed systems of all kinds. This approach comes along together with group of technologies to describe precisely the structure of one Web service and the composition of a set of Web services. Although the technological basement is given, there is a lot of open questions, e. g. semantic compatibility of two Web services. This paper abstracts from concrete syntax of any proposed language definition. Instead, we apply Petri nets to model Web services. Thus, we are able to reason about essential properties, e. g. usability of a Web service - our notion of a quality criterion. Based on this framework, we discuss and define a criterion for semantic compatibility of Web services.
close
close
• Weber, Herbert, Ehrig, Hartmut, Reisig, Wolfgang, Borusan, Alexander, Lembke, Sabine, Dehnert, Juliane, Weber, Michael, Martens, Axel, Padberg, Julia, Ermel, Claudia, Qemali, A.
The Petri Net Baukasten of the DFG Forschergruppe PETRI NET TECHNOLOGY
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
In the long history of Petri nets a universe of Petri nets has evolved consisting of an enormously rich theory, a wide variety of tools, and numerous successful applications and case studies in various application domains. This vast variety is not any more handable for anyone working with Petri nets, which results in the strong need of a structured access to Petri nets. This structured access has been the main aim of the DFG-Forschergruppe PETRI NET TECHNOLOGY, which has developed the so-called Petri Net Baukasten for this purpose. It is designed to support Petri net experts, application developers and tool developers alike in their specific work with Petri nets. This paper presents an overview of the concepts, initial and 2nd installment of the Petri Net Baukasten, which have been presented at the 1st and 2nd International Colloquium on Petri Net Technologies for Modelling Communication Based Systems in 1999 and 2001, respectively.
close
close
• Martens, Axel
On Usability of Web Services
, editors
In Proceedings of 1st Web Services Quality Workshop (WQW 2003), Rome, Italy, 2003
This paper is concerned with the application of Web services to distributed, cross-organizational business processes. Web services provide a platform independent concept of components and composition. Thus, they seem to be a proper technology to cover the heterogenous structures within distributed business processes: One Web service realizes a local subprocess. A distributed business process is realized by the composition of a set of Web services. Although the technological basement is given, there is a lot of open questions: Do two Web services fit together in a way, that the composition yields a deadlock-free system? - the question of compatibility. Can one Web service be exchanged by another within a composed system without running into problems? - the question of equivalence. Can we reason about the quality of one given Web service without considering the environment it will by used in? In this paper we present the notion of usability - our quality criterion of a Web service. This criterion is intuitive and can be easily proven locally. Moreover, this notion allows to answer the other questions mentioned above. The approach and the results presented in this paper are taken from a larger framework for modeling and analyzing business processes by help of Web services published in my PhD thesis [9].
close
close
• Martens, Axel
On Compatibility of Web Services
, editors
volume 65 of Petri Net Newsletter 65, 2003
close
• Martens, Axel

Dissertation, 2003
close
• ### 2001

• Martens, Axel
Modeling Workflow in Virtual Enterprises
Herbert Weber and Hartmut Ehrig and Wolfgang Reisig, editors
In Proc. of 2nd Int. Coll. on Petri Net Technologies for Modelling Communication Based Systems, DFG Research Group Petri Net Technology, 2001
close
• ### 2000

• Inter-operability of Workshop Applications - Local Criteria for Global Soundness
, editors
In Business Process Management, volume 1806 of Lecture Notes in Computer Science, Springer-Verlag, 2000
close

• Cross-talk revisited - What's the problem?
volume 58 of Petri Net Newsletter 58, 2000
close
• ### 1999

• Battke, Anne, Borusan, Alexander, Dehnert, Juliane, Ehrig, Hartmut, Ermel, Claudia, Gajewsky, Maike, Hoffmann, Kathrin, Hohberg, Bodo, , Lembke, Sabine, Martens, Axel, Padberg, Julia, Reisig, Wolfgang, Vesper, Tobias, Weber, Herbert, Weber, Michael
Petrinetz-Technologie: Initial Realization of the Petri Net Baukasten
Informatik-Berichte, , oct 1999
close

• , editors
In , , jun 1999
close
• ### 1997

• Martens, Axel
Software-Engineering von Workflow-Applikationen mit Petrinetzen
Diplomarbeit, aug 1997
close

## Massuthe, Peter

### 2010

• 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
• ### 2009

• Massuthe, Peter
Operating Guidelines for Services
Dissertation, Apr 2009
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
• ### 2008

• Massuthe, Peter, Serebrenik, Alexander, Sidorova, Natalia, Wolf, Karsten
Can I find a Partner?
Preprint, , Rostock, Germany, mar 2008
We study open nets as Petri net models of web services, with a link to the practically relevant language WS-BPEL. For those nets, we investigate the problem of serviceableness which we consider as fundamental as the successful notion of soundness for workflow nets, i.e. Petri net models of business processes and workflows. While we could give algorithmic solutions to the serviceableness problem for subclasses of open nets in earlier work, this article shows that the problem is in general undecidable.
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

• 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
• 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

• Fiona: A Tool to Analyze Interacting Open 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
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
• ### 2007

• Services as a Paradigm of Computation
Cliff B. Jones and Zhiming Liu and Jim Woodcock, editors
In Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj\orner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, volume 4700 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.
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
• 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
• Reisig, Wolfgang, Wolf, Karsten, Bretschneider, Jan, Kaschner, Kathrin, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
Challenges in a Service-Oriented World
volume 70 of ERCIM News 70, jul 2007
Interacting services raise a number of new software engineering challenges. To meet these challenges, the behaviour of the involved services must be considered. We present results regarding the behaviour of services in isolation, the interaction of services in choreographies, the exchangeability of a service, and the synthesis of desired partner services.
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
• Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
Behavioral Constraints for Services
Informatik-Berichte, Humboldt-Universität zu Berlin, may 2007
Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be filtered'' yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.
close
close
• Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
Behavioral Constraints for Services
Gustavo Alonso and Peter Dadam and Michael Rosemann, editors
In Business Process Management, 5th International Conference, BPM 2007, Brisbane, Australia, September 24-28, 2007, Proceedings, volume 4714 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be "filtered" yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.
close
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
• Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
Operating Guidelines for Finite-State Services
Jetty Kleijn and Alex Yakovlev, editors
In 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007, Proceedings, volume 4546 of Lecture Notes in Computer Science, Springer-Verlag, 2007
We study services modeled as open workflow nets (oWFN) and describe their behavior as service automata. Based on service automata, we introduce the concept of an operating guideline, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to properly interact (in this paper: deadlock-freely and with limited communication) with an oWFN N. It can be executed thus forming a properly interacting partner of N, or it can be used to support service discovery. An operating guideline for N is a particular service automaton S that is enriched with Boolean annotations. S interacts properly with the service automaton Prov, representing the behavior of N , and is able to simulate every other service that interacts properly with Prov . The attached annotations give complete information about whether or not a simulated service interacts properly with Prov, too.
close
close
• ### 2006

• 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, 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
• 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, 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
• 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
• ### 2005

• 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
• 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
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, 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, 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
• Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
An Operating Guideline Approach to the SOA
In 2nd South-East European Workshop on Formal Methods 2005 (SEEFM05), Ohrid, Republic of Macedonia, 2005
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
• ### 2004

• Massuthe, Peter
Verfeinerungstechniken der Temporal Logic of Distributed Actions TLDA
Diplomarbeit, mar 2004
close
close
• ### 2003

• Massuthe, Peter
Parallele Komposition in TLA
Studienarbeit, sep 2003
close
close

## Parnjai, Jarungjit

### 2011

• Mooij, Arjan, Parnjai, Jarungjit, Stahl, Christian, Voorhoeve, Marc
Constructing Replaceable Services Using Operating Guidelines and Maximal Controllers
Bravetti, Mario and Bultan, Tevfik, editors
In Web Services and Formal Methods, volume 6551 of Lecture Notes in Computer Science, Springer Berlin / Heidelberg, 2011
close
• Parnjai, Jarungjit
Filtering Undesirable Service Substitution Behaviors using Filtering Guidelines
Daniel Eichhorn and Agnes Koschmider and Huayu Zhang, editors
In Proceedings of the 3rd Central-European Workshop on Services and their Composition, ZEUS 2011, Karlsruhe, Germany, February 21--22, 2011, volume 705 of CEUR Workshop Proceedings, CEUR-WS.org, 2011
close
• ### 2009

• 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

## Peuker, Sibylle

### 2001

• Peuker, Sibylle
Halbordnungsbasierte Verfeinerung zur Verifikation verteilter Algorithmen
Dissertation, jul 2001
close
close
• Peuker, Sibylle
Property Preserving Transition Refinement with Concurrent Runs: An Example
In 2nd International Conference on Application of Concurrency to System Design (ACSD 2001), IEEE Computer Society, 2001
close
• ### 2000

• Peuker, Sibylle
Property Preserving Transition Refinement with Concurrent Runs
Informatik-Berichte, , jul 2000
close
• ### 1999

• Peuker, Sibylle
Phased Decomposition of Distributed Algorithms
Informatik-Berichte, , apr 1999
close

• Integrating distributed algorithms into distributed systems
volume 37 of Fundamenta Informaticae 37 (3), feb 1999
close
• ### 1997

• DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen
Informatik-Berichte, , dec 1997
close
• Peuker, Sibylle
Invariant property preserving extensions of elementary Petri nets
1997
close

## Prüfer, Robert

### 2014

• Duske, Kristian, Müller, Richard, Prüfer, Robert, Stöhr, Daniel
A BPMN Model of the Charite Stroke Treatment Process
Informatik-Berichte, Humboldt-Universität zu Berlin, 2014
close

• Introducing Configurability into Scenario-Based Specification of Business Processes
In ZEUS, 2014
close
• ### 2012

• Data and Abstraction for Scenario-Based Modeling with Petri Nets
In Petri Nets, 2012
close
• ### 2010

• Prüfer, Robert
Optimierung der Sweep-Line-Methode
Diplomarbeit, apr 2010
close
• Prüfer, Robert
On Optimizing the Sweep-Line Method
Martin Schwarick and Monika Heiner, editors
In Proceedings of the 17th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2010, Cottbus, Germany, October 07-08, 2010, volume 643 of CEUR Workshop Proceedings, CEUR-WS.org, oct 2010
close
• ### 2009

• Prüfer, Robert
Optimierung der Sweeplinemethode
Studienarbeit, mar 2009
close

## Reisig, Wolfgang

### 2018

• Reisig, Wolfgang
Associative composition of components with double-sided interfaces
submitted to Acta Informatica, 2018
close
• ### 2017

• Brandt, Jörgen, Reisig, Wolfgang, Leser, Ulf
Computation semantics of the functional scientific workflow language Cuneiform
volume 27 of Journal of Functional Programming 27, Cambridge University Press, 2017
close
• Reisig, Wolfgang
Associative Composition of Reactive Systems
to appear, 2017
close
• ### 2015

• Certifcation of Distributed Algorithms Solving Problems with Optimal Substructure
In Software Engineering and Formal Methods, 2015
close
• ### 2013

• Reisig, Wolfgang
Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies
Springer, 2013
close
• Reisig, Wolfgang
The Synthesis Problem
volume 7 of T. Petri Nets and Other Models of Concurrency 7, 2013
close
• Reisig, Wolfgang, Rozenberg, Grzegorz, Thiagarajan, P. S.
In Memoriam: Carl Adam Petri
volume 7 of T. Petri Nets and Other Models of Concurrency 7, 2013
close
• Reisig, Wolfgang
Remarks on Egon Börger: "Approaches to model business processes: a critical analysis of BPMN, workflow patterns and YAWL, SOSYM 11: 305-318"
volume 12 of Software and System Modeling 12 (1), 2013
close
• ### 2012

• Reisig, Wolfgang
A Fresh Look at Petri Net Extensions
In Software Service and Application Engineering, 2012
close
• ### 2011

• Reisig, Wolfgang
Petri Nets
Ina Koch and Wolfgang Reisig and Falk Schreiber, editors
In Modeling in Systems Biology, The Petri Net Approach, Springer, 2011
close
• Reisig, Wolfgang
Rezension - Die vergessene Revolution oder die Wiedergeburt des antiken Wissens
volume 34 of Informatik Spektrum, Springer 34, december 2011
close
• ### 2010

• Reisig, Wolfgang
Petrinetze: Modellierungstechnik, Analysemethoden, Fallstudien
Leitfäden der Informatik, Vieweg+Teubner, 15 July 2010
close
• Reisig, Wolfgang
50 Jahre Verhaltensmodellierung: Vom Modellieren mit Programmen zum Programmieren mit Modellen
In Modellierung, 2010
close
• Blass, Andreas, Dershowitz, Nachum, Reisig, Wolfgang
Yuri, Logic, and Computer Science
In Fields of Logic and Computation, 2010
close
• ### 2009

• Reisig, Wolfgang
The Universal Net Composition Operator
Forschungsbericht, Humboldt-Universität zu Berlin, jan 2009
Petri nets are frequently composed of given nets. Literature suggests a lot of different composition operators, for different purposes and different classes of Petri nets. Formal definitions are frequently surprisingly technical, not matching the intuitively very elegant composition of Petri nets in the framework of their graphical representation. This paper suggests the universal net composition operator. This operator allows to specify any specific composition variant by very simple means, leaving all technical details to the operator, where they are treated once and for all. General properties of composition, in particular associativity, are inherited by all instantiations of the operator. We show the practical advantage of the universal composition operator by means of a lot of examples from various areas of Petri nets.
close
close
• Brauer, Wilfried, Reisig, Wolfgang
Carl Adam Petri and ''Petri Nets''
Erol Gelenbe and Jean-Pierre Kahane (Hrsg.), editors
volume 3 of Advances in Computer Science and Engineering: Texts, Fundamental Concepts in Computer Science 3, Imperial College Press, 2009
close
• Reisig, Wolfgang
Simple Composition of Nets
Giuliana Franceschinis and Karsten Wolf, editors
In Proceedings of the 30th International Conference on Petri Nets and Other Models Of Concurrency, volume 5606 of Lecture Notes in Computer Science, Springer-Verlag, Paris, France, jun 2009
close
• ### 2008

• 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
Towards a Theory of Services
Roland Kaschek, Christian Kop, Claudia Steinberger, Guenther Fliedl (Eds.), editors
In Information Systems and e-Business Technologies, 2nd International United Information Systems Conference, UNISCON 2008, Springer-Verlag, Klagenfurt, Austria, apr 2008
Service-oriented Computing and Service-oriented Architectures aspire to better exploit existing middleware technologies. To this end, a more flexible, platform independent software design methodology is suggested, to develop rapid, low cost, interoperable, evolving and massively distributed software systems. Intended application areas include electronic commerce, information systems, supply chain control, and many other areas. Time is ripe to underpin this effort by theoretically well-founded concepts to model services, and to analyze such models. In this paper we suggest first proposals and principles for a comprehensive theory of services.
close
close
• Reisig, Wolfgang
The computable kernel of Abstract State Machines
volume 409 of Theoretical Computer Science 409, aug 2008
Abstract State Machines (ASMs) were introduced as "a computation model that is more powerful and more universal than standard computation models", by Yuri Gurevich in 1985. ASMs gained much attention as a specification method. It is extremely flexible because any mathematical structure may serve as a state. Gurevich characterized the expressive power of ASMs in terms of intuitively convincing postulates. The core result of this paper shows that the next-state function M of an Abstract State Machine M can be described on a symbolic level, notwithstanding the generality of the model: The successor state M(S) of a state S is fully specified by the equivalence ~s induced by S on the terms over the signature of M. Consequently, M(S) is computable in case ~s is decidable. Furthermore, this result implies a notion of computability for general structures, e.g. for algorithms operating on real numbers.
close
close
• Reisig, Wolfgang
The Scholten/Dijkstra Pebble Game Played Straightly, Distributely, Online and Reversed
volume 4800 of Pillars of Computer Science, LNCS 4800, Springer-Verlag, 2008
The Scholten/Dijkstra "Pebble Game" is re-examined. We show that the algorithm lends itself to a distributed as well as an online version, and even to a reversed variant. Technically this is achieved by exploiting the local and the reversible nature of Petri Net transitions. Furthermore, these properties allow to retain the verification arguments of the algorithm.
close
close
• Lohmann, Niels, Kopp, Oliver, Leymann, Frank, Reisig, Wolfgang
Analyzing BPEL4Chor: Verification and Participant Synthesis
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
Choreographies offer means to capture global interactions between business processes of different partners. BPEL4Chor has been introduced to describe these interactions using BPEL. Currently, there are no formal methods available to verify BPEL4Chor choreographies. In this paper, we present how BPEL4Chor choreographies can be completely verified using Petri nets. A case study undermines that our verification techniques scale. Additionally, we show how the verification techniques can be used to generate a stub process for a partner taking part in a choreography. This is especially useful when the behavior of one participant is intended to follow the corresponding requirements of the other participants. Thus, the missing participant behavior can be generated and the error-prone design of that participant can be skipped.
close
close
• ### 2007

• Services as a Paradigm of Computation
Cliff B. Jones and Zhiming Liu and Jim Woodcock, editors
In Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj\orner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, volume 4700 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.
close
close
• Hohberg, Bodo, Reisig, Wolfgang, Wu, Bixia
Entwurf und Verifikation nachrichtenbasierter verteilter Algorithmen durch verteilende Verfeinerung
Informatik-Berichte, Humboldt-Universität zu Berlin, 2007
close
close
• Reisig, Wolfgang, Wolf, Karsten, Bretschneider, Jan, Kaschner, Kathrin, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
Challenges in a Service-Oriented World
volume 70 of ERCIM News 70, jul 2007
Interacting services raise a number of new software engineering challenges. To meet these challenges, the behaviour of the involved services must be considered. We present results regarding the behaviour of services in isolation, the interaction of services in choreographies, the exchangeability of a service, and the synthesis of desired partner services.
close
close

• 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

• An ASM-Characterization of a Class of Distributed Algorithms
In Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis, Festschrift volume of Lecture Notes in Computer Science, Springer, 2007
close
• 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
• ### 2006

• 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
• 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

• How Expressive are Petri Net Schemata?
Susanna Donatelli and P. S. Thiagarajan, editors
In Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, Springer, 2006
Petri net schemata are an intuitive and expressive approach to describe high-level Petri nets. A Petri net schema is a Petri net with edges and transitions inscribed by terms and Boolean expressions, respectively. A concrete high-level net is gained by interpreting the symbols in the inscriptions by a structure. Its semantics can then be described in terms of a transition system. Therefore, the semantics of a Petri Net schema can be conceived as a family of transition systems indexed by structures. In this paper we characterize the expressive power of a general version of Petri net schemata. For that purpose we examine families of transition systems in general and characterize the families as generated by Petri net schemata. It turns out that these families of transition systems can be characterized by simple and intuitive requirements.
close
close

• Compensation in Workflow Nets
Susanna Donatelli and P. S. Thiagarajan, editors
In Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, Springer, 2006
close
• Brauer, Wilfried, Reisig, Wolfgang
Carl Adam Petri und die Petrinetze''
volume 29 of Informatik-Spektrum 29 (5), oct 2006
close

• On the Expressive Power of Unbounded-Nondeterministic Abstract State Machines
Informatik-Berichte, , dec 2006
Conventional computational models assume a symbolical representation of states. Gurevich's Abstract State Machines (ASMs) take a more liberal position: any mathematical structure may serve as a state. Gurevich characterizes the expressive power of sequential ASMs in a non-trivial theorem: he defines the class of \emphsequential algorithms by help of only a few, amazingly general requirements and proves this class to be equivalent to sequential ASMs. Later, this result has been extended to the class of bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among infinitely many alternatives. We define the class of unbounded-nondeterministic algorithms by a conservative extension of Gurevich's original requirements to sequential algorithms. We show that this class is equivalent to unbounded-nondeterministic ASMs.
close
close
• ### 2005

• Reisig, Wolfgang
Modeling- and Analysis Techniques for Web Services and Business Processes
Martin Steffen and Gianluigi Zavattaro, editors
In Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings, volume 3535 of Lecture Notes in Computer Science, Springer Verlag, may 2005
Open distributed systems include in particular Web services and business processes. There is a need of techniques to model such systems formally, and to derive decisive properties from such models. Three such techniques are presented in this paper, exemplified by help of realistic examples, and mutually related w.r.t. their respective expressive power and the availability of analysis techniques.
close
close
• Reisig, Wolfgang
On the Expressive Power of Petri Net Schemata
Gianfranco Ciardo and Philippe Darondeau, editors
In Applications and Theory of Petri Nets 2005: 26th International Conference, ICATPN 2005, Miami, USA, June 20-25, 2005. Proceedings, volume 3536 of Lecture Notes in Computer Science, Springer Verlag, may 2005
High-level Petri nets are frequently represented as Petri net schemas, with places, transitions and arcs inscribed by terms. A concrete system is then gained by interpreting the symbols in those terms. The behavior of a concrete system is a transition system. The composition of all those transition systems represents the behavior of the Petri net schema. This paper characterizes the expressive power of (a basic class of) Petri net schemas. It turns out that quite simple as well as quite general requirements at a transition system suffice to generate it by such a Petri net schema.
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
• Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian
Kommunizierende Workflow-Services modellieren und analysieren
Informatik - Forschung und Entwicklung, Springer-Verlag, oct 2005
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
• 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
• 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
• Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
An Operating Guideline Approach to the SOA
In 2nd South-East European Workshop on Formal Methods 2005 (SEEFM05), Ohrid, Republic of Macedonia, 2005
close
• Reisig, Wolfgang
Modeling- and Analysis Techniques for Web Services and Business Processes
Informatik-Berichte, , 2005
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
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
• ### 2004

• Alexander, Adrianna, Reisig, Wolfgang
Compositional Temporal Logic Based on Partial Order
Informatik-Berichte, , dec 2004
close
• Reisig, Wolfgang, Brade, A.
ASM Models for Web Services
Informatik-Berichte, , 2004
close
• Reisig, Wolfgang
The computable kernel of Sequential Abstract State Machines
Informatik-Berichte, , 2004
close
• Alexander, Adrianna, Reisig, Wolfgang
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
• ### 2003

• Alexander, Adrianna, Reisig, Wolfgang
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
• Weber, Herbert, Ehrig, Hartmut, Reisig, Wolfgang, Borusan, Alexander, Lembke, Sabine, Dehnert, Juliane, Weber, Michael, Martens, Axel, Padberg, Julia, Ermel, Claudia, Qemali, A.
The Petri Net Baukasten of the DFG Forschergruppe PETRI NET TECHNOLOGY
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
In the long history of Petri nets a universe of Petri nets has evolved consisting of an enormously rich theory, a wide variety of tools, and numerous successful applications and case studies in various application domains. This vast variety is not any more handable for anyone working with Petri nets, which results in the strong need of a structured access to Petri nets. This structured access has been the main aim of the DFG-Forschergruppe PETRI NET TECHNOLOGY, which has developed the so-called Petri Net Baukasten for this purpose. It is designed to support Petri net experts, application developers and tool developers alike in their specific work with Petri nets. This paper presents an overview of the concepts, initial and 2nd installment of the Petri Net Baukasten, which have been presented at the 1st and 2nd International Colloquium on Petri Net Technologies for Modelling Communication Based Systems in 1999 and 2001, respectively.
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
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
• ### 2002

• Reisig, Wolfgang
Teleteaching-Vorlesung 'Verteilte Systeme: Formale Methoden - Anwendungen - Werkzeuge'
Sigrid E. Schubert and Bernd Reusch and Norbert Jesse, editors
In , volume 19 of LNI, GI, 2002
close
• ### 2001

• Reisig, Wolfgang
Modelling of learning process, using methodology of System Petri Nets
In Tagungsband der International Scientific Conference MANAGEMENT INFORMATION SYSTEMS, Tibilisi, jun 2001
close
• ### 2000

• Reisig, Wolfgang
The Linear Theory of Multiset Based Dynamic Systems
Cristian Calude and Gheorghe Paun and Grzegorz Rozenberg and Arto Salomaa, editors
In Workshop on Multiset Processing (WMP 2000), volume 2235 of Lecture Notes in Computer Science, Springer-Verlag, 2000
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

• Inter-operability of Workshop Applications - Local Criteria for Global Soundness
, editors
In Business Process Management, volume 1806 of Lecture Notes in Computer Science, Springer-Verlag, 2000
close
• Foremniak, Adrianna, Reisig, Wolfgang
A Temporal Logic of Distributed Actions (TLDA)
Informatik-Berichte, , 2000
close
• ### 1999

• Battke, Anne, Borusan, Alexander, Dehnert, Juliane, Ehrig, Hartmut, Ermel, Claudia, Gajewsky, Maike, Hoffmann, Kathrin, Hohberg, Bodo, , Lembke, Sabine, Martens, Axel, Padberg, Julia, Reisig, Wolfgang, Vesper, Tobias, Weber, Herbert, Weber, Michael
Petrinetz-Technologie: Initial Realization of the Petri Net Baukasten
Informatik-Berichte, , oct 1999
close
• ### 1998

• Reisig, Wolfgang
On the structure of DNA Algorithm
Informatik-Berichte, , dec 1998
close
• Desel, Jörg, Reisig, Wolfgang
Place/Transition Petri Nets.
In Petri Nets, nov 1998
close
• Reisig, Wolfgang
Distributed Algorithms: Modeling and Analysis with Petri Nets
In Systems, Man, and Cybernetics, 1998. 1998 IEEE International Conference on, volume 1 of oct 1998
close
• Reisig, Wolfgang
Elements Of Distributed Algorithms: Modeling and Analysis with Petri Nets
Springer-Verlag, sep 1998
close
• ### 1997

• Ehrig, Hartmut, Reisig, Wolfgang
An Algebraic View on Petri Nets.
volume 61 of Bulletin of the EATCS 61, feb 1997
close

• DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen
Informatik-Berichte, , dec 1997
close
• Reisig, Wolfgang
Verteilte Algorithmen: Nutzen sie der Forschergruppe?
1997
close
• Reisig, Wolfgang
Interleaved progress, concurrent progress, and local progress
D. A. Peled and V. R. Pratt and G. J. Holzmann, editors
In Proceedings of the DIMACS workshop on Partial order methods in verification (POMIV '96), volume 29 of AMS Press, Inc., New York, NY, USA, 1997
close

• Petri Net Based Verification of Distributed Algorithms: An Example
volume 9 of Formal Aspects of Computing 9 (4), Springer-Verlag, 1997
close

• Verification of Distributed Algorithms with Algebraic Petri Nets
, editors
In Foundations of Computer Science: Potential - Theory - Cognition, volume 1337 of Lecture Notes in Computer Science, Springer-Verlag, 1997
close
• ### 1996

• Memorandum: Petrinetzmodelle zur Verifikation verteilter Algorithmen
Informatik-Berichte, , aug 1996
close

• Algebraic System Nets for Modelling Distributed Algorithms
volume 51 of Petri Net Newsletter 51, nov 1996
close
• Ehrig, Hartmut, Reisig, Wolfgang, Weber, Herbert
Kick-Off-Workshop der DFG-Forschergruppe 'Petrinetz-Technologie'
Informatik-Berichte, , dec 1996
close
• Reisig, Wolfgang
Temporallogische Verifikation verteilter Algortihmen: Mehr als nur eine Variante
, editors
In Formal Methods for Concurrency, GI-Kolloquium, Fachberichte der TU Dresden, , jul 1996
close

• Petri Net Based Verification of Distributed Algorithms: An Example
Informatik-Berichte, , may 1996
close
• Reisig, Wolfgang
Modelling and Verification of Distributed Algorithms
In CONCUR 96, volume 1119 of Lecture Notes in Computer Science, Springer-Verlag, 1996
close

• Distributed Algorithms for Networks of Agents.
In Petri Nets (2), 1996
close
• Reisig, Wolfgang, Rozenberg, Grzegorz
Informal Introduction to Petri Nets
In Petri Nets, 1996
close
• Desel, Jörg, Reisig, Wolfgang
The Synthesis Problem of Petri Nets.
volume 33 of Acta Informatica 33 (4), 1996
close
• ### 1995

• Reisig, Wolfgang
Petri Net Models of Distributed Algorithms.
In Computer Science Today, 1995
close
• ### 1994

• Reisig, Wolfgang
Correctness Proofs of Distributed Algorithms.
In Dagstuhl Seminar on Distributed Systems, 1994
close
• Reisig, Wolfgang
Petri-Netze und ihre Anwendungen
In , VDI Reihe 10: Informatik / Kommunikationstechnik, VDI-Verlag, , 1994
close
• Reisig, Wolfgang
Progress in Petrinets
Informatik-Berichte, , 1994
close
• Reisig, Wolfgang

, , Unter den Linden 6, 10099 Berlin, Germany, 1994
close
• ### 1993

• Reisig, Wolfgang
Formal methods for concurrent systems design: a survey
, editors
In Programming Models for Massively Parallel Computers, 1993. Proceedings, IEEE, sep 1993
Concurrency is frequently employed as a means to increase the performance of computing systems: a conventional sequential program is designed, to be parallelised later on. This contribution is intended to show that concurrent systems can also differ essentially from conventional, sequential systems, with respect to the kind of problems to be solved, and even to the principal limits of capability and performance. This paper surveys particular concepts and properties of concurrent systems, followed by a choice of models that more or less reflect those properties. Finally, the author discusses a typical example of an algorithm for concurrent systems.
close
close
• Reisig, Wolfgang
Spezifikation, Modellierung und Korrektheit von Informationssystemen
G. Scheschonk and Wolfgang Reisig, editors
In , Springer, 1993
close
• Desel, Jörg, Reisig, Wolfgang
The Synthesis Problem of Petri Nets.
In STACS, SFB-Bericht, 1993
close
• ### 1992

• Reisig, Wolfgang
Elements of a Temporal Logic Coping with Concurrency
SFB-Bericht, , 1992
close
• Reisig, Wolfgang
Report on the REX Workshop on Semantics-Foundations and Applications
volume 84 of Bulletin of the EATCS 84, 1992
close
• Reisig, Wolfgang
Combining Petri Nets and Other Formal Methods
In Application and Theory of Petri Nets, 1992
close
• Reisig, Wolfgang
A Primer in Petri Net Design
Springer Compass International, 1992
close
• ### 1991

• Reisig, Wolfgang
Petri Nets and Algebraic Specifications
volume 80 of Theor. Comput. Sci. 80 (1), 1991
close
• Reisig, Wolfgang
Parallel Composition of Liveness
SFB-Bericht, , 1991
close
• Reisig, Wolfgang
Concurrent Temporal Logic
SFB-Bericht, , 1991
close
• ### 1990

• Reisig, Wolfgang
Petrinetze: Grundfragen, Konzepte, Konsequenzen
Arbeitspapiere der GMD, 1990
close
• Plünnecke, Helmut, Reisig, Wolfgang
Bibliography on Petri nets 1990.
In Applications and Theory of Petri Nets, 1990
close
• ### 1989

• Reisig, Wolfgang
The decent philosophers: An exercise in operational semantics of concurrent systems
J.W. de Bakker, editors
In 25 Jaar Semantiek-Liber Amicorum, CWI, Amsterdamm, 1989
close
• ### 1988

• Reisig, Wolfgang
Towards a temporal logic of causality and choice in distributed systems
In REX Workshop, 1988
close
• Reisig, Wolfgang
Concurrency is more fundamental than interleaving
volume 35 of Bulletin of the EATCS 35, 1988
close
• Reisig, Wolfgang
Temporal Logic and Causality in Concurrent Systems.
In Concurrency, 1988
close
• ### 1987

• Smith, E., Reisig, Wolfgang
The Semantics of a Net is a Net: An Exercise in General Net Theory
K. Voss and H.J. Genrich and G. Rozenberg, editors
Concurrency and Nets - Advances in Petri Nets, Springer-Verlag, Berlin, 1987
close
• Reisig, Wolfgang
Das Verhalten verteilter Systeme
GMD-Bericht, Oldenbourg Berichte der GMD, , 1987
Modern information processing devices are normally considered distributed systems. Then particular processes are generally represented by sequences of states and/or transitions. In this book a different approach is developed where processes are only derived from the causal dependicies. The conceptual and practical advantages are explained using the problem of the dining philosophers''.
close
close
• Reisig, Wolfgang
Towards a Temporal Logic for True Concurrency. Part I: Linear Time Propositional Logic
Arbeitspapiere der GMD, , 1987
A logic is introduced, tailored for causality based partial order semantics of nonsequential systems. Properties which are essential for such systems can be formulated in the logic. Technically, the system model we consider is the most fundamental version of Petri Nets. The logic resembles to a liniear time propositional logic, applied to a universe of sets of partially ordered potential states.
close
close
• Reisig, Wolfgang, Vautherin, J.
An Algebraic Approach to High Level Petri Nets
In Proceedings of the Eighth European Workshop on Application and Theory of Petri Nets, Universidad de Zaragoza, Spain, 1987
close
• ### 1986

• Reisig, Wolfgang
Embedded System Description Using Petri Nets
In Embedded Systems, 1986
close
• Reisig, Wolfgang
Anforderungsbeschreibung und Systementwurf mit Petri-Netzen.
Handbuch der modernen Datenverarbeitung, Heft 130: Formale Methoden in der Systementwicklung, Forkel-Verlag, jul 1986
close
• Reisig, Wolfgang
A strong part of concurrency.
In European Workshop on Applications and Theory of Petri Nets, 1986
close
• Reisig, Wolfgang
Petri Nets in Software Engineering
In Advances in Petri Nets, 1986
close
• Reisig, Wolfgang
Place/Transition Systems
In Advances in Petri Nets, 1986
close
• Drees, Stefan, Gomm, Dominik, Plünnecke, Helmut, Reisig, Wolfgang, Walter, Rolf
Bibliography of Petri nets
In European Workshop on Applications and Theory of Petri Nets, 1986
close
• ### 1985

• Reisig, Wolfgang
Petri Nets with Individual Tokens
volume 41 of Theoretical Computer Science 41, 1985
close
• Reisig, Wolfgang
On the Semantics of Petri Nets.
E.J. Neuhold and G. Chroust, editors
Formal Models in Programming, IFIP 1985, North-Holland, Elsevier Science Publishers B. V., 1985
close
• Reisig, Wolfgang
Systementwurf mit Netzen
Springer, 1985
close
• ### 1984

• Reisig, Wolfgang
On the Semantics of Petri Nets.
Univ. Hamburg, Fachbereich Informatik, Bericht Nr. 100, sep 1984
close
• Reisig, Wolfgang
What Operational Semantics is Adequate for Nonsequential Systems?
Research Report, Tech. Univ. of Helsinki, Digital Systems Laboratory, Research, 1984
close
• Reisig, Wolfgang
Partial Order Semantics versus Interleaving Semantics for CSP-like Languages and its Impact on Fairness.
In ICALP, 1984
close
• Herzog, Otthein, Reisig, Wolfgang, Valk, Rüdiger
Petri-Netze: ein Abri\ss ihrer Grundlagen und Anwendungen.
volume 7 of Informatik Spektrum 7 (1), 1984
close
• Goltz, Ursula, Reisig, Wolfgang
CSP-programs with individual tokens.
In European Workshop on Applications and Theory in Petri Nets, 1984
close
• ### 1983

• Reisig, Wolfgang
System Design Using Petri Nets
In Requirements Engineering, 1983
close
• Goltz, Ursula, Reisig, Wolfgang
Processes of Place/Transition-Nets
In ICALP, 1983
close
• Goltz, Ursula, Reisig, Wolfgang
The Non-sequential Behavior of Petri Nets
volume 57 of Information and Control 57 (2/3), 1983
close
• Berthelot, G., Memmi, G., Reisig, Wolfgang
A Control Structure for Sequential Processes Synchronized by Buffers
In 4th Workshop on Theory and Applications of Petri Nets, Toulouse, September 1983, 1983
close
• ### 1982

• Reisig, Wolfgang
Petri Nets with Individual Tokens
In European Workshop on Applications and Theory of Petri Nets, 1982
close
• Reisig, Wolfgang
Deterministic Buffer Synchronization of Sequential Processes
volume 18 of Acta Informatica 18, 1982
close
• Reisig, Wolfgang
Petrinetze, Eine Einführung
Springer, 1982
close
• ### 1981

• Reisig, Wolfgang
Recursive Nets
In Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets, 1981
close
• Goltz, Ursula, Reisig, Wolfgang, Thiagarajan, P. S.
Two Alterative Definitions of Synchronic Distance
In Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets, 1981
close
• Goltz, Ursula, Reisig, Wolfgang
Weighted Synchronic Distances.
In Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets, 1981
close
• ### 1980

• Reisig, Wolfgang
A Graph Grammar Representation of Non-Sequential Processes
In WG, 1980
close
• Reisig, Wolfgang
Schemes for Nonsequential Processing Systems.
In MFCS, 1980
close
• ### 1979

• Reisig, Wolfgang
On a Class of Co-Operating Sequential Processors.
J.C. Syre, editors
In Proc. of the 1st European Conference on Parallel and Distributed Processing, Cepadues Editions, Toulouse, 1979
close
• Reisig, Wolfgang
A Note on the Representation of Finite Tree Automata
volume 8 of Information Processing Letters 8 (5), 1979
close
• Reisig, Wolfgang
Zur Verwendung von Petrinetz-Morphismen bei der Systemkonstruktion.
H.C. Mayr and B.E. Meyer, editors
, Springer-Verlag, Berlin, Heidelberg, New York, 1979
close
• Reisig, Wolfgang
On Solving Conflicts in Petri Nets. Workshop on Graph Theoretical Concepts in Computer Science, Berlin 1979
U. Pape, editors
Discrete Structures and Algorithms, Hanser Verlag, 1979
close
• Reisig, Wolfgang
Untersuchungen einer Klasse kooperierender sequentieller Prozesse mit Hilfe von Petri-Netzen
Dissertation, 1979
close
• ### 1977

• Reisig, Wolfgang
Interactive Schemes
M. Feilmeier, editors
In Parallel Computers - Parallel Mathematics, Proc. of the IMACS-GI-Symp., March 14--16, 1977, Munich, North-Holland Publishing Company, Amsterdam, 1977
close
• ### 1975

• Reisig, Wolfgang
Eine Verallgemeinerung des Berechenbarkeitsbegriffes durch Gleichungssysteme
Interner Bericht, , 1975
close
• ### 1974

• Indermark, K., Reisig, Wolfgang
On Recursively Definable Relations
In Report on the 14th Lattice Theory Conference, Szeged, Hungary, 1974, 1974
close

## Sürmeli, Jan

### 2016

• Homogeneous Equations of Algebraic Petri Nets
volume abs/1606.05490 of CoRR abs/1606.05490, 2016
close

• Homogeneous Equations of Algebraic Petri Nets
Jos\'ee Desharnais and Radha Jagadeesan, editors
In 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Qu\'ebec City, Canada, volume 59 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016
close

• Characterizing Stable and Deriving Valid Inequalities of Petri Nets
volume 146 of Fundam. Inform. 146 (1), 2016
close
• ### 2014

• Introducing Configurability into Scenario-Based Specification of Business Processes
In ZEUS, 2014
close
• ### 2013

• Cost-optimizing compositions of services - analysis and synthesis
Informatik-Berichte, Humboldt-Universität zu Berlin, 2013
close

• Synthesizing Cost-Minimal Partners for Services
Basu, Samik and Pautasso, Cesare and Zhang, Liang and Fu, Xiang, editors
In Service-Oriented Computing, volume 8274 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2013
close
• ### 2012

• Sürmeli, Jan
Synthesizing cost-minimal partners for services
Informatik-Berichte, Humboldt-Universität zu Berlin, 2012
close
• Sürmeli, Jan
Cost-minimal Adapters for Services
In Proceedings of the 4th Central-European Workshop on Services and their Composition, ZEUS-2012, Bamberg, Germany, February 23-24, 2012, 2012
close
• Sürmeli, Jan
Service Discovery with Cost Thresholds
In Proceedings of the 9th International Workshop on Web Services and Formal Methods, WS-FM 2012 September 6-7, 2012, Tallinn, Estonia, 2012
close
• ### 2011

• Schuller, Dieter, Sürmeli, Jan
Dienstgüte-basierte Service-Selektion für Zustandsbehaftete Services
Daniel Eichhorn and Agnes Koschmider and Huayu Zhang, editors
In Proceedings of the 3rd Central-European Workshop on Services and their Composition, ZEUS 2011, Karlsruhe, Germany, February 21--22, 2011, volume 705 of CEUR Workshop Proceedings, CEUR-WS.org, 2011
close
• Sürmeli, Jan
Towards deciding policy violation during service discovery
Daniel Eichhorn and Agnes Koschmider and Huayu Zhang, editors
In Proceedings of the 3rd Central-European Workshop on Services and their Composition, ZEUS 2011, Karlsruhe, Germany, February 21--22, 2011, volume 705 of CEUR Workshop Proceedings, CEUR-WS.org, 2011
close
• ### 2010

• Estimating costs of a service
Christian Gierds and Jan Sürmeli, editors
In Proceedings of the 2nd Central-European Workshop on Services and their Composition, ZEUS 2010, Berlin, Germany, February 25--26, 2010, volume 563 of CEUR Workshop Proceedings, CEUR-WS.org, 2010
When designing a publicly available Web service, a service designer has to take care of costs and revenue caused by this services. In the very beginning possible partners might only be vaguely known, or the service behavior contains arbitrary repetitions. Then the estimation of costs for running this service is difficult and decisions based on them can hardly be made. We propose a static analysis of the service's behavior. We over-approximate possible runs and therefore costs of the service. Our approach provides a basis for reasoning about nonfunctional properties as shown for costs.
close
close
• Oanea, Olivia, Sürmeli, Jan, Wolf, Karsten
Service Discovery Using Communication Fingerprints
Informatik-Berichte, Humboldt-Universität zu Berlin, jul 2010
close
• Oanea, Olivia, Sürmeli, Jan, Wolf, Karsten
Service Discovery Using Communication Fingerprints
Paul Maglio and Mathias Weske and Jian Yang and Marcelo Fantinato, editors
In 8th International Conference on Service Oriented Computing, ICSOC 2010, December 7-10, 2010, San Francisco, California, USA, Proceedings, volume 6470 of Lecture Notes in Computer Science, Springer-Verlag, dec 2010
A request to a service registry must be answered with a service that fits in several regards, including semantic compatibility, non-functional compatibility, and interface compatibility. In the case of stateful services, there is the additional need to check behavioral (i.e. protocol) compatibility. This paper is concerned with the latter aspect. An apparant approach to establishing behavioral compatibility would be to apply the well-known technology of model checking to a composition of the provided service and the requesting service. However, this procedure must potentially be repeated for all provided services in the registry which may unprohibitively slow down the response time of the broker. Hence, we propose to insert a preprocessing step. It consists of computing an abstraction of the behavior for each published service that we call communication fingerprint. Upon request, we use the fingerprint to rule out as many as possible incompatible services thus reducing the number of candidates that need to be model checked for behavioral compatibility. The technique is based on linear programming and is thus extremely efficient. We validate our approach on a large set of services that we cut out of real world business processes.
close
close
• ### 2009

• Creating Message Profiles of Open Nets
Oliver Kopp and Niels Lohmann, editors
In Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, 2009
close
• Sürmeli, Jan
Strukturelle Analyse von Servicenetzen
Diplomarbeit, feb 2009
close
• Sürmeli, Jan
Profiling Services with Static Analysis
In AWPN, volume 501 of CEUR Workshop Proceedings, CEUR-WS.org, 2009
close

## Stahl, Christian

### 2013

• Müller, Richard, Stahl, Christian, Aalst, Wil M. P. van der, Westergaard, Michael
Service Discovery from Observed Behavior while Guaranteeing Deadlock Freedom in Collaborations
Basu, Samik and Pautasso, Cesare and Zhang, Liang and Fu, Xiang, editors
In Service-Oriented Computing, volume 8274 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2013
close
• Müller, Richard, Stahl, Christian, Vogler, Walter
Undecidability of accordance for open systems with unbounded message queues
BPM Center Report, BPMcenter.org, 2013
close
• Vogler, Walter, Stahl, Christian, Müller, Richard
Trace- and Failure-Based Semantics for Bounded Responsiveness
Canal, Carlos and Villari, Massimo, editors
In Advances in Service-Oriented and Cloud Computing, volume 393 of Communications in Computer and Information Science, Springer Berlin Heidelberg, 2013
close
• Vogler, Walter, Stahl, Christian, Müller, Richard
Trace- and Failure-Based Semantics for Responsiveness
BPM Center Report, BPMcenter.org, 2013
close
• Müller, Richard, Stahl, Christian, Aalst, Wil M. P. van der, Westergaard, Michael
Service Discovery from Observed Behavior While Guaranteeing Deadlock Freedom in Collaborations
BPM Center Report, BPMcenter.org, 2013
close
• ### 2012

• Müller, Richard, Aalst, Wil M. P. van der, Stahl, Christian
Conformance Checking of Services Using the Best Matching Private View
In Proceedings of the 9th International Workshop on Web Services and Formal Methods, WS-FM 2012 September 6-7, 2012, Tallinn, Estonia, 2012
close
• Vogler, Walter, Stahl, Christian, Müller, Richard
A Trace-Based Semantics for Responsiveness
Jens Brandt and Keijo Heljanko, editors
In Proceedings of the 12th International Conference on Application of Concurrency to System Design, ACSD 2012, Hamburg, Germany, June 27-29, 2012, IEEE, 2012
close

• Deciding the Precongruence for Deadlock Freedom Using Operating Guidelines
, editors
In Proceedings of the 2nd International Workshop on Petri Nets Compositions, CompoNet'12, Hamburg, Germany, June 25-26, 2012, volume 853 of CEUR Workshop Proceedings, CEUR-WS.org, jun 2012
close
• ### 2011

• Mooij, Arjan, Parnjai, Jarungjit, Stahl, Christian, Voorhoeve, Marc
Constructing Replaceable Services Using Operating Guidelines and Maximal Controllers
Bravetti, Mario and Bultan, Tevfik, editors
In Web Services and Formal Methods, volume 6551 of Lecture Notes in Computer Science, Springer Berlin / Heidelberg, 2011
close
• ### 2010

• 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
• ### 2009

• 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
• 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
• 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

• 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
• 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
• 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
• 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
• ### 2008

• 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
• 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

• 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
• 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
• 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
• 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