Dirk Fahland

wissenschaftlicher Mitarbeiter am Lehrstuhl Theorie der Programmierung und
Post-Doc in der Gruppe Architecture of Information Systems (Prof. Wil v.d. Aalst) an der TU Eindhoven

Adresse Humboldt-Universität zu Berlin
Institut für Informatik
Unter den Linden 6
10099 Berlin
Kontakt s. homepage an der TU Eindhoven
E-Mail fahland@informatik.hu-berlin.de


seit 11/2010 Post-Doc in der Gruppe Architecture of Information Systems (Prof. Wil v.d. Aalst) an der TU Eindhoven, homepage an der TU Eindhoven
seit 08/2009 wissenschaftlicher Mitarbeiter am Lehrstuhl Theorie der Programmierung
08/2006-09/2010 Promotionsstudent an der TU Eindhoven in der Gruppe Architecture of Information Systems (AIS) im Rahmen des B.E.S.T-Programms
08/2006-07/2009 Kollegiat im Graduiertenkolleg Metrik
08/2005-06/2006 Auslandsjahr an der National University of Singapore
04/2002-07/2005 studentischer Mitarbeiter am Lehrstuhl ToP
10/2001-07/2006 Studium der Informatik an der Humboldt-Universität in Berlin, Abschluß als Diplom-Informatiker

Meine Dissertation From Scenarios To Components ist als .pdf verfügbar.

Aktuelle Informationen über Publikationen, Vorträge und Softwarewerkzeuge sind auf meiner homepage an der TU Eindhoven zu finden.


Aktuell (SS 2010)

WS 2009/10

WS 2006/2007


  • Modellierung und Verifikation verteilter Systeme
  • Szenario-basierter Entwurf von Systemen
  • Service-basierter Entwurf von Systemen
  • Semantik und Nutzbarkeit von Modellierungssprachen

Betreuung von Studien- und Diplomarbeiten

abgeschlossene Arbeiten

  • Alexander Schulz, Adaption szenario-basierter Modelle zur Laufzeit, Diplomarbeit (04/2011)
  • Konstanze Swist, Kosten- und Lastenanalyse von Prozessen im Katastrophenmanagement, Diplomarbeit (03/2010)
  • Manja Wolf, Erstellung einer modellbasierten Laufzeitumgebung fur adaptive Prozesse, Diplomarbeit (11/2008)
  • Konstanze Swist, Modellierung des Workflows der Task Force Erdbeben des GFZ mit Petrinetzen, Studienarbeit (10/2008)
  • Lars Döhling, Equator - Ein Wiki für die Task Force Erdbeben, Studienarbeit (10/2008)
  • Peter Laufer, Public-View-Generierung, Diplomarbeit (11/2007)





  • DSML 2008
  • WS-FM 2007, 2008


  • AICCSA 2008
  • BPM 2007, 2008, 2010
  • CONCUR 2006
  • ECOWS 2007, 2010
  • edBPM 2009
  • FM 2006
  • FMOODS 2009
  • HSCC 2006
  • ICSOC 2009, 2010
  • FORTE 2007
  • Petri Nets 2007, 2008, 2010
  • SOS 2007


  • LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC)
  • Software and Systems Modeling (SOSYM)



  • Dirk Fahland, Christian Gierds
    Analyzing and Completing Middleware Designs for Enterprise Integration Using Coloured Petri Nets
    In CAiSE, 2013
  • Christian Gierds, Dirk Fahland
    Discovering Pattern-Based Mediator Services from Communication Logs
    In WESOA, 2013
  • 2012

  • Dirk Fahland, Christian Gierds
    Using Petri Nets for Modeling Enterprise Integration Patterns
    bpmcenter.org, 2012
  • Dirk Fahland, Robert Prüfer
    Data and Abstraction for Scenario-Based Modeling with Petri Nets
    In Petri Nets, 2012
  • 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.
  • Matthias Weidlich, Stefan Zugal, Jakob Pinggera, Dirk Fahland, Barbara Weber, Hajo Reijers, Jan Mendling
    The Impact of Sequential and Circumstantial Changes on Process Models
    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.
  • Dirk Fahland, Matthias Weidlich
    Scenario-based process modeling with Greta
    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.
  • 2009

  • Dirk Fahland, Jan Mendling, Hajo Reijers, Barbara Weber, Matthias Weidlich, Stefan Zugal
    Declarative vs. Imperative Process Modeling Languages: The Issue of Maintainability
    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.
  • Dirk Fahland, C\'edric Favre, Barbara Jobstmann, Jana Koehler, Niels Lohmann, Hagen Völzer, Karsten Wolf
    Instantaneous Soundness Checking of Industrial Business Process Models
    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
  • 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
    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.
  • Dirk Fahland
    Oclets - scenario-based modeling with Petri nets
    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.
  • Dirk Fahland
    A scenario is a behavioral view - Orchestrating services by scenario integration
    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.
  • 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/.
  • 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.
  • Dirk Fahland
    Adaptive und Selbststabilisierende Workflows
    In Proceedings des gemeinsamen Workshops der Graduiertenkollegs, Trustworthy Software Systems, Gito-Verlag, Berlin, 2008
  • 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.
  • Dirk Fahland
    Oclets -- Scenario-Based Modeling with Petri Nets
    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.
  • 2007

  • Dirk Fahland
    Modeling and Verifying Declarative Workflows
    In Dagstuhl ''zehn plus eins'', Verlagshaus Mainz, Aachen, 2007
  • Wolfgang Reisig, Jan Bretschneider, Dirk Fahland, Niels Lohmann, Peter Massuthe, Christian Stahl
    Services as a Paradigm of Computation
    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.
  • Dirk Fahland
    Synthesizing Petri nets from LTL specifications - An engineering approach
    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.
  • Dirk Fahland
    A Formal Approach to Adaptive Processes using Scenario-based Concepts.
    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.
  • Dirk Fahland
    Towards Analyzing Declarative Workflows
    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.
  • 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.
  • 2006

  • Wolfgang Reisig, Dirk Fahland, Niels Lohmann, Peter Massuthe, Christian Stahl, Daniela Weinberg, Karsten Wolf, Kathrin Kaschner
    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.
  • 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.
  • 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.
  • Dirk Fahland, Wolfgang Reisig
    ASM-based semantics for BPEL: The negative Control Flow
    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.
  • 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.
  • 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.