## Publikationen (nach name sortiert)

### 2005

Komposition Temporallogischer Spezifikationen - Spezifikation und Verifikation von Systemen mit Temporal Logic of Distributed Actions
Dissertation, sep 2005
This thesis introduces a new temporal logic, called Temporal Logic ofDistributed Actions, TLDA for short. TLDA is designed for compositional specification and verification of distributed systems. TLDA originates syntactically from an already established temporal logic, TLA. But TLDA, contrary to TLA and other known compositional temporal logics, is based semantically on a partial order structure, called distributed run. Compared to TLA, the use of this semantical model increases the expressiveness of TLDA. Both the system and its properties are described in one formalism: They are represented by a set of distributed runs and specified in TLDA by a temporal logic formula. Hence, the verification of a system is reduced to proving that the system specification implies the property specification. We provide a set of proof rules for this. We show that the composition of systems is specified by conjunction of the specifications of its components and, usually, the specification of the interaction between the components. Hence, the specification of a composed system can be derived from specifications of its components. Component properties are preserved in the process of composition. Thus, components can be verified separately and then be integrated into the composed system. This economises the effort for verification. Attuned for distributed runs we develop a semantical criterion for TLDA-formulas, called environmental invariance. We show that environmental invariant formulas are suited for the specification of system components. We prove that such environmental invariant formulas, due to their properties, supply a modular design of systems.
close
close
• ### 2004

• Compositional Temporal Logic Based on Partial Order
Informatik-Berichte, Humboldt-Universität zu Berlin, dec 2004
close

• Compositional Temporal Logic Based on Partial Order
In 11th International Symposium on Temporal Representation and Reasoning (TIME'04), IEEE Computer Society, 2004
The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. The logic supports a compositional design of systems: subsystems can be specified separately and then be integrated into one system. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.
close
close
Composition of Temporal Logic Specifications
Jordi Cortadella and Wolfgang Reisig, editors
In Applications and Theory of Petri Nets 2004, 25th International Conference (ICATPN 2004), Lecture Notes in Computer Science, Springer-Verlag, 2004
The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA supports a modular design of systems: Subsystems can be specified and verified separately and then be integrated into one system. The properties of the subsystems will be preserved in this process. 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

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

• Adrianna Foremniak, Peter H. Starke
Structural Analysis of Signal-Event Systems
volume 43 of Fundamenta Informaticae 43 (1-4), aug 2000
close

• A Temporal Logic of Distributed Actions (TLDA)
Informatik-Berichte, Humboldt-Universität zu Berlin, 2000
close

## Andreas Glausch

### 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
• Andreas Glausch
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, Humboldt-Universität zu Berlin, 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
• Andreas Glausch
Distributed Abstract State Machines - Status Report of a Doctoral Thesis
Jörg Desel, editors
In Proceedings of the Doctoral Consortium ACSD \& PetriNets 2006, Åbo Akademi, 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

• Andreas Glausch
Eine Charakterisierung einfacher Petrinetz-Schemata
Karsten Schmidt and Christian Stahl, editors
In 12. Workshop "Algorithmen und Werkzeuge für Petrinetze" (AWPN 2005), Proceedings, Humboldt-Universität zu Berlin, sep 2005
Wir untersuchen die Ausdrucksmächtigkeit von Petrinetz-Schemata. Dazuführen wir die Teilklasse der einfachen Petrinetz-Schemata ein und zeigen, welche Systeme sich durch ein einfaches Petrinetz-Schema darstellen lassen und welche nicht. Die hinreichenden und notwendigen Eigenschaften dazu formulieren wir in einem Theorem.
close
close
• Andreas Glausch
Varianten des ASM-Theorems
Diplomarbeit, jun 2005
Abstract-State-Machines, kurz ASMs, sind eine Methode zur formalen Beschreibung von Algorithmen. Diese Methode hebt sich dabei deutlich von klassischen Algorithmusbegriffen wie Turingmaschinen und berechenbaren Funktionen ab. So lassen sich mit ASMs unter anderem auch nicht-terminierende Algorithmen beschreiben. Genauso wie es unterschiedliche Klassen von Algorithmen gibt, existieren auch eine ganze Reihe unterschiedlicher Klassen von ASMs, so zum Beispiel die sequentiellen, die nichtdeterministischen und die verteilten ASMs. Für die Klasse der sequentiellen ASMs exisitiert eine schöne Charakterisierung durch das sogenannte ASM-Theorem. Diese Charakterisierung basiert auf natürlichen und leicht verständlichen Forderungen und erleichtert somit dass Verständnis für die Ausdrucksmächtigkeit der sequentiellen ASMs und von Algorithmen im Allgemeinen. In dieser Arbeit erweitern wir das ASM-Theorem auf die Klasse der nichtdeterministischen ASMs und auf die Klasse der verteilten ASMs.
close
close
• ### 2003

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

## Axel Martens

### 2007

• Simon Moser, Axel Martens, Katharina Görlach, Wolfram Amme, Artur Godlinski
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

• Axel Martens
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
• Axel Martens
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
• Axel Martens
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
• Bernd-Holger Schlingloff, Axel Martens, Karsten Schmidt
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
• Axel Martens
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

• Axel Martens, Christian Stahl, Daniela Weinberg, Dirk Fahland, Thomas Heidinger
Business Process Execution Language for Web services - Semantik, Analyse und Visualisierung
Informatik-Berichte, Humboldt-Universität zu Berlin, jul 2004
Moderne Systeme der Informationstechnik bestehen zumeist aus einer Vielzahl von Komponenten, die in einem Netzwerk auf verteilten Knoten ausgeführt werden. Mit dem Web-Service-Ansatz können solche Systeme einfacher und flexibler entwickelt werden. Diese Arbeit befasst sich mit der Modellierung, Visualisierung und Analyse von Web Services. Ein Web Service kapselt eine Anwendung und stellt diese über ein wohldefiniertes Interface der Außenwelt zur Verfügung. Im Gegensatz zu früheren Ansätzen dienen eine Reihe zusammenhängender Technologien zur Beschreibung eines Web Service. Diese Arbeit beschäftigt sich vor allem mit der internen Struktur eines Web Service, beschrieben mit Hilfe der Business Process Execution Language for Web Services (BPEL4WS) [ACD+02]. Der Web-Service-Ansatz bietet ein homogenes Konzept von Komponenten und ihrer Komposition ber einem heterogenen Netzwerk. Damit ist die syntaktische Grundlage für die Entwicklung verteilter Systeme gelegt. Wesentlich für den Erfolg der Web Services ist jedoch die Beantwortung der semantischen Fragestellungen: Passen zwei gegebene Web Services inhaltlich zusammen? Kann in einem verteilten System ein gegebener Web Service durch einen anderen ersetzt werden? Entspricht ein konkreter Web Service einer gegebenen abstrakten Spezifikation? Diese Arbeit befasst sich mit der Beantwortung dieser und weiterer Fragestellungen im Web-Service-Ansatz: In einem ersten Schritt entwickeln wir eine formale Semantik für die Sprache BPEL4WS. Darauf aufbauend werden Methoden zur Analyse verteilter Systeme auf die konkreten Anforderungen bertragen und neue Verfahren entwickelt. Für die Diskussion der Modelle und Eigenschaften entwickeln wir eine intuitive graphische Repräsentation der Sprache BPEL4WS. Das Ziel der Forschungen ist die Umsetzung der Methoden in einem integrierten Entwicklungswerkzeug für BPEL4WS. Die vorliegende Arbeit beschreibt die ersten Ergebnisse in einem laufenden Projekt.
close
close
• Axel Martens
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

• Axel Martens
Compatibility of Web Services
In 10th Workshop on Algorithms and Tools for Petri Nets (AWPN 2003), Eichstätt, Germany, 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
• Herbert Weber, Hartmut Ehrig, Wolfgang Reisig, Alexander Borusan, Sabine Lembke, Juliane Dehnert, Michael Weber, Axel Martens, Julia Padberg, Claudia Ermel, A. Qemali
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
• Axel Martens
On Usability of Web Services
Coral Calero and Oscar Díaz and Mario Piattini, 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
• Axel Martens
On Compatibility of Web Services
Gabriel Juhás and Ekkart Kindler, editors
volume 65 of Petri Net Newsletter 65, 2003
close
• Axel Martens
Verteilte Geschäftsprozesse - Modellierung und Verifikation mit Hilfe von Web Services
Dissertation, 2003
close
• ### 2001

• Axel Martens
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
Wil M. P. van der Aalst and Jörg Desel and Andreas Oberweis, 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

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

• Szenarios - Lokale Kriterien für globale Korrektheit
K. Spies and B. Schätz, editors
In Formale Beschreibungstechniken für verteilte Systeme, 9. GI/ITG Fachgesprächs, Utz Verlag, München, jun 1999
close
• ### 1997

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

## Baver Acu

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

## Christian Gierds

### 2012

• Christian Gierds, Arjan J. Mooij, Karsten Wolf
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

• Christian Gierds
Strukturelle Reduktion von Bedienungsanleitungen
Diplomarbeit, jan 2008
In dieser Arbeit werden wir uns mit Diamantenstrukturen in Bedienungsanleitungen beschäftigen. Im Rahmen der Service-Oriented Architecture beschreiben Bedienungsanleitungen Kommunikationspartner (Strategien) von Diensten. Ein großer Vorteil der Bedienungsanleitungen ist die endliche Repräsentation der gewöhnlich unendlich großen Menge aller Strategien eines Dienstes. Bedienungsanleitungen können nichtsdestotrotz sehr groß werden. Diamantenstrukturen sind eine der Hauptursachen dafür. Wir wollen eine Kurzschreibweise einführen, die das Eintreten von Ereignissen in jeder beliebigen Reihenfolge in einem Zustandsübergang beschreibt. Anschließend werden wir verschiedene Muster für Diamantenstrukturen vorstellen, also Muster mit Ereignissen, die in jeder beliebigen Reihenfolge stattfinden können. Für diese Muster werden wir Ersetzungen mit der eingeführten Kurzschreibweise angeben. Wir werden ferner Algorithmen angeben, welche die von uns definierten Diamantenmuster in Bedienungsanleitungen erkennen.
close
close
• Christian Gierds, Arjan J. Mooij, Karsten Wolf
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
• Christian Gierds
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

• Christian Gierds
Ein schärferes Kriterium für die Wahl von Endzuständen in Bedienungsanleitungen, Liberalsten Partnern und Public Views
Studienarbeit, oct 2007
In der Welt der Service Orientierten Architektur (SOA) besteht der Bedarf, Dienste auf ihre mögliche Interaktion mit anderen Diensten hin zu untersuchen. Dienste werden wir in Form von Serviceautomaten betrachten, die als asynchron kommunizierende Automaten definiert sind. Um die Frage einer sinnvollen, also verklemmungsfreien Kommunikation zu klären, gibt es das Konzept der Bedienungsanleitungen. Wie werden für diese ein scharfes Kriterium für die Wahl der Endzustände angeben und zeigen, dass diese Wahl sich in vorhandene Konzepte integriert. Besonderes Augenmerk werden wir dabei auf den Liberalsten Partner und den Public View eines Serviceautomaten werfen und an diesen unsere Definition rechtfertigen.
close
close

## Christian Stahl

### 2012

• Richard Müller, W. M. P. van der Aalst, Christian Stahl
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
• Walter Vogler, Christian Stahl, Richard Müller
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
Michael Köhler-Bußmeier, 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

• Arjan Mooij, Jarungjit Parnjai, Christian Stahl, Marc Voorhoeve
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

• Wil M. P. van der Aalst, Niels Lohmann, Peter Massuthe, Christian Stahl, Karsten Wolf
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
• Arjan J. Mooij, Christian Stahl, Marc Voorhoeve
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

• 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
• Karsten Wolf, Christian Stahl, Janine Ott, Robert Danitz
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
• Wil M. P. van der Aalst, Arjan J. Mooij, Christian Stahl, Karsten Wolf
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
• Nannette Liske, Niels Lohmann, Christian Stahl, Karsten Wolf
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
• Niels Lohmann, Eric Verbeek, Chun Ouyang, Christian Stahl
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
• Kees van Hee, Eric Verbeek, Christian Stahl, Natalia Sidorova
A Framework for Linking and Pricing No-Cure-No-Pay Services
Kurt Jensen and Wil M. P. van der Aalst, editors
volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2, Springer-Verlag, mar 2009
In this paper, we present a framework that allows us to orchestrate web services such that the web services involved in this orchestration interact properly. To achieve this, we predefine service interfaces and certain routing constructs. Furthermore, we define a number of rules to incrementally compute the price of such a properly interacting orchestration (i.e. a web service) from the price of its web services. The fact that a web service gets only payed after its service is delivered (no-cure-no-pay) is reflected by considering a probability of success. To determine a safe price that includes the risk a web service takes, we consider the variance of costs.
close
close

• Deciding 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
• Christian Stahl
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
• Dieter König, Niels Lohmann, Simon Moser, Christian Stahl, Karsten Wolf
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

• 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
• Kees M. van Hee, H.M.W. Verbeek, Christian Stahl, Natalia Sidorova
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
• Wil M. P. van der Aalst, Niels Lohmann, Peter Massuthe, Christian Stahl, Karsten Wolf
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

• Wil M. P. van der Aalst, Peter Massuthe, Arjan J. Mooij, Christian Stahl, Karsten Wolf
Erratum -- Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
Informatik-Berichte, Humboldt-Universität zu Berlin, jun 2007
close
• Kees M. van Hee, Natalia Sidorova, Christian Stahl, H. M. W. Verbeek
A Price of Service in a Compositional SOA Framework
Computer Science Report, Technische Universiteit Eindhoven, The Netherlands, jul 2007
In this paper we propose a framework for SOA covering such important features as proper termination (soundness) and correct correlation of tasks. Within this framework, we define a method for the calculation of the price of services. Our framework is compositional in the sense that composing a system from subsystems that meet our correctness requirements we obtain a system that still meets these requirements.
close
close
• Dieter König, Niels Lohmann, Simon Moser, Christian Stahl, Karsten Wolf
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
• Niels Lohmann, H. M. W. Verbeek, Chun Ouyang, Christian Stahl, Wil M. P. van der Aalst
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
• Wil M. P. van der Aalst, Michael Beisiegel, Kees M. van Hee, Dieter König, Christian Stahl
An SOA-based architecture framework
volume 2 of International Journal of Business Process Integration and Management (IJBPIM) 2 (2), 2007
We present an Service-Oriented Architecture (SOA)-based architecture framework. The architecture framework is designed to be close to industry standards, especially to the Service ComponentArchitecture (SCA).The framework is language independent and the building blocks of each system, activities and data, are first class citizens.We present a meta model of the architecture framework and discuss its concepts in detail. Through the framework, concepts of an SOA such as wiring, correlation and instantiation can be clarified.
close
close
• Wil M. P. van der Aalst, Peter Massuthe, Christian Stahl, Karsten Wolf
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
• Wolfgang Reisig, Karsten Wolf, Jan Bretschneider, Kathrin Kaschner, Niels Lohmann, Peter Massuthe, Christian Stahl
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

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

• Analysis Techniques for Service Models
In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, IEEE Computer Society, nov 2006
The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.
close
close

• Analyzing Interacting BPEL Processes
In Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings, volume 4102 of Lecture Notes in Computer Science, Springer-Verlag, sep 2006
This paper addresses the problem of analyzing theinteraction between BPEL processes. We present a technology chain that starts out with a BPEL process and transforms it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). A case study demonstrates the value of this technology chain.
close
close
• Wil M. P. van der Aalst, Michael Beisiegel, Kees M. van Hee, Dieter König, Christian Stahl
A SOA-Based Architecture Framework
Frank Leymann and Wolfgang Reisig and Satish R. Thatte and Wil M. P. van der Aalst, editors
In The Role of Business Processes in Service Oriented Architectures, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, nov 2006
In this paper we present first results of a SOA-based architecture framework. The architecture framework is required to be close to industry standards, especially to service component architecture (SCA), language independent (i.e. it is adoptable) and the building blocks of each system, activities and data, are first class citizens. We present a meta model of the architecture framework and discuss its concepts in detail.
close
close
• Milo\vs Krsti\'c, Eckhard Grass, Christian Stahl, Maxim Piz
System Integration by Request-driven GALS Design
volume 153 of IEE Proc. Computers \& Digital Techniques 153 (5), September 2006
A novel request-driven globally asynchronous locally synchronous (GALS) technique for the system integration of complex digital blocks is proposed. For this new GALS technique, an asynchronous wrapper compliant is developed and evaluated. This proposed GALS technique is applied to a baseband processor compatible with the wireless LAN standard IEEE 802.11a. The developed GALS baseband processor chip is fabricated and measured. Besides improvements of the system integration process, a 5 dB reduction in electromagnetic interference, 30\% reduction in instantaneous supply current variation, and similar dynamic power consumption as in the synchronous baseband processor is achieved.
close
close
• ### 2005

• Sebastian Hinz, Karsten Schmidt, Christian Stahl
Transforming BPEL to Petri Nets
Wil M. P. van der Aalst and B. Benatallah and F. Casati and F. Curbera, editors
In Proceedings of the Third International Conference on Business Process Management (BPM 2005), volume 3649 of Lecture Notes in Computer Science, Springer-Verlag, Nancy, France, sep 2005
We present a Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation). The semantics is implemented as a parser that translates BPEL specifications into the input language of the Petri net model checking tool LoLA. We demonstrate that the semantics is well suited for computer aided verification purposes.
close
close

• 12. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2005), Proceedings
Informatik-Berichte, Humboldt-Universität zu Berlin, sep 2005
close

• Kommunizierende Workflow-Services modellieren und analysieren
Informatik - Forschung und Entwicklung, Springer-Verlag, oct 2005
Zur adäquaten Nutzung von Workflow-Implementierungen kommunizierender Geschäftsprozesse werden Konzepte vorgeschlagen,die von konkreten Implementierungen abstrahieren. Auf der Basis von Petrinetzen werden unterschiedliche Varianten der Bedienbarkeit von Workflows charakterisiert und dafür Entscheidungsalgorithmen vorgestellt. Die Angemessenheit des Ansatzes wird am Beispiel der Semantik von Komponenten der Geschäftsprozess-Modellierungssprache BPEL demonstriert.
close
close
• Eckhard Grass, Frank Winkler, Milos Krstic, Alexandra Julius, Christian Stahl, Maxim Piz
Enhanced GALS Techniques for Datapath Applications
Vassilis Paliouras and Johan Vounckx and Diederik Verkest, editors
In Integrated Circuit and System Design: 15th International Workshop, PATMOS 2005, Leuven, Belgium, September 20-23, 2005, volume 3728 of Lecture Notes in Computer Science, Springer-Verlag, aug 2005
Based on a previously reported request driven technique for Globally-Asynchronous Locally-Synchronous (GALS) circuits this paper presents two significant enhancements. Firstly, the previously required local ring oscillators are avoided. Instead, an external clock with arbitrary phase for each GALS block is used. Details of the required wrapper circuitry, the proposed design flow and performance are provided. Secondly, to reduce supply noise, a novel approach applying individual clock jitter for GALS blocks is proposed. A simulation using the jitter technique shows that for a typical GALS system, the power spectrum of the supply current can be reduced by about 15 dB.
close
close
• Christian Stahl
A Petri Net Semantics for BPEL
Informatik-Berichte, Humboldt-Universität zu Berlin, jul 2005
We present a pattern-based Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics is complete - it covers the standard behaviour of BPEL as well as the exceptional behav-iour (e.g. faults, events, compensation). Therefore every business process specified in BPEL can be transformed into a Petri net.
close
close
• Christian Stahl, Wolfgang Reisig, Milos Krstic
Hazard Detection in a GALS Wrapper: a Case study
Informatik-Berichte, Humboldt-Universität zu Berlin, 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
• Milos Krstic, Eckhard Grass, Christian Stahl
Request-Driven GALS Technique for Wireless Communication System
In Proceedings of the 11th International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 2005), IEEE Computer Society, New York, NY, USA, mar 2005
A Globally Asynchronous - Locally Synchronous (GALS) technique for application in wireless communication systems is proposed and evaluated. The GALS wrappers are based on a request-driven operation with an embedded time-out function. A formally verified GALS wrapper is deployed for the ?GALSification? of a baseband processor for WLAN. Details of the GALS partitioning, implementation and the design-flow are discussed. Furthermore, a test strategy based on built-in self-test (BIST) is suggested. The described baseband processor was fabricated and successfully tested. The GALS design is compared with a clock-gated, synchronous version. Advantages for system integration are achieved along with a 1% reduction in dynamic power consumption, a 30% reduction in peak power supply current, and 5 dB reduction in spectral noise.
close
close
• Christian Stahl, Wolfgang Reisig, Milos Krstic
Hazard Detection in a GALS Wrapper: A Case Study
Jörg Desel and Y. Watanabe, 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

• Verteilte Geschäftsprozesse modellieren und analysieren
Informatik-Berichte, Humboldt-Universität zu Berlin, feb 2005
Verteilte Geschäftsprozesse nutzen das Internet, um auf heterogenen Rechnerstrukturen Dienste auszubieten. Modellierungstechniken und Implementierungssprachen für solche Dienste werfen im Vergleich mit herkömmlichen Rechnern grundlegend neue Fragestellungen auf. Wir diskutieren einige davon und zeigen, wie Petrinetze ihre Beantwortung ermöglichen.
close
close
• ### 2004

• A Petri net semantic for BPEL4WS - validation and application
Ekkart Kindler, editors
In Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN'04), Universität Paderborn, oct 2004
We translated a small business process into a recently defined Petri net semantic. Then we used the tool LoLA for validating the semantic as well as for proving relevant properties of the particular process.
close
close
• Axel Martens, Christian Stahl, Daniela Weinberg, Dirk Fahland, Thomas Heidinger
Business Process Execution Language for Web services - Semantik, Analyse und Visualisierung
Informatik-Berichte, Humboldt-Universität zu Berlin, jul 2004
Moderne Systeme der Informationstechnik bestehen zumeist aus einer Vielzahl von Komponenten, die in einem Netzwerk auf verteilten Knoten ausgeführt werden. Mit dem Web-Service-Ansatz können solche Systeme einfacher und flexibler entwickelt werden. Diese Arbeit befasst sich mit der Modellierung, Visualisierung und Analyse von Web Services. Ein Web Service kapselt eine Anwendung und stellt diese über ein wohldefiniertes Interface der Außenwelt zur Verfügung. Im Gegensatz zu früheren Ansätzen dienen eine Reihe zusammenhängender Technologien zur Beschreibung eines Web Service. Diese Arbeit beschäftigt sich vor allem mit der internen Struktur eines Web Service, beschrieben mit Hilfe der Business Process Execution Language for Web Services (BPEL4WS) [ACD+02]. Der Web-Service-Ansatz bietet ein homogenes Konzept von Komponenten und ihrer Komposition ber einem heterogenen Netzwerk. Damit ist die syntaktische Grundlage für die Entwicklung verteilter Systeme gelegt. Wesentlich für den Erfolg der Web Services ist jedoch die Beantwortung der semantischen Fragestellungen: Passen zwei gegebene Web Services inhaltlich zusammen? Kann in einem verteilten System ein gegebener Web Service durch einen anderen ersetzt werden? Entspricht ein konkreter Web Service einer gegebenen abstrakten Spezifikation? Diese Arbeit befasst sich mit der Beantwortung dieser und weiterer Fragestellungen im Web-Service-Ansatz: In einem ersten Schritt entwickeln wir eine formale Semantik für die Sprache BPEL4WS. Darauf aufbauend werden Methoden zur Analyse verteilter Systeme auf die konkreten Anforderungen bertragen und neue Verfahren entwickelt. Für die Diskussion der Modelle und Eigenschaften entwickeln wir eine intuitive graphische Repräsentation der Sprache BPEL4WS. Das Ziel der Forschungen ist die Umsetzung der Methoden in einem integrierten Entwicklungswerkzeug für BPEL4WS. Die vorliegende Arbeit beschreibt die ersten Ergebnisse in einem laufenden Projekt.
close
close
• Christian Stahl
Transformation von BPEL4WS in Petrinetze
Diplomarbeit, apr 2004
BPEL4WS ist eine Sprache zur Beschreibung verteilter Geschäftsprozesse mit Web Services. Es besteht die Notwendigkeit, die Sprache trotz ihrer Komplexität zu verstehen, um mit ihr im Umfeld von Web Services arbeiten zu können. Mit Hilfe einer formalen Semantik ist es möglich, die Sprache selbst und mit BPEL4WS spezifizierte Geschäftsprozesse zu verifizieren. In der vorliegenden Arbeit wird eine Petrinetz-Semantik für BPEL4WS vorgestellt. Dazu wird gezeigt, dass jedes Konstrukt der Sprache BPEL4WS in ein Petrinetz-Muster übersetzt werden kann. Damit ist es möglich, jeden in der Geschäftsprozesssprache BPEL4WS modellierten Geschäftsprozess in ein Petrinetz zu transformieren. Bei der Entwicklung der Semantik kann auf Forschungsergebnisse aus dem Bereich "Petrinetze als Werkzeug zur Geschäftsprozessmodellierung" zurückgegriffen werden.
close
close
• Jose M. Vidal, Paul Buhler, Christian Stahl
Multiagent Systems with Workflows
volume 8 of IEEE Internet Computing 8 (1), feb 2004
Industry and researchers have two different visions for the future of Web services. Industry wants to capitalize on Web service technology to automate business processes via centralized workflow enactment. Researchers are interested in the dynamic composition of Web services. The authors show how these two visions are points in a continuum and discuss a possible path for bridging the gap between them.
close
close
• ### 2003

• Dirk Hain, Christian Stahl
Komposition von Web Services
Studienarbeit, apr 2003
Verteilte Systeme haben in den letzten Jahren in der Informatik immer mehr an Bedeutung gewonnen. Die Web-Service-Architektur ist eine Software-Architektur zur Modellierung und Implementierung verteilter Systeme. Sie ist als eine der zukunftsträchtigsten Technologien angesehen, die aber noch in der Erprobungsphase steckt. Unter anderem ist die Kompatibilität von Web Services eine offene Frage, wobei weniger syntaktische als vielmehr sematischen Kompatibilität problematisch ist. Diese Arbeit soll Ansätze zur Bestimmung semantischer Kompatibilität von Web Services liefern.
close
close

## Christoph Wagner

### 2011

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

• Christoph Wagner
Partner datenverarbeitender Services
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

## Daniela Weinberg

### 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
• ### 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
• Daniela Weinberg
Efficient Controllability Analysis of Open Nets
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
A service is designed to interact with other services. If the service interaction is stateful and asynchronous, the interaction protocol can become quite complex. A service may be able to interact with a lot of possible partner services, one partner or no partner at all. Having no partner surely is not intended by the designer. But the stateful interaction between services can be formalized and thus analyzed at design time. We present a formalization which is centered around a graph data structure that we call interaction graph, which represents feasible runs of a partner service according to the interaction protocol. As interaction graphs suffer from state explosion, we introduce a set of suitable reduction rules to alleviate the complexity of our approach. As our case studies show we are able to analyze the interaction behavior of a service efficiently.
close
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
• ### 2006

• Analysis Techniques for Service Models
In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, IEEE Computer Society, nov 2006
The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.
close
close

• Analyzing Interacting BPEL Processes
In Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings, volume 4102 of Lecture Notes in Computer Science, Springer-Verlag, sep 2006
This paper addresses the problem of analyzing theinteraction between BPEL processes. We present a technology chain that starts out with a BPEL process and transforms it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). A case study demonstrates the value of this technology chain.
close
close
• Daniela Weinberg
Reduction Rules for Interaction Graphs
Informatik-Berichte, Humboldt-Universität zu Berlin, feb 2006
The internet today has grown to be more than just being a basis for exchanging information. It steadily becomes a platform for processing business processes. Many companies distribute their service with the help of web services or integrate other web services into their own workflow. However, before a web service gets published it should be examined well. We will introduce a way of examining the controllability of a web service. That means, we study whether a controller can actually use the functionality provided by the web service. We propose the interaction graph of a web service, that is modelled by an open workflow net. To verify whether such a net is controllable or not it is sufficient to construct a reduced interaction graph. We will define reduction rules that minimize the size of the graph greatly. The analysis using the interaction graph as well as the reduction rules shown in this paper are implemented and have been integrated into an analysis tool kit for web services.
close
close
• ### 2005

• Ingo Stürmer, Daniela Weinberg, Mirko Conrad
Overview of Existing Safeguarding Techniques for Automatically Generated Code
In SEAS '05: Proceedings of the Second International Workshop on Software Engineering for Automotive Systems, ACM Press, New York, NY, USA, 2005
Code generators are increasingly used in an industrial context to translate graphical models into executable code. Since the code is often deployed in safety-related environments, the quality of the code generators is of paramount importance. In this paper, we will present and discuss state-of-the-art techniques for safeguarding automatic code generation applied in model-based development.
close
close

• Reduction Rules for Interaction Graphs
Karsten Schmidt and Christian Stahl, editors
In 12. Workshop "Algorithmen und Werkzeuge für Petrinetze" (AWPN 2005), Proceedings, Humboldt-Universität zu Berlin, sep 2005
The internet today has grown to be more than just being a basisfor exchanging information. It steadily becomes a platform for processing business processes. Many companies distribute their service with the help of web services or integrate other web services into their own workflow. However, before a web service gets published it should be examined well. We will introduce a way of examining the controllability of a web service. We propose the interaction graph of a web service, that is modelled by an open workflow net. To verify whether such a net is controllable or not it is sufficient to construct a reduced interaction graph. We will define reduction rules that minimize the size of the graph greatly. The analysis using the interaction graph as well as the reduction rules are implemented and have been integrated into an analysis tool kit for web services.
close
close
• ### 2004

• Daniela Weinberg
Analyse der Bedienbarkeit
Diplomarbeit, oct 2004
Das heutige Internet wächst zunehmend von einer Plattform als Informationsquelle hin zu einer Basis für die Abwicklung von Geschäftsprozessen. Zahlreiche Firmen stellen ihre Dienste bereits mit Hilfe von Web-Services zur Verfügung oder integrieren andere bereitgestellte Web-Services in ihren Geschäftsablauf. Nach Studien einiger Forschungsinstitute geht der Trend in der heutigen IT-Branche stark zum Einsatz solcher verteilter Geschäftsprozesse. Es werden Schlagworte wie out-tasking, plug-and-play und Lego-Wirtschaft geprägt. Bevor ein Geschäftsprozess in Form eines Web-Services jedoch veröffentlicht wird, sollte dieser geeignet untersucht werden. Wir werden uns in dieser Arbeit diesem Thema mit Hilfe von Petri-Netz-Modulen nähern. Sie modellieren gerade die interne Struktur von Geschäftsprozessen und ermöglichen es, den Prozess geeignet zu analysieren. Uns interessiert bei der Analyse, ob die Funktionalität, die ein Web-Service bereitstellen soll, auch wirklich genutzt werden kann. Wir sprechen in diesem Zusammenhang von Bedienbarkeit. Für die Analyse definieren wir den Interaktionsgraphen eines Workflow-Moduls, welcher die Zustände des Moduls und dessen Interaktion mit einer Umgebung veranschaulicht. Auf dieser Grundlage können wir dann eine Bedienstrategie definieren, durch die das Modul bedient werden kann. Das hei¼t, wenn eine Umgebung das Modul so bedienen kann, dass dieses ordentlich terminiert, finden wir eine Bedienstrategie in dem Interaktionsgraphen des Moduls. Darüber hinaus bieten die Graphen dem Modellierer die Möglichkeit, einen Blick auf die Abläufe seines Moduls zu werfen und genau erkennen zu können, welche Zustände des Moduls bei welcher Interaktion mit der Umgebung eingenommen werden. Auf Grundlage dieser Analyse kann der Modellierer seinen Prozess überarbeiten, anpassen etc. Um die Bedienbarkeit der Workflow-Module durch den Interaktionsgraphen zu verifizieren, reicht es aus, einen reduzierten Graphen zu konstruieren. Wir werden Reduktionsregeln definieren, die den Nachweis der Bedienbarkeit in den reduzierten Graphen erhalten. Die in dieser Arbeit entwickelten Algorithmen sind implementiert und in Wombat4ws, einem Analysewerkzeug für Web-Services, integriert worden.
close
close
• Axel Martens, Christian Stahl, Daniela Weinberg, Dirk Fahland, Thomas Heidinger
Business Process Execution Language for Web services - Semantik, Analyse und Visualisierung
Informatik-Berichte, Humboldt-Universität zu Berlin, jul 2004
Moderne Systeme der Informationstechnik bestehen zumeist aus einer Vielzahl von Komponenten, die in einem Netzwerk auf verteilten Knoten ausgeführt werden. Mit dem Web-Service-Ansatz können solche Systeme einfacher und flexibler entwickelt werden. Diese Arbeit befasst sich mit der Modellierung, Visualisierung und Analyse von Web Services. Ein Web Service kapselt eine Anwendung und stellt diese über ein wohldefiniertes Interface der Außenwelt zur Verfügung. Im Gegensatz zu früheren Ansätzen dienen eine Reihe zusammenhängender Technologien zur Beschreibung eines Web Service. Diese Arbeit beschäftigt sich vor allem mit der internen Struktur eines Web Service, beschrieben mit Hilfe der Business Process Execution Language for Web Services (BPEL4WS) [ACD+02]. Der Web-Service-Ansatz bietet ein homogenes Konzept von Komponenten und ihrer Komposition ber einem heterogenen Netzwerk. Damit ist die syntaktische Grundlage für die Entwicklung verteilter Systeme gelegt. Wesentlich für den Erfolg der Web Services ist jedoch die Beantwortung der semantischen Fragestellungen: Passen zwei gegebene Web Services inhaltlich zusammen? Kann in einem verteilten System ein gegebener Web Service durch einen anderen ersetzt werden? Entspricht ein konkreter Web Service einer gegebenen abstrakten Spezifikation? Diese Arbeit befasst sich mit der Beantwortung dieser und weiterer Fragestellungen im Web-Service-Ansatz: In einem ersten Schritt entwickeln wir eine formale Semantik für die Sprache BPEL4WS. Darauf aufbauend werden Methoden zur Analyse verteilter Systeme auf die konkreten Anforderungen bertragen und neue Verfahren entwickelt. Für die Diskussion der Modelle und Eigenschaften entwickeln wir eine intuitive graphische Repräsentation der Sprache BPEL4WS. Das Ziel der Forschungen ist die Umsetzung der Methoden in einem integrierten Entwicklungswerkzeug für BPEL4WS. Die vorliegende Arbeit beschreibt die ersten Ergebnisse in einem laufenden Projekt.
close
close
• ### 2003

• Daniela Weinberg
Graphische Repräsentation von BPEL
Studienarbeit, aug 2003
close

## Dirk Fahland

### 2012

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

• Jakob Pinggera, Stefan Zugal, Barbara Weber, Dirk Fahland, Matthias Weidlich, Jan Mendling, Hajo Reijers
How the Structuring of Domain Knowledge Can Help Casual Process Modelers
In ER 2010, 2010
Modeling business processes has become a common activity in industry, but it is increasingly carried out by non-experts. This raises a challenge: How to ensure that the resulting process models are of sufficient quality? This paper contends that a prior structuring of domain knowledge, as found in informal specifications, will positively influence the act of process modeling in various measures of performance. This idea is tested and confirmed with a controlled experiment, which involved 83 master students in business administration and industrial engineering from Humboldt-Universität zu Berlin and Eindhoven University of Technology. In line with the reported findings, our recommendation is to explore ways to bring more structure in the specifications that are used as input for process modeling endeavors.
close
close
• Matthias Weidlich, Stefan Zugal, Jakob Pinggera, Dirk Fahland, Barbara Weber, Hajo Reijers, Jan Mendling
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
• Dirk Fahland, Matthias Weidlich
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

• Dirk Fahland, Jan Mendling, Hajo Reijers, Barbara Weber, Matthias Weidlich, Stefan Zugal
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
• Dirk Fahland, C\'edric Favre, Barbara Jobstmann, Jana Koehler, Niels Lohmann, Hagen Völzer, Karsten Wolf
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
• Dirk Fahland, Daniel Lübke, Jan Mendling, Hajo Reijers, Barbara Weber, Matthias Weidlich, Stefan Zugal
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
• Dirk Fahland
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
• Dirk Fahland
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

• Dirk Fahland
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
• Dirk Fahland, Heiko Woith
Towards Process Models for Disaster Response
In Business Process Management Workshops, International Workshop on Process Management for Highly Dynamic and Pervasive Scenarios (PM4HDPS), co-located with 6th International Conference on Business Process Management (BPM'08), volume 17 of Lecture Notes in Business Information Processing, 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
• Dirk Fahland
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
• Dirk Fahland
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
• Dirk Fahland
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

• Dirk Fahland
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
• Dirk Fahland
Synthesizing Petri nets from LTL specifications - An engineering approach
Philippi, Stephan and Pinl, Alexander, editors
In Proceedings 14.Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN), Arbeitsbericht aus dem Fach Informatik, Nr. 25/2007, Universität Koblenz-Landau, D, September 2007
In this paper we present a pattern-based approach for synthesizing truly distributed Petri nets from a class of LTL specifications. The synthesis allows for the automatic, correct generation of humanly conceivable Petri nets, thus circumventing a manual construction of nets, or the use of Büuchi automata which are not distributed and often less intuitive to understand.
close
close
• Dirk Fahland
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
• Dirk Fahland
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
• Dirk Fahland, Timo M. Gläßer, Bastian Quilitz, Stephan Weißleder, Ulf Leser
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

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

• Dirk Fahland
Complete Abstract Operational Semantics for the Web Service Business Process Execution Language
Informatik-Berichte, Humboldt-Universität zu Berlin, sep 2005
In this technical report we present an abstract operational semantics for the Business ProcessExecution Language for Web Services, or BPEL for short. In effect, the semantics defined herein are a variation and an extension of the semantics published first in [FGV04a] and [Far04] defined by the group of Uwe Glässer the Simon Fraser University, Vancouver, Canada. We namely add semantics for correlation handling, dead path elimination and event handling; we define the data handling on a finer level; we slightly alter the basic framework of how activities are formalized in [FGV04a] in order to achieve greater robustness against changes of the informal specification. Furthermore this technical report serves as a base for a joint work with the group of Simon Fraser University.
close
close

• ASM-based semantics for BPEL: The negative Control Flow
Danièle Beauquier and Egon Börger and Anatol Slissenko, 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

• Dirk Fahland
Ein Ansatz einer formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines
Studienarbeit, aug 2004
In dieser Arbeit stellen wir einen Ansatz zur Definition einer formalen Semantik für die Business Process Execution Language for Web Services (kurz BPEL4WS) von IBM, Microsoft und deren Industriepartnern vor. Zur Formalisierung wählen wir den Abstract-State-Machine-Formalismus (kurz ASM), dessen theoretische Fundierung es uns erlaubt, die Semantik von BPEL4WS auf der selben Abstraktionsebene zur formalisieren, die in der informalen BPEL4WS-Spezifikation vorgegeben ist. Wir werden den inneren Aufbau der Sprache präzise, formal abbilden und damit eine intuitiv und anschaulich nachvollziehbare Entsprechung zwischen den Abläufen eines BPEL4WSProzesses gemäß der gegebenen informalen Semantik und unserer formalen Semantik aufzeigen. Dazu analysieren wir die Struktur von BPEL4WS und zeigen mit welchen Mitteln des ASM-Formalismus diese adäquat, formal erfasst werden und wie in ASM notierte Spezifikationen zu lesen sind. Hierzu werden wir beispielhaft ausgewählte, syntaktische Konstrukte von BPEL4WS nach unserem Ansatz formalisieren. Die vorliegende Arbeit bezieht sich auf die informale BPEL4WS-Spezifikation v1.1, veröffentlicht am 5. Mai 2003.
close
close
• Axel Martens, Christian Stahl, Daniela Weinberg, Dirk Fahland, Thomas Heidinger
Business Process Execution Language for Web services - Semantik, Analyse und Visualisierung
Informatik-Berichte, Humboldt-Universität zu Berlin, jul 2004
Moderne Systeme der Informationstechnik bestehen zumeist aus einer Vielzahl von Komponenten, die in einem Netzwerk auf verteilten Knoten ausgeführt werden. Mit dem Web-Service-Ansatz können solche Systeme einfacher und flexibler entwickelt werden. Diese Arbeit befasst sich mit der Modellierung, Visualisierung und Analyse von Web Services. Ein Web Service kapselt eine Anwendung und stellt diese über ein wohldefiniertes Interface der Außenwelt zur Verfügung. Im Gegensatz zu früheren Ansätzen dienen eine Reihe zusammenhängender Technologien zur Beschreibung eines Web Service. Diese Arbeit beschäftigt sich vor allem mit der internen Struktur eines Web Service, beschrieben mit Hilfe der Business Process Execution Language for Web Services (BPEL4WS) [ACD+02]. Der Web-Service-Ansatz bietet ein homogenes Konzept von Komponenten und ihrer Komposition ber einem heterogenen Netzwerk. Damit ist die syntaktische Grundlage für die Entwicklung verteilter Systeme gelegt. Wesentlich für den Erfolg der Web Services ist jedoch die Beantwortung der semantischen Fragestellungen: Passen zwei gegebene Web Services inhaltlich zusammen? Kann in einem verteilten System ein gegebener Web Service durch einen anderen ersetzt werden? Entspricht ein konkreter Web Service einer gegebenen abstrakten Spezifikation? Diese Arbeit befasst sich mit der Beantwortung dieser und weiterer Fragestellungen im Web-Service-Ansatz: In einem ersten Schritt entwickeln wir eine formale Semantik für die Sprache BPEL4WS. Darauf aufbauend werden Methoden zur Analyse verteilter Systeme auf die konkreten Anforderungen bertragen und neue Verfahren entwickelt. Für die Diskussion der Modelle und Eigenschaften entwickeln wir eine intuitive graphische Repräsentation der Sprache BPEL4WS. Das Ziel der Forschungen ist die Umsetzung der Methoden in einem integrierten Entwicklungswerkzeug für BPEL4WS. Die vorliegende Arbeit beschreibt die ersten Ergebnisse in einem laufenden Projekt.
close
close

## Ekkart Kindler

### 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, Katholische Universität Eichstätt, 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
• Ekkart Kindler
Systematische Spezifikation und Verifikation von Konsistenzprotokollen
Habilitationsschrift, aug 2001
close

• A Universal Module Concept for Petri Nets - An Implementation-Oriented Approach
Informatik-Berichte, Humboldt-Universität zu Berlin, apr 2001
close
• ### 2000

• Ekkart Kindler, Dennis Shasha
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
Kjeld Høyer Mortensen, editors
In Tool Demonstrations, 21. ICATPN, Århus, Denmark, jun 2000
close
• Ekkart Kindler
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
• Matthias Jüngel, Ekkart Kindler, Michael Weber
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, Århus, Dänemark, jun 2000
close
• Matthias Jüngel, Ekkart Kindler, Michael Weber
The Petri Net Markup Language
S. Philippi, editors
In 7. Workshop Algorithmen und Werkzeuge für Petrinetze, Fachberichte Informatik 7/2000, Universität Koblenz-Landau, 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
Wil M. P. van der Aalst and Jörg Desel and Andreas Oberweis, 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
• Ekkart Kindler
Serializability, concurrency control and replication control
G. Saake and K. Schwarz and C. Türker, 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

• Szenarios - Lokale Kriterien für globale Korrektheit
K. Spies and B. Schätz, editors
In Formale Beschreibungstechniken für verteilte Systeme, 9. GI/ITG Fachgesprächs, Utz Verlag, München, jun 1999
close
• Ekkart Kindler
Serializability, concurrency control and replication control
G. Saake and K. Schwarz and C. Türker, 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
• Ekkart Kindler
A classification of consistency models
Technical Report, Freie Universität Berlin, Institut für Informatik, oct 1999
close

• Der Petrinetz-Kern: Ein Überblick
E. Schnieder, editors
In Entwicklung und Betrieb komplexer Automatisierungssysteme, 6. Fachtagung, Band II, may 1999
close
• Ekkart Kindler, Wil M. P. van der Aalst
Liveness, Fairness, and Recurrence
Technical Report, University of Georgia, Department of Computer Science, Athens, USA, apr 1999
close
• Thomas Baar, Ekkart Kindler, Hagen Völzer
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
• Thomas Baar, Ekkart Kindler
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
Jörg Desel and Manuel Silva, 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
• Ekkart Kindler
The interplay of transaction models and memory models
M. Tamer Özsu and Asuman Dogac and Özgür Ulusoy, 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
Jörg Desel and Manuel Silva, 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
• Ekkart Kindler
Database theory - Petri net theory - Workflow theory
Informatik-Berichte, Humboldt-Universität zu Berlin, may 1998
close
• Thomas Baar, Ekkart Kindler
Einsatz von ILF und DAWN zur Verifikation verteilter Algorithmen - Eine Vorstudie
Informatik-Berichte, Humboldt-Universität zu Berlin, 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
• Jens Hauptmann, Bodo Hohberg, Ekkart Kindler, Ines Schwenzer, Michael Weber
Der Petrinetz-Kern - Dokumentation der Anwendungs-Schnittstelle
Informatik-Berichte, Humboldt-Universität zu Berlin, feb 1998
close
• ### 1997

• Ekkart Kindler
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, Universität Hamburg, Fachbereich Informatik, sep 1997
close

• ESTL: A temporal logic for events and states
Informatik-Berichte, Humboldt-Universität zu Berlin, nov 1997
close

• Flexibility in algebraic nets
Informatik-Berichte, Humboldt-Universität zu Berlin, nov 1997
close

• DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen
Informatik-Berichte, Humboldt-Universität zu Berlin, dec 1997
close
• Jörg Desel, Ekkart Kindler, Andreas Oberweis
Algorithmen und Werkzeuge für Petrinetze, 4. Workshop
Informatik-Berichte, Humboldt-Universität zu Berlin, sep 1997
close
• Ekkart Kindler
A compositional partial order semantics for Petri net components
Pierre Azéma and Gianfranco Balbo, 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
Christian Freksa and Matthias Jantzen and Rüdiger Valk, editors
In Foundations of Computer Science: Potential - Theory - Cognition, volume 1337 of Lecture Notes in Computer Science, Springer-Verlag, 1997
close
• Ekkart Kindler
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, Universität Karlsruhe, feb 1997
close
• Olaf Fricke, Alexander Borusan, Tobias Vesper, Ekkart Kindler
Verifikation im Vorgehensmodell anhand eines Beispiels
1997
close
• ### 1996

• Rolf Walter, Hagen Völzer, Tobias Vesper, Wolfgang Reisig, Ekkart Kindler, Jörn Freiheit, Jörg Desel
Memorandum: Petrinetzmodelle zur Verifikation verteilter Algorithmen
Informatik-Berichte, Humboldt-Universität zu Berlin, aug 1996
close

• Der Traum von einem universellen Petrinetz-Werkzeug - Der Petrinetz-Kern
Jörg Desel and Ekkart Kindler and Andreas Oberweis, editors
In 3. Workshop Algorithmen und Werkzeuge für Petrinetze, Institut AIFB, Universität Karlsruhe, oct 1996
close

• Automatisch überprüfbare Beweistechniken für algebraische Petrinetze
Jörg Desel and Ekkart Kindler and Andreas Oberweis, editors
In 3. Workshop Algorithmen und Werkzeuge für Petrinetze, Institut AIFB, Universität Karlsruhe, oct 1996
close

• Algebraic System Nets for Modelling Distributed Algorithms
volume 51 of Petri Net Newsletter 51, nov 1996
close
• Ekkart Kindler
A Specification and Verification Method for Caching Protocols
Jörg Desel and Horst Reichel, editors
In Formal Methods for Concurrency, GI-Kolloquium, Fachberichte der TU Dresden, Technische Universität 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
• Ekkart Kindler
A Compositional Partial Order Semantics for Petri Net Components
SFB-Bericht, Technische Universität München, mar 1996
close
• Ekkart Kindler, Andreas Listl, Rolf Walter
A Specification Method for Transaction Models with Data Replication
Informatik-Berichte, Humboldt-Universität zu Berlin, mar 1996
close

• Petri Net Based Verification of Distributed Algorithms: An Example
Informatik-Berichte, Humboldt-Universität zu Berlin, may 1996
close

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

## Hagen Völzer

### 2009

• Dirk Fahland, C\'edric Favre, Barbara Jobstmann, Jana Koehler, Niels Lohmann, Hagen Völzer, Karsten Wolf
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
• ### 2000

• Hagen Völzer
Fairneß, Randomisierung und Konspiration in verteilten Algorithmen
Dissertation, dec 2000
Fairneß (d.h. faire Konfliktlösung), Randomisierung (d.h. Münzwürfe) und partielle Synchronie sind verschiedene Konzepte, die häufig zur Lösung zentraler Synchronisations- und Koordinationsprobleme in verteilten Systemen verwendet werden. Beispiele für solche Probleme sind das Problem des wechselseitigen Ausschlusses (kurz: Mutex-Problem) sowie das Konsens-Problem. Für einige solcher Probleme wurde bewiesen, daß ohne die oben genannten Konzepte keine Lösung für das betrachtete Problem existiert. Unmöglichkeitsresultate dieser Art verbessern unser Verständnis der Wirkungsweise verteilter Algorithmen sowie das Verständnis des Trade-offs zwischen einem leicht analysierbaren und einem ausdrucksstarken Modell für verteiltes Rechnen. In dieser Arbeit stellen wir zwei neue Unmöglichkeitsresultate vor. Darüberhinaus beleuchten wir ihre Hintergründe. Wir betrachten dabei Modelle, die Randomisierung einbeziehen, da bisher wenig über die Grenzen der Ausdrucksstärke von Randomisierung bekannt ist. Mit einer Lösung eines Problems durch Randomisierung meinen wir, daß das betrachtete Problem mit Wahrscheinlichkeit 1 gelöst wird. Im ersten Teil der Arbeit untersuchen wir die Beziehung von Fairneß und Randomisierung. Einerseits ist bekannt, daß einige Probleme (z.B. das Konsens- Problem) durch Randomisierung nicht aber durch Fairneß lösbar sind. Wir zeigen nun, daß es andererseits auch Probleme gibt (nämlich das Mutex-Problem), die durch Fairneß, nicht aber durch Randomisierung lösbar sind. Daraus folgt, daß Fairneß nicht durch Randomisierung implementiert werden kann. Im zweiten Teil der Arbeit verwenden wir ein Modell, das Fairneß und Randomisierung vereint. Ein solches Modell ist relativ ausdrucksstark: Es erlaubt Lösungen für das Mutex-Problem, das Konsens-Problem, sowie eine Lösung für das allgemeine Mutex-Problem. Beim allgemeinen Mutex-Problem (auch bekannt als Problem der speisenden Philosophen) ist eine Nachbarschaftsrelation auf den Agenten gegeben und ein Algorithmus gesucht, der das Mutex-Problem für jedes Paar von Nachbarn simultan löst. Schließlich betrachten wir das ausfalltolerante allgemeine Mutex-Problem -- eine Variante des allgemeinen Mutex-Problems, bei der Agenten ausfallen können. Wir zeigen, daß sogar die Verbindung von Fairneß und Randomisierung nicht genügt, um eine Lösung für das ausfalltolerante allgemeine Mutex-Problem zu konstruieren. Ein Hintergrund für dieses Unmöglichkeitsresultat ist ein unerwünschtes Phänomen, für das in der Literatur der Begriff Konspiration geprägt wurde. Konspiration wurde bisher nicht adäquat charakterisiert. Wir charakterisieren Konspiration auf der Grundlage nicht-sequentieller Abläufe. Desweiteren zeigen wir, daß Konspiration für eine große Klasse von Systemen durch die zusätzliche Annahme von partieller Synchronie verhindert werden kann, d.h. ein konspirationsbehaftetes System kann zu einem randomisierten System verfeinert werden, das unter Fairneß und partieller Synchronie mit Wahrscheinlichkeit 1 konspirationsfrei ist. Partielle Synchronie fordert, daß alle relativen Geschwindigkeiten im System durch eine Konstante beschränkt sind, die jedoch den Agenten nicht bekannt ist. Die Darstellung der Unmöglichkeitsresultate und die Charakterisierung von Konspiration wird erst durch die Verwendung nicht-sequentieller Abläufe möglich. Ein nicht-sequentieller Ablauf repräsentiert im Gegensatz zu einem sequentiellen Ablauf kausale Ordnung und nicht zeitliche Ordnung von Ereignissen. Wir entwickeln in dieser Arbeit eine nicht-sequentielle Semantik für randomisierte verteilte Algorithmen, da es bisher keine in der Literatur gibt. In dieser Semantik wird kausale Unabhängigkeit durch stochastische Unabhängigkeit widergespiegelt.
close
close
• Felix C. Gärtner, Hagen Völzer
Redundancy in Space in Fault-Tolerant Systems
Technical Report, Department of Computer Science, Darmstadt University of Technology, jul 2000
close

• Algebraic Nets with Flexible Arcs
Theoretical Computer Science, 2000
close
• ### 1999

• Thomas Baar, Ekkart Kindler, Hagen Völzer
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
• ### 1998

• Flexibility in Algebraic Nets
Jörg Desel and Manuel Silva, 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
• ### 1997

• DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen
Informatik-Berichte, Humboldt-Universität zu Berlin, dec 1997
close

• Flexibility in algebraic nets
Informatik-Berichte, Humboldt-Universität zu Berlin, nov 1997
close
• Hagen Völzer
Verifying fault tolerance of distributed algorithms formally: A case study
Informatik-Berichte, Humboldt-Universität zu Berlin, may 1997
close

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

• Rolf Walter, Hagen Völzer, Tobias Vesper, Wolfgang Reisig, Ekkart Kindler, Jörn Freiheit, Jörg Desel
Memorandum: Petrinetzmodelle zur Verifikation verteilter Algorithmen
Informatik-Berichte, Humboldt-Universität zu Berlin, aug 1996
close

• Petri Net Based Verification of Distributed Algorithms: An Example
Informatik-Berichte, Humboldt-Universität zu Berlin, may 1996
close

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

## Jan Bretschneider

### 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
• Jan Bretschneider
Produktbedienungsanleitungen zur Charakterisierung austauschbarer Services
Diplomarbeit, mar 2007
Unternehmen sind bestrebt, immer mehr Geschäfte mit ihren Kunden teilweise oder vollständig automatisiert abzuwickeln. In diesem Bestreben machen sie mehr und mehr Gebrauch von der serviceorientierten Architektur (SOA). Grundbaustein der SOA ist der Service, der eine von einem Unternehmen angebotene Dienstleistung oder Funktionalität über eine wohldefinierte Schnittstelle bereitstellt und von Kunden oder Services anderer Unternehmen verwendet werden kann. Damit wir zwei Services als sinnvoll miteinander interagierend bezeichnen können, müssen sie verschiedene Mindestanforderungen erfüllen. Auf Grundlage dieser Mindestanforderungen können wir für jeden gegebenen Service eine Bedienungsanleitung konstruieren, die alle sinnvoll mit ihm interagierenden Services charakterisiert. Auch tritt die Frage auf, gegen welche Services ein Service ausgetauscht werden kann, so dass alle Services, die mit dem alten sinnvoll interagieren konnten, auch mit dem neuen sinnvoll interagieren können. Diesen allgemeinen Austauschbarkeitsbegriff parametrisieren wir in der vorliegenden Arbeit und beschäftigen uns mit dem Fall, dass durch den Austausch eines Services nur eine bestimmte Menge von Services unberührt bleiben soll, weil dies eine größere Freiheit in der Wahl des austauschenden Service erlaubt. Wir werden die Menge der Services, gegen die sich ein bestimmter Service bezüglich einer gegebenen Menge von Services austauschen lässt, mit Hilfe des Konzepts der Bedienungsanleitungen genau charakterisieren.
close
close
• Wolfgang Reisig, Karsten Wolf, Jan Bretschneider, Kathrin Kaschner, Niels Lohmann, Peter Massuthe, Christian Stahl
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

• Jan Bretschneider
Modellierung und Synthese eines geschwindigkeitsinvarianten GALS-Wrappers
Studienarbeit, feb 2006
Global asynchrone, lokal synchrone (GALS) Systeme vereinen dieVorteile synchroner und asynchroner Schaltungen und mindern zugleich ihre Nachteile. Ein GALS-System besteht aus mehreren lokal synchron arbeitenden Modulen, von denen jedes von einem asynchron arbeitenden Wrapper umhüllt wird. Durch diese Wrapper kommunizieren die Module asynchron miteinander. Das IHP Frankfurt hat auf Grundlage einer informalen Spezifikation einen GALS-Wrapper entwickelt. Erst nachträglich wurde ein formales Modell für diesen Wrapper erstellt und auf Korrektheit überprüft. Dabei wurden Fehler in der Implementierung gefunden und korrigiert. Wir beschreiben den Entwurf eines per Konstruktion korrekten Wrappers, der sich an der Schnittstelle zu seiner Umgebung genauso verhält, wie der Wrapper des IHP. Dazu modellieren wir erst sein Verhalten als Petrinetz und generieren danach aus diesem Modell mit dem Werkzeug petrify eine geschwindigkeitsinvariante Schaltung, die per Konstruktion korrekt arbeitet.
close
close

## Jan Sürmeli

### 2011

• Dieter Schuller, Jan Sürmeli
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
• Jan Sürmeli
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
• Olivia Oanea, Jan Sürmeli, Karsten Wolf
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
• Jan Sürmeli
Strukturelle Analyse von Servicenetzen
Diplomarbeit, feb 2009
close
• Jan Sürmeli
Profiling Services with Static Analysis
In AWPN, volume 501 of CEUR Workshop Proceedings, CEUR-WS.org, 2009
close

## Jarungjit Parnjai

### 2011

• Arjan Mooij, Jarungjit Parnjai, Christian Stahl, Marc Voorhoeve
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
• Jarungjit Parnjai
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

• 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

## Johannes Klaus Fichte

### 2009

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

## Karsten Wolf

### 2012

• Christian Gierds, Arjan J. Mooij, Karsten Wolf
Reducing Adapter Synthesis to Controller Synthesis
volume 5 of IEEE T. Services Computing 5 (1), 2012
close
• ### 2010

• Wil M. P. van der Aalst, Niels Lohmann, Peter Massuthe, Christian Stahl, Karsten Wolf
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
• Olivia Oanea, Jan Sürmeli, Karsten Wolf
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

• Wil M. P. van der Aalst, Arjan J. Mooij, Christian Stahl, Karsten Wolf
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
• Dirk Fahland, C\'edric Favre, Barbara Jobstmann, Jana Koehler, Niels Lohmann, Hagen Völzer, Karsten Wolf
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
• Karsten Wolf, Christian Stahl, Janine Ott, Robert Danitz
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

• 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
• Nannette Liske, Niels Lohmann, Christian Stahl, Karsten Wolf
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

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

• Peter Massuthe, Alexander Serebrenik, Natalia Sidorova, Karsten Wolf
Can I find a Partner?
Preprint, Universität Rostock, 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
• Dieter König, Niels Lohmann, Simon Moser, Christian Stahl, Karsten Wolf
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

• 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
• Peter Massuthe, Alexander Serebrenik, Natalia Sidorova, Karsten Wolf
Can I find a Partner? Undecidablity of Partner Existence for Open Nets
volume 108 of Information Processing Letters 108 (6), Nov 2008
close
• Chistian Stahl, Karsten Wolf
An Approach to Tackle Livelock-Freedom in SOA
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
We calculate a fixed finite set of state space fragments for a service P, where each fragment carries a part of the whole behavior of P. By composing these fragments according to the behavior of a service R we build the state space of their composition P \oplus R which can be checked for deadlocks and livelocks. We show that this approach is applicable to realize a find'' request by a service $R$ with a provided service P in SOA.
close
close
• Christian Gierds, Arjan J. Mooij, Karsten Wolf
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
• Wil M. P. van der Aalst, Niels Lohmann, Peter Massuthe, Christian Stahl, Karsten Wolf
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

• 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
• Wil M. P. van der Aalst, Peter Massuthe, Arjan J. Mooij, Christian Stahl, Karsten Wolf
Erratum -- Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
Informatik-Berichte, Humboldt-Universität zu Berlin, jun 2007
close
• Dieter König, Niels Lohmann, Simon Moser, Christian Stahl, Karsten Wolf
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
• Wolfgang Reisig, Karsten Wolf, Jan Bretschneider, Kathrin Kaschner, Niels Lohmann, Peter Massuthe, Christian Stahl
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
• Kathrin Kaschner, Peter Massuthe, Karsten Wolf
Symbolic Representation of Operating Guidelines for Services
volume 72 of Petri Net Newsletter 72, apr 2007
close

• 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

• 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
• Wil M. P. van der Aalst, Peter Massuthe, Christian Stahl, Karsten Wolf
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

• 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

• An Algorithm for Matching Nondeterministic Services with Operating Guidelines
Informatik-Berichte, Humboldt-Universität zu Berlin, 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

• 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

• 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
• Kathrin Kaschner, Peter Massuthe, Karsten Wolf
Symbolische Repräsentation von Bedienungsanleitungen für Services
Daniel Moldt, editors
In 13. Workshop "Algorithmen und Werkzeuge für Petrinetze" (AWPN 2006), Proceedings, Universität Hamburg, sep 2006
close

• Operating Guidelines for Finite-State Services
Informatik-Berichte, Humboldt-Universität zu Berlin, 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

• 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
• Stephan Roch, Karsten Schmidt
On the step explosion problem
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
• ### 2005

• Operating Guidelines for Services
Karsten Schmidt and Christian Stahl, editors
In 12. Workshop "Algorithmen und Werkzeuge für Petrinetze" (AWPN 2005), Proceedings, Humboldt-Universität zu Berlin, 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
• Sebastian Hinz, Karsten Schmidt, Christian Stahl
Transforming BPEL to Petri Nets
Wil M. P. van der Aalst and B. Benatallah and F. Casati and F. Curbera, editors
In Proceedings of the Third International Conference on Business Process Management (BPM 2005), volume 3649 of Lecture Notes in Computer Science, Springer-Verlag, Nancy, France, sep 2005
We present a Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation). The semantics is implemented as a parser that translates BPEL specifications into the input language of the Petri net model checking tool LoLA. We demonstrate that the semantics is well suited for computer aided verification purposes.
close
close
• Carsten Frenkler, Karsten Schmidt
Modellierung und Analyse transaktionaler Geschäftsprozesse
Karsten Schmidt and Christian Stahl, editors
In 12. Workshop "Algorithmen und Werkzeuge für Petrinetze" (AWPN 2005), Proceedings, Humboldt-Universität zu Berlin, sep 2005
Wie erweitern in dieser Arbeit Workflow-Module um ein Konzept, mit dem derEinfluß eines Datenbanksystems auf die Bedienbarkeit eines Geschäftsprozesses untersucht werden kann. Wir integrieren transaktionale Eigenschaften als internes Verhalten in Workflow-Module und können damit Bedienbarkeit und Einhaltung transaktionaler Eigenschaften durch Analyse entscheiden.
close
close

• 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

• 12. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2005), Proceedings
Informatik-Berichte, Humboldt-Universität zu Berlin, sep 2005
close

• Kommunizierende Workflow-Services modellieren und analysieren
Informatik - Forschung und Entwicklung, Springer-Verlag, oct 2005
Zur adäquaten Nutzung von Workflow-Implementierungen kommunizierender Geschäftsprozesse werden Konzepte vorgeschlagen,die von konkreten Implementierungen abstrahieren. Auf der Basis von Petrinetzen werden unterschiedliche Varianten der Bedienbarkeit von Workflows charakterisiert und dafür Entscheidungsalgorithmen vorgestellt. Die Angemessenheit des Ansatzes wird am Beispiel der Semantik von Komponenten der Geschäftsprozess-Modellierungssprache BPEL demonstriert.
close
close

• Reduction Rules for Interaction Graphs
Karsten Schmidt and Christian Stahl, editors
In 12. Workshop "Algorithmen und Werkzeuge für Petrinetze" (AWPN 2005), Proceedings, Humboldt-Universität zu Berlin, sep 2005
The internet today has grown to be more than just being a basisfor exchanging information. It steadily becomes a platform for processing business processes. Many companies distribute their service with the help of web services or integrate other web services into their own workflow. However, before a web service gets published it should be examined well. We will introduce a way of examining the controllability of a web service. We propose the interaction graph of a web service, that is modelled by an open workflow net. To verify whether such a net is controllable or not it is sufficient to construct a reduced interaction graph. We will define reduction rules that minimize the size of the graph greatly. The analysis using the interaction graph as well as the reduction rules are implemented and have been integrated into an analysis tool kit for web services.
close
close

• Matching Nondeterministic Services with Operating Guidelines
Informatik-Berichte, Humboldt-Universität zu Berlin, 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
• Bernd-Holger Schlingloff, Axel Martens, Karsten Schmidt
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

• An Operating Guideline Approach to the SOA
In 2nd South-East European Workshop on Formal Methods 2005 (SEEFM05), Ohrid, Republic of Macedonia, 2005
close

• An Operating Guideline Approach to the SOA
Informatik-Berichte, Humboldt-Universität zu Berlin, 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

• Operating Guidelines - an Alternative to Public View
Informatik-Berichte, Humboldt-Universität zu Berlin, 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
• Karsten Schmidt
Informatik-Berichte, Humboldt-Universität zu Berlin, 2005
close

• Verteilte Geschäftsprozesse modellieren und analysieren
Informatik-Berichte, Humboldt-Universität zu Berlin, feb 2005
Verteilte Geschäftsprozesse nutzen das Internet, um auf heterogenen Rechnerstrukturen Dienste auszubieten. Modellierungstechniken und Implementierungssprachen für solche Dienste werfen im Vergleich mit herkömmlichen Rechnern grundlegend neue Fragestellungen auf. Wir diskutieren einige davon und zeigen, wie Petrinetze ihre Beantwortung ermöglichen.
close
close
• Karsten Schmidt
Controllability of Open Workflow Nets
Jörg Desel and Ulrich Frank, editors
In Enterprise Modelling and Information Systems Architectures, volume P-75 of Lecture Notes in Informatics (LNI), Köllen Druck+Verlag GmbH, Bonn, 2005
close

• 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

• A Petri net semantic for BPEL4WS - validation and application
Ekkart Kindler, editors
In Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN'04), Universität Paderborn, oct 2004
We translated a small business process into a recently defined Petri net semantic. Then we used the tool LoLA for validating the semantic as well as for proving relevant properties of the particular process.
close
close
• Farn Wang, Karsten Schmidt, Fang Yu, Geng-Dian Huang, Bow-Yaw Wang
BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction
volume 30 of IEEE Transactions on Software Engineering (TSE) 30 (6), jun 2004
Dynamic data-structures with pointer links, which are heavily used in real-world software, cause extremely difficult verification problems. Currently, there is no practical framework for the efficient verification of such software systems. We investigated symmetry reduction techniques for the verification of software systems with C-like indirect reference chains like x->y->z->w. We formally defined the model of software with pointer data structures and developed symbolic algorithms to manipulate conditions and assignments with indirect reference chains using BDD technology. We relied on two techniques, inactive variable elimination and process-symmetry reduction in the data-structure configuration, to reduce time and memory complexity. We used binary permutation for efficiency, but we also identified the possibility of an anomaly of false image reachability. We implemented the techniques in tool Red 5.0 and compared performance with Murø and SMC against several benchmarks.
close
close
• Karsten Schmidt
Automated Generation of a Progress Measure for the Sweep-Line Method
In Proc. 10th Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2988 of Lecture Notes in Computer Science, Springer-Verlag, 2004
In the context of Petri nets, we propose an automated construction of a progress measure which is an important pre-requisite for a state space reduction technique called the sweep-line method. Our construction is based on linear-algebraic considerations concerning the transition vectors of the Petri net under consideration.
close
close
• Karsten Schmidt
Distributed Usability of Web Services
In Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN 04), Bericht tr-ri-04-251, Universität Paderborn, 2004
We estabilish a theory of distributed usability. To do so, it is however neccessary to modify the already existing theory of central usability.
close
close
• ### 2003

• Karsten Schmidt
Using Petri Net Invariants in State Space Construction
Hubert Garavel and John Hatcliff, editors
In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), 9th International Conference, Part of ETAPS 2003, volume 2619 of Lecture Notes in Computer Science, Warsaw, Poland, 2003
The linear algebraic invariant calculus is a powerful technique for the verification of Petri nets. Traditionally it is used for structural verification, i.e. for avoiding the explicit construction of a state space. In this paper, we study the use of Petri net invariants for reducing the memory resources required during state space construction. While place invariants help to reduce the amount of memory needed for each single state (without reducing the number of states as such), transition invariants can be used to reduce the number of states to be stored. Interestingly, our approach does not require computing invariants in full, let alone storing them permanently. All information we need can be deduced from an upper triangular form of the Petri net's incidence matrix. Experiments prove that the place invariant technique leads to improvements in both memory and run time costs while transition invariants lead to a space/time tradeoff that can be controlled heuristically.
close
close
• Karsten Schmidt
Distributed Verification with LoLA
volume 54 of Fundamenta Informaticae 54 (2-3), 2003
We report work in progress on a distributed version of explicit state space generation in the Petri net verification tool LoLA. We propose a data structure where all available memory of all involved workstations can be fully exploited, and load balancing actions are possible at any time while the verification is running. It is even possible to extend the set of involved workstations while a verification is running.
close
close
• Lars Michael Kristensen, Karsten Schmidt, Antii Valmari
Question Guided Stubborn Set Methods for State Properties
2003
close
• ### 2002

• Karsten Schmidt
Explicit State Space Verification
Habilitationsschrift, dec 2002
Verification is the task of determining whether a (model of a) system holds a given behavioral property. State space verification comprises a class of computer aided verification techniques where the property is verified through exhaustive exploration of the reachable states of the system. Brute force implementations of state space verification are intractable, due to the well known state explosion problem. Explicit state space verification techniques explore the state space one state at a time, and rely usually on data structures where the size of the data structure increases monotonously with an increasing number of explored states. They alleviate state explosion by constructing a reduced state space that, by a mathematically founded construction, behaves like the original system with respect to the specified properties. Thereby, decrease of the number of states in the reduced system is the core issue of a reduction technique thus reducing the amount of memory required. An explicit state space verification technique comprises of - a theory that establishes whether, and how, certain properties can be preserved through a construction of a reduced state space; - a set of procedures to execute the actual construction efficiently. In this thesis, we contribute to several existing explicit state space verification techniques in either of these two respects. We extend the class of stubborn set methods (an instance of partial order reduction) by constructions that preserve previously unsupported classes of properties. Many existing constructions rely on the existence of "invisible" actions, i.e. actions whose effect does not immediately influence the verified property. We propose efficient constructions that can be applied without having such invisible actions, and prove that they preserve reachability properties as well as certain classes of more complex behavioral system properties. This way, so called "global" properties can now be approached with better stubborn set methods. We pick up a graph automorphism based approach to symmetry reduction and propose a set of construction algorithms that make this approach feasible. In difference to established symmetry techniques that rely on special "symmetry creating" data types, a broader range of symmetries can be handled with our approach thus obtaining smaller reduced state spaces. Coverability graph construction leads to a finite representation of an infinite state space of a Petri net by condensing diverging sequences of states to their limit. We prove rules to determine temporal logic properties of the original system from its coverability graph, far beyond the few properties known to be preserved so far. We employ the Petri net concept of linear algebraic invariants for compressing states as well as for leaving states out of explicit storage. Compression uses place invariants for replacing states by smaller fingerprints that still uniquely identify a state (unlike many hash compression techniques). For reducing the number of explicitly stored states, we rely on the capability of Petri net transition invariants to characterize cycles in the state space. For termination of an exhaustive exploration of a finite state space, it is sufficient to cover all cycles with explicitly stored states. Both techniques are easy consequences of well known facts about invariants. As a novel contribution, we observe that both techniques can be applied without computing an explicit representation of (a generating set for) the respective invariants. This speeds up the constructions considerably and saves a significant amount of memory. For all presented techniques, we illustrate their capabilities to reduce the complexity of state space reduction using a few academic benchmark examples. We address compatibility issues, i.e. the possibility to apply techniques in combination, or in connection with different strategies for exploring the reduced state space. We propose a scheme to distribute state space exploration on a cluster of workstations and discuss consequences for using this scheme for state space reduction. We collect observations concerning the impact of the choice of system description formalisms, and property specification languages, on the availability of explicit state space verification techniques.
close
close
• Farn Wang, Karsten Schmidt
Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures
Doron Peled and Moshe Y. Vardi, editors
In Proc. Int. Conf. Formal Techniques for Networked and Distributed Systems (FORTE 2002), volume 2529 of Lecture Notes in Computer Science, Springer-Verlag, 2002
We formally define the model of software with pointer data structures. We developed symbolic algorithms for the manipulation of conditions and assignments with indirect operands for verification with BDD-like data-structures. We rely on two techniques, including inactive variable elimination and process-symmetry reduction in the data-structure configuration, to contain the time and memory complexity. We use binary permutation for efficiency but also identify the possibility of anomaly of image false reachability. We implemented the techniques in tool red and compare performance with Mur and SMC against several other benchmarks.
close
close
• ### 2001

• Karsten Schmidt
Narrowing Petri Net State Spaces Using the State Equation
volume 47 of Fundamenta Informaticae 47 (3-4), oct 2001
Given a (possibly partially defined) state, all count vectors of transition sequences reaching that state are solutions to a corresponding Petri net state equation. We propose a search strategy where sequences corresponding to a minimal solution of the state equation are explored first. Then step by step the search space is relaxed to arbitrary count vectors. This heuristics relies on the observation that in many (though provably not in all) cases, minimal solutions of the state equation can be realized as a firing sequence. If no target state is reachable, either the state equation does not have solutions, or our search method would yield the full state space. We study the impact of the state equation on reachability, present an algorithm that exploits information from the state equation and discuss its application in stateless search as well as its combination with stubborn set reduction.
close
close
• Karsten Schmidt
Using invariants for state space reduction
In Workshop on Concurrency, Specification and Programming, Warsaw, 2001
close
• ### 2000

• Karsten Schmidt
LoLA: A Low Level Analyser
Mogens Nielsen and Dan Simpson, editors
In Application and Theory of Petri Nets, 21st International Conference (ICATPN 2000), volume 1825 of Lecture Notes in Computer Science, Springer-Verlag, jun 2000
With LoLA, we put recently developed state space oriented algorithms to other tool developers disposal. Providing a simple interface was a major design goal such that it is as easy as possible to integrate LoLA into tools of different application domains. LoLA supports place/transition nets. Implemented verification techniques cover standard properties (liveness, reversibility, boundedness, reachability, dead transitions, deadlocks, home states) as well as satisfiability of state predicates and CTL model checking. For satisfiability, both exhaustive search and heuristically goal oriented system execution are supported. For state space reduction, LoLA features symmetries, stubborn sets, and coverability graphs.
close
close
• Karsten Schmidt
Stubborn Sets for Model Checking the EF/AG Fragment of CTL
volume 43 of Fundamenta Informaticae 43 (1-4), aug 2000
The general stubborn set approach to CTL model checking [2] has the drawback that one either finds a stubborn set with only one enabled transition or one has to expand all enabled transitions. This restriction does not apply in our approach to a fragment of CTL. Furthermore, our reduction does not depend on the invisibility of transitions in a stubborn set.
close
close
• Karsten Schmidt
Flexible net Inscriptions with LoLA
volume 59 of Petri Net Newsletter 59, 2000
close
• Karsten Schmidt
Integrating Low Level Symmetries into Reachability Analysis
Susanne Graf and Michael I. Schwartzbach, editors
In Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, volume 1785 of Lecture Notes in Computer Science, Springer-Verlag, 2000
We present three methods for the integration of symmetries into reachability analysis. Two of them lead to maximal reduction but their runtime depends on the symmetry structure. The third one works always fast but does not always yield maximal reduction.
close
close
• Karsten Schmidt
Narrowing the state space of Petri nets using the state equation
In Workshop on Concurrency, Specification and Programming, Berlin, 2000
close
• Karsten Schmidt
How to Calculate Symmetries of Petri Nets
volume 36 of Acta Informatica 36 (7), 2000