Publikationen (nach Gebiet sortiert)

Adaptive/flexible Workflows (13)

Adaptive/flexible Workflows

    Konferenzbeiträge auf Workshops

  • Fahland, Dirk, Weidlich, Matthias
    Scenario-based process modeling with Greta
    Marcello La Rosa, editors
    In Proc. of BPM Demonstration Track 2010, Hoboken, USA, September 14-16, 2010, volume 615 of CEUR-WS.org, Hoboken, USA, September 2010
    Designing understandable business process models is one of the key factors to successful business process management. Current modeling practices advocate the use of block-oriented concepts and subprocesses to structure complex process models. However, such guidelines cannot be applied in any case as case studies in process mining have shown. Previously, we proposed the scenario-based paradigm to structure models of complex processes in behavioral fragments, i.e., scenarios. This paper presents GRETA as a tool that supports scenario-based process modeling and execution.
    close
    close
  • Fahland, Dirk
    Oclets - scenario-based modeling with Petri nets
    Giuliana Franceschinis and Karsten Wolf, editors
    In Proceedings of the 30th International Conference on Petri Nets and Other Models Of Concurrency, 22-26 May 2009, volume 5606 of Lecture Notes in Computer Science, Springer-Verlag, Paris, France, jun 2009
    We present a novel, operational, formal model for scenario-based modeling with Petri nets. A scenario-based model describes the system behavior in terms of partial runs, called scenarios. This paradigm has been formalized in message sequence charts (MSCs) and live sequence charts (LSCs) which are in industrial and academic use. A particular application for scenarios are process models in disaster management where system behavior has to be adapted frequently, occasionally at run-time. An operational semantics of scenarios would allow to execute and adapt such systems on a formal basis. In this paper, we present a class of Petri nets for specifying and modeling systems with scenarios and anti-scenarios. We provide an operational semantics allowing to iteratively construct partially ordered runs that satisfy a given specification. We prove the correctness of our results.
    close
    close
  • Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
    Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
    John Krogstie and Terry Halpin and Erik Proper, editors
    In Proceedings of the 14th International Conference on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD'09), volume 29 of Lecture Notes in Business Information Processing, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
    Advantages and shortcomings of different process modeling languages are heavily debated, both in academia and industry, but little evidence is presented to support judgements. With this paper we aim to contribute to a more rigorous, theoretical discussion of the topic by drawing a link to well-established research on program comprehension. In particular, we focus on imperative and declarative techniques of modeling a process. Cognitive research has demonstrated that imperative programs deliver sequential information much better while declarative programs offer clear insight into circumstantial information. In this paper we show that in principle this argument can be transferred to respective features of process modeling languages. Our contribution is a pair of propositions that are routed in the cognitive dimensions framework. In future research, we aim to challenge these propositions by an experiment.
    close
    close
  • Fahland, Dirk, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
    Declarative vs. Imperative Process Modeling Languages: The Issue of Maintainability
    Stefanie Rinderle-Ma and Shazia Wasim Sadiq and Frank Leymann, editors
    In Business Process Management Workshops, BPM 2009 International Workshops, Ulm, Germany, September 7, 2009. Revised Papers, volume 43 of Lecture Notes in Business Information Processing, Springer, Ulm, Germany, sep 2009
    The rise of interest in declarative languages for process modeling both justifies and demands empirical investigations into their presumed advantages over more traditional, imperative alternatives. Our concern in this paper is with the ease of maintaining business process models, for example due to changing performance or conformance demands. We aim to contribute to a rigorous, theoretical discussion of this topic by drawing a link to well-established research on maintainability of information artifacts.
    close
    close
  • Fahland, Dirk, Woith, Heiko
    Towards Process Models for Disaster Response
    In Business Process Management Workshops, International Workshop on Process Management for Highly Dynamic and Pervasive Scenarios (PM4HDPS), co-located with 6th International Conference on Business Process Management (BPM'08), volume 17 of Lecture Notes in Business Information Processing, Springer, Milan, Italy, September 2008
    In the immediate aftermath of a disaster routine processes, even if specifically designed for such a situation, are not enacted blindly. Actions and processes rather adapt their behavior based on observations and available information. Attempts to support these processes by technology rely on process models that faithfully capture process execution and adaptation. Based on experiences from actual disaster response settings, we propose to specify an adaptive process as a set of scenarios using a Petri net syntax. Our operational model provides an adaptation operator that synthesizes and adapts the system behavior at run-time based on the given scenarios. An example illustrates our approach.
    close
    close
  • Fahland, Dirk
    Adaptive und Selbststabilisierende Workflows
    Diehl, Malte and Lipskoch, Henrik and Meyer, Roland and Storm, Christian, editors
    In Proceedings des gemeinsamen Workshops der Graduiertenkollegs, Trustworthy Software Systems, Gito-Verlag, Berlin, 2008
    close
  • Fahland, Dirk
    Oclets -- Scenario-Based Modeling with Petri Nets
    Niels Lohmann and Karsten Wolf, editors
    In Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008, volume 380 of CEUR Workshop Proceedings, CEUR-WS.org, sep 2008
    Scenario-based specifications are used for modeling highly-complex, distributed systems in terms of partial runs (scenarios) the system shall have. But it is difficult to derive an implementing, operational model from a given set of scenarios, especially if concepts like anti-scenarios which must not occur are used. In this paper, we present a novel model for scenario-based specifications with Petri nets including anti-scenarios; we provide an operational semantics for our model.
    close
    close
  • Fahland, Dirk
    A Formal Approach to Adaptive Processes using Scenario-based Concepts.
    Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
    In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, Siedlce, Poland, jun 2007
    The problem and need for adapting business processes and service behavior to cope with changing circumstances is identified well. Standard models for business processes still rely on a fixed process logic, the change of which is rather hard to achieve. Ad-hoc changes to a standard model are usually considered too `dangerous' as they are performed in not well-defined manner. Other models for adaptive processes deviate to some extent from established business process models. This deviation comes at the price of limited understandability and loss in analysis capabilities. We propose a model for adaptive processes based on Petri nets which have successfully been applied in modeling and analyzing business process and web services. Our operator to adapt the behavior of such models is formalized by the help of scenario-based concepts known from live-sequence charts in purely mathematical terms. This combination of concepts allows to write down the result of the adaptation rather than how adaptation shall be performed.
    close
    close
  • Fahland, Dirk
    Synthesizing Petri nets from LTL specifications - An engineering approach
    Philippi, Stephan and Pinl, Alexander, editors
    In , , September 2007
    close
    close
  • Fahland, Dirk
    Modeling and Verifying Declarative Workflows
    In Dagstuhl ''zehn plus eins'', Verlagshaus Mainz, Aachen, 2007
    close
  • Fahland, Dirk
    Towards Analyzing Declarative Workflows
    Jana Koehler and Marco Pistore and Amit P. Sheth and Paolo Traverso and Martin Wirsing, editors
    In Autonomous and Adaptive Web Services, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007
    Enacting tasks in a workflow cannot always follow a pre-defined process model. In application domains like disaster management workflows are partially specified and circumstances of their enactment change. There exist various approaches for formal workflow models that are effective in such situations, like declarative specifications instead of operational models for formalizing flexible workflow process. These powerful models leave a gap to existing techniques in the domain of workflow modeling, workflow analysis, and workflow management. In this paper we bridge this gap with a compositional mechanism for translating declarative workflow models to operational workflow models. The mechanism is of a general nature and we reveal its principles as we provide an exemplary definition for translating DecSerFlow models based on LTL to Petri nets. We then demonstrate its use in analyzing and refining declarative models.
    close
    close
  • Studien- und Diplomarbeiten

  • Wolf, Manja

    Diplomarbeit, sep 2008
    close
    close
  • Technische Berichte

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

Architecture Framework (6)

Architecture Framework

    Konferenzbeiträge auf Workshops

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

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

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

Asm (15)

Asm

    Konferenzbeiträge auf Workshops

  • Glausch, Andreas, Reisig, Wolfgang
    A Semantic Characterization of Unbounded-Nondeterministic ASMs
    In Proceedings of the 2nd Conference on Algebra and Coalgebra in Computer Science, volume 4624 of Lecture Notes in Computer Science, aug 2007
    Universal algebra usually considers and examines algebras as static entities. In the mid 80ies Gurevich proposed Abstract State Machines (ASMs) as a computation model that regards algebras as dynamic: a state of an ASM is represented by a freely chosen algebra which may change during a computation. In 2000, Gurevich characterized the class of sequential ASMs in a purely semantical way by five amazingly general and elegant axioms. Later this result has been extended to bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among unboundedly many (sometimes infinitely many) alternatives. We characterize the class of unbounded-nondeterministic ASMs by an extension of Gurevich's original axioms for sequential ASMs. We apply this result to prove the reversibility of unbounded-nondeterministic ASMs.
    close
    close
  • Glausch, Andreas
    A Semantic Characterization of Elementary Wide-Step ASMs
    In Proceedings of the 14th International ASM Workshop, jun 2007
    close
  • Fahland, Dirk, Reisig, Wolfgang
    ASM-based semantics for BPEL: The negative Control Flow
    , editors
    In Proceedings of the 12th International Workshop on Abstract State Machines (ASM'05), Paris XII, mar 2005
    BPEL is presently the most prominent language to specify and execute business processes, using Web Services as its technological basis. Particular problems arise when activities are faulty: faults have to be propagated, other activities have to be irregularly terminated, etc. We describe the formal semantics of fault handlers and event handlers, demonstrating that ASMs are most adequate for this purpose.
    close
    close
  • Reisig, Wolfgang
    The Computable Kernel of ASM
    , editors
    In Abstract State Machines, Advances in Theory and Practice, 10th International Workshop, ASM 2003, Taormina, Italy, volume 2589 of Lecture Notes in Computer Science, 2003
    A rich variety of system models for sequential, deterministic systems has been suggested during recent decades, including automata, process algebras, many versions of Petri Nets, and models to describe the semantics of Programming languages. All models for sequential, deterministic systems assume a set S of states, or configurations, and a next state function $\upsilon: S \rightarrow S$.
    close
    close
  • Reisig, Wolfgang
    Towards an ASM Thesis for Unconventional Algorithms
    Yuri Gurevich and Philipp W. Kutter and Martin Odersky and Lothar Thiele, editors
    In Abstract State Machines, volume 1912 of Lecture Notes in Computer Science, Springer-Verlag, 2000
    All descriptions of algorithms, be they formal or informal, employ data structures, operations on them, and some policy to cause operations be applied to data. Gurevich calls a formal description technique for algorithms algorithm universal if it allows for each informally described algorithm a formal representation that would essentially make precise the notions used in the informal description, not employing additional data, operations or steps. Gurevich's ASM thesis claims Abstract State Machines be algorithm universal for conventional, sequential algorithms. Here we are behind properties of formal presentations that are algorithm universal for unconventional, distributed algorithms.
    close
    close
  • Publikationen in Zeitschriften und Büchern

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

  • Brade, Alexander

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

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

Bdd (2)

Bdd

    Konferenzbeiträge auf Workshops

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

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

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

Bedienbarkeit (9)

Bedienbarkeit

    Konferenzbeiträge auf Workshops

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

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


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

    Studienarbeit, oct 2007
    close
    close
  • Technische Berichte

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

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

Bedienungsanleitung (9)

Bedienungsanleitung

    Dissertationen und Habilitationen

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

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

  • Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
    Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
    volume 53 of The Computer Journal 53 (1), 2010
    To implement an interorganizational process between different enterprizes, one needs to agree on the ``rules of engagement''. These can be specified in terms of a contract that describes the overall intended process and the duties of all parties involved. We propose to use such a process-oriented contract which can be seen as the composition of the public views of all participating parties. Based on this contract each party may locally implement its part of the contract such that the implementation (the private view) agrees on the contract. In this paper, we propose a formal notion for such process-oriented contracts and give a criterion for accordance between a private view and its public view. The public view of a party can be substituted by a private view if and only if the private view accords with the public view. Using the notion of accordance the overall implemented process is guaranteed to be deadlock-free and it is always possible to terminate properly. In addition, we present a technique for automatically checking our accordance criterion. A case study illustrates how our proposed approach can be used in practice.
    close
    close
  • Stahl, Christian, Wolf, Karsten
    Deciding Service Composition and Substitutability Using Extended Operating Guidelines
    volume 68 of Data Knowl. Eng. 68 (9), 2009
    We study the correct interaction between services using the following notion for correctness: there is no deadlock in the interaction of the services, and a given set of activities is not dead, that is, each activity in this set is executed in at least one run. The second condition has not been studied before. An operating guideline of a service P is an operational characterization of all deadlock-free interacting partners of P. In this paper, we present an extension of the concept of an operating guideline to characterize all correctly interacting partners of a service P. This extension can be used for answering at least the following two questions. First, given a service R, does R interact correctly with P? Second, given a service P', can P be substituted by P', that is, is every correctly interacting partner of P a correctly interacting partner of P', too?
    close
    close
  • Stahl, Christian, Massuthe, Peter, Bretschneider, Jan
    Deciding Substitutability of Services with Operating Guidelines
    Kurt Jensen and Wil M. P. van der Aalst, editors
    volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2 (5460), Springer-Verlag, mar 2009
    Deciding whether a service S can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of restriction can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
    close
    close
  • Studien- und Diplomarbeiten

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

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

Bpel (29)

Bpel

    Konferenzbeiträge auf Workshops

  • Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
    Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
    John Krogstie and Terry Halpin and Erik Proper, editors
    In Proceedings of the 14th International Conference on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD'09), volume 29 of Lecture Notes in Business Information Processing, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
    Advantages and shortcomings of different process modeling languages are heavily debated, both in academia and industry, but little evidence is presented to support judgements. With this paper we aim to contribute to a more rigorous, theoretical discussion of the topic by drawing a link to well-established research on program comprehension. In particular, we focus on imperative and declarative techniques of modeling a process. Cognitive research has demonstrated that imperative programs deliver sequential information much better while declarative programs offer clear insight into circumstantial information. In this paper we show that in principle this argument can be transferred to respective features of process modeling languages. Our contribution is a pair of propositions that are routed in the cognitive dimensions framework. In future research, we aim to challenge these propositions by an experiment.
    close
    close
  • König, Dieter, Lohmann, Niels, Moser, Simon, Stahl, Christian, Wolf, Karsten
    Extending the Compatibility Notion for Abstract WS-BPEL Processes
    Wei-Ying Ma and Andrew Tomkins and Xiaodong Zhang, editors
    In Proceedings of the 17th International Conference on World Wide Web, WWW 2008, Beijing, China, April 21--25, 2008, apr 2008
    WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.
    close
    close
  • Lohmann, Niels
    A Feature-Complete Petri Net Semantics for WS-BPEL 2.0
    Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
    In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, jun 2007
    We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.
    close
    close
  • Reisig, Wolfgang, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela, Wolf, Karsten, Kaschner, Kathrin
    Analysis Techniques for Service Models
    In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, IEEE Computer Society, nov 2006
    The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.
    close
    close
  • Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela
    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
  • Fahland, Dirk, Reisig, Wolfgang
    ASM-based semantics for BPEL: The negative Control Flow
    , editors
    In Proceedings of the 12th International Workshop on Abstract State Machines (ASM'05), Paris XII, mar 2005
    BPEL is presently the most prominent language to specify and execute business processes, using Web Services as its technological basis. Particular problems arise when activities are faulty: faults have to be propagated, other activities have to be irregularly terminated, etc. We describe the formal semantics of fault handlers and event handlers, demonstrating that ASMs are most adequate for this purpose.
    close
    close
  • Martens, Axel
    Simulation and Equivalence between BPEL Process Models
    In Proceedings of the Design, Analysis, and Simulation of Distributed Systems Symposium (DASD'05), Part of the 2005 Spring Simulation Multiconference (SpringSim'05), San Diego, California, apr 2005
    The integration of business process across the boundaries of individual enterprises or business units is becoming increasingly important. In this scenario, process models play an all-important role. On the one hand, the interaction between the participating companies often is specified globally, for example by means of multiple abstract process models - one for each partner. On the other hand, each partner defines its local process autonomously in terms of an executable process model. The important question is whether such an executable model is consistent to the predefined abstract model. This paper defines a simulation relation between BPEL process models, and presents a method to verify consistency automatically, on top of it.
    close
    close
  • Hinz, Sebastian, Schmidt, Karsten, Stahl, Christian
    Transforming BPEL to Petri Nets
    Wil M. P. van der Aalst and B. Benatallah and F. Casati and F. Curbera, editors
    In Proceedings of the Third International Conference on Business Process Management (BPM 2005), volume 3649 of Lecture Notes in Computer Science, Springer-Verlag, Nancy, France, sep 2005
    We present a Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation). The semantics is implemented as a parser that translates BPEL specifications into the input language of the Petri net model checking tool LoLA. We demonstrate that the semantics is well suited for computer aided verification purposes.
    close
    close
  • Schmidt, Karsten, Stahl, Christian
    A Petri net semantic for BPEL4WS - validation and application
    Ekkart Kindler, editors
    In Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN'04), , oct 2004
    We translated a small business process into a recently defined Petri net semantic. Then we used the tool LoLA for validating the semantic as well as for proving relevant properties of the particular process.
    close
    close
  • Publikationen in Zeitschriften und Büchern

  • Lohmann, Niels, Verbeek, Eric, Ouyang, Chun, Stahl, Christian
    Comparing and Evaluating Petri Net Semantics for BPEL
    volume 4 of International Journal of Business Process Integration and Management (IJBPIM) 4 (1), 2009
    We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modelling decisions. These decisions together with their consequences are discussed. We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.
    close
    close
  • Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela
    Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation
    volume 64 of Data Knowl. Eng. 64 (1), jan 2008
    We address the problem of analyzing the interaction between WS-BPEL processes. We present a technology chain that starts out with a WS-BPEL process and translates it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). To manage processes of realistic size, we present a concept of a \emphflexible model generation which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.
    close
    close
  • Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian
    Kommunizierende Workflow-Services modellieren und analysieren
    Informatik - Forschung und Entwicklung, Springer-Verlag, oct 2005
    close
    close
  • Vidal, Jose M., Buhler, Paul, Stahl, Christian
    Multiagent Systems with Workflows
    volume 8 of IEEE Internet Computing 8 (1), feb 2004
    Industry and researchers have two different visions for the future of Web services. Industry wants to capitalize on Web service technology to automate business processes via centralized workflow enactment. Researchers are interested in the dynamic composition of Web services. The authors show how these two visions are points in a continuum and discuss a possible path for bridging the gap between them.
    close
    close
  • Studien- und Diplomarbeiten



  • Diplomarbeit, mar 2008
    close
    close
  • Kleine, Jens

    Studienarbeit, oct 2006
    close
    close
  • Laufer, Peter

    Studienarbeit, may 2006
    close
    close
  • Hinz, Sebastian

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

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

    Studienarbeit, aug 2003
    close
  • Technische Berichte

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

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

Bpel-semantik (18)

Bpel-semantik

    Konferenzbeiträge auf Workshops

  • König, Dieter, Lohmann, Niels, Moser, Simon, Stahl, Christian, Wolf, Karsten
    Extending the Compatibility Notion for Abstract WS-BPEL Processes
    Wei-Ying Ma and Andrew Tomkins and Xiaodong Zhang, editors
    In Proceedings of the 17th International Conference on World Wide Web, WWW 2008, Beijing, China, April 21--25, 2008, apr 2008
    WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.
    close
    close
  • Lohmann, Niels
    A Feature-Complete Petri Net Semantics for WS-BPEL 2.0
    Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
    In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, jun 2007
    We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.
    close
    close
  • Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela
    Analyzing Interacting BPEL Processes
    In Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings, volume 4102 of Lecture Notes in Computer Science, Springer-Verlag, sep 2006
    This paper addresses the problem of analyzing theinteraction between BPEL processes. We present a technology chain that starts out with a BPEL process and transforms it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). A case study demonstrates the value of this technology chain.
    close
    close
  • Hinz, Sebastian, Schmidt, Karsten, Stahl, Christian
    Transforming BPEL to Petri Nets
    Wil M. P. van der Aalst and B. Benatallah and F. Casati and F. Curbera, editors
    In Proceedings of the Third International Conference on Business Process Management (BPM 2005), volume 3649 of Lecture Notes in Computer Science, Springer-Verlag, Nancy, France, sep 2005
    We present a Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation). The semantics is implemented as a parser that translates BPEL specifications into the input language of the Petri net model checking tool LoLA. We demonstrate that the semantics is well suited for computer aided verification purposes.
    close
    close
  • Fahland, Dirk, Reisig, Wolfgang
    ASM-based semantics for BPEL: The negative Control Flow
    , editors
    In Proceedings of the 12th International Workshop on Abstract State Machines (ASM'05), Paris XII, mar 2005
    BPEL is presently the most prominent language to specify and execute business processes, using Web Services as its technological basis. Particular problems arise when activities are faulty: faults have to be propagated, other activities have to be irregularly terminated, etc. We describe the formal semantics of fault handlers and event handlers, demonstrating that ASMs are most adequate for this purpose.
    close
    close
  • Schmidt, Karsten, Stahl, Christian
    A Petri net semantic for BPEL4WS - validation and application
    Ekkart Kindler, editors
    In Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN'04), , oct 2004
    We translated a small business process into a recently defined Petri net semantic. Then we used the tool LoLA for validating the semantic as well as for proving relevant properties of the particular process.
    close
    close
  • Publikationen in Zeitschriften und Büchern

  • Lohmann, Niels, Verbeek, Eric, Ouyang, Chun, Stahl, Christian
    Comparing and Evaluating Petri Net Semantics for BPEL
    volume 4 of International Journal of Business Process Integration and Management (IJBPIM) 4 (1), 2009
    We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modelling decisions. These decisions together with their consequences are discussed. We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.
    close
    close
  • Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela
    Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation
    volume 64 of Data Knowl. Eng. 64 (1), jan 2008
    We address the problem of analyzing the interaction between WS-BPEL processes. We present a technology chain that starts out with a WS-BPEL process and translates it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). To manage processes of realistic size, we present a concept of a \emphflexible model generation which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.
    close
    close
  • Studien- und Diplomarbeiten

  • Laufer, Peter

    Studienarbeit, may 2006
    close
    close
  • Kleine, Jens

    Studienarbeit, oct 2006
    close
    close
  • Hinz, Sebastian

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

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

Dawn (6)

Dawn

    Konferenzbeiträge auf Workshops

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

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

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

    Diplomarbeit, oct 1999
    close
  • Technische Berichte

  • Baar, Thomas, Kindler, Ekkart
    Einsatz von ILF und DAWN zur Verifikation verteilter Algorithmen - Eine Vorstudie
    Informatik-Berichte, , mar 1998
    close
  • Weber, Michael, Walter, Rolf, , Vesper, Tobias, Reisig, Wolfgang, Peuker, Sibylle, Kindler, Ekkart, ,
    DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen
    Informatik-Berichte, , dec 1997
    close

Deklarative Modelle (5)

Deklarative Modelle

    Konferenzbeiträge auf Workshops

  • Fahland, Dirk, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
    Declarative vs. Imperative Process Modeling Languages: The Issue of Maintainability
    Stefanie Rinderle-Ma and Shazia Wasim Sadiq and Frank Leymann, editors
    In Business Process Management Workshops, BPM 2009 International Workshops, Ulm, Germany, September 7, 2009. Revised Papers, volume 43 of Lecture Notes in Business Information Processing, Springer, Ulm, Germany, sep 2009
    The rise of interest in declarative languages for process modeling both justifies and demands empirical investigations into their presumed advantages over more traditional, imperative alternatives. Our concern in this paper is with the ease of maintaining business process models, for example due to changing performance or conformance demands. We aim to contribute to a rigorous, theoretical discussion of this topic by drawing a link to well-established research on maintainability of information artifacts.
    close
    close
  • Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
    Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
    John Krogstie and Terry Halpin and Erik Proper, editors
    In Proceedings of the 14th International Conference on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD'09), volume 29 of Lecture Notes in Business Information Processing, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
    Advantages and shortcomings of different process modeling languages are heavily debated, both in academia and industry, but little evidence is presented to support judgements. With this paper we aim to contribute to a more rigorous, theoretical discussion of the topic by drawing a link to well-established research on program comprehension. In particular, we focus on imperative and declarative techniques of modeling a process. Cognitive research has demonstrated that imperative programs deliver sequential information much better while declarative programs offer clear insight into circumstantial information. In this paper we show that in principle this argument can be transferred to respective features of process modeling languages. Our contribution is a pair of propositions that are routed in the cognitive dimensions framework. In future research, we aim to challenge these propositions by an experiment.
    close
    close
  • Fahland, Dirk
    Modeling and Verifying Declarative Workflows
    In Dagstuhl ''zehn plus eins'', Verlagshaus Mainz, Aachen, 2007
    close
  • Fahland, Dirk
    Synthesizing Petri nets from LTL specifications - An engineering approach
    Philippi, Stephan and Pinl, Alexander, editors
    In , , September 2007
    close
    close
  • Fahland, Dirk
    Towards Analyzing Declarative Workflows
    Jana Koehler and Marco Pistore and Amit P. Sheth and Paolo Traverso and Martin Wirsing, editors
    In Autonomous and Adaptive Web Services, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007
    Enacting tasks in a workflow cannot always follow a pre-defined process model. In application domains like disaster management workflows are partially specified and circumstances of their enactment change. There exist various approaches for formal workflow models that are effective in such situations, like declarative specifications instead of operational models for formalizing flexible workflow process. These powerful models leave a gap to existing techniques in the domain of workflow modeling, workflow analysis, and workflow management. In this paper we bridge this gap with a compositional mechanism for translating declarative workflow models to operational workflow models. The mechanism is of a general nature and we reveal its principles as we provide an exemplary definition for translating DecSerFlow models based on LTL to Petri nets. We then demonstrate its use in analyzing and refining declarative models.
    close
    close

Exchangeability (15)

Exchangeability

    Dissertationen und Habilitationen

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

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

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

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

Gals (8)

Gals

    Konferenzbeiträge auf Workshops

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

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

  • Julius, Alexandra

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

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

Interaktionsgraph (1)

Interaktionsgraph

    Studien- und Diplomarbeiten


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

Lola (3)

Lola

    Konferenzbeiträge auf Workshops

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

  • Fahland, Dirk
    Translating UML2 Activity Diagrams Petri Nets for analyzing IBM WebSphere Business Modeler process models
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2008
    We present a formal semantics for a variant of UML2 Activity Diagrams that is used in the IBM WebSphere Business Modeler for modeling business processes. Business process models created in the IBM WebSphere Business Modeler or with other UML2 modeling tools often constitutes one of the key specification artifacts for building an information system that implements or supports the specified processes. As UML2 Activity Diagrams lack a universally agreed semantics, the step from specification to implementation usually faces a semantical impedance caused by different interpretation of the same diagram. A well-defined formal semantics for the specification language determines the interpretation of a diagram and allows for reasoning about as well as validating and verifying a given specification on common (formal) grounds. We adapt approaches for formalizing semantics of UML2 Activity Diagrams and apply them to the core features of the IBM WebSphere Business Modeler language for purpose of formal verification. We provide a parameterized Petri net pattern for each language concepts. A diagram is translated by instantiating a pattern for each use of a concept; merging the resulting Petri net fragments according to the structure of the original diagram yields a Petri net that specifies the behavioral semantics of the diagram. The resulting Petri net can be verified for control-flow errors using the model checker LoLA. The semantics has been implemented in a tool that is available at http://www.service-technology.org/uml2owfn/.
    close
    close
  • Stahl, Christian, Reisig, Wolfgang, Krstic, Milos
    Hazard Detection in a GALS Wrapper: a Case study
    Informatik-Berichte, , feb 2005
    An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion three techniques to reduce the model?s state space are presented. By use of these techniques we detected several potential hazards in the wrapper.
    close
    close

Matching (12)

Matching

    Konferenzbeiträge auf Workshops

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

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

  • Stahl, Christian, Wolf, Karsten
    Deciding Service Composition and Substitutability Using Extended Operating Guidelines
    volume 68 of Data Knowl. Eng. 68 (9), 2009
    We study the correct interaction between services using the following notion for correctness: there is no deadlock in the interaction of the services, and a given set of activities is not dead, that is, each activity in this set is executed in at least one run. The second condition has not been studied before. An operating guideline of a service P is an operational characterization of all deadlock-free interacting partners of P. In this paper, we present an extension of the concept of an operating guideline to characterize all correctly interacting partners of a service P. This extension can be used for answering at least the following two questions. First, given a service R, does R interact correctly with P? Second, given a service P', can P be substituted by P', that is, is every correctly interacting partner of P a correctly interacting partner of P', too?
    close
    close
  • Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela
    Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation
    volume 64 of Data Knowl. Eng. 64 (1), jan 2008
    We address the problem of analyzing the interaction between WS-BPEL processes. We present a technology chain that starts out with a WS-BPEL process and translates it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). To manage processes of realistic size, we present a concept of a \emphflexible model generation which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.
    close
    close
  • Massuthe, Peter, Wolf, Karsten
    An Algorithm for Matching Non-deterministic Services with Operating Guidelines
    volume 2 of International Journal of Business Process Integration and Management (IJBPIM) 2 (2), 2007
    Interorganisational cooperation is more and more organised by the paradigm of services. Service-Oriented Architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester and the service broker, together with the three operations publish, find and bind. We provide a formal method based on non-deterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artefact to realise the publish operation. In our approach, the find operation reduces to a matching problem between the requesters service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free interaction. In this paper, matching of deterministic as well as non-deterministic automata with operating guidelines is presented.
    close
    close
  • Technische Berichte

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

Offene Workflownetze (5)

Offene Workflownetze

    Dissertationen und Habilitationen

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

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

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

Open Workflow Nets (1)

Open Workflow Nets

    Konferenzbeiträge auf Workshops

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

Operating Guidelines (24)

Operating Guidelines

    Konferenzbeiträge auf Workshops

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

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

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

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

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

Owfn (1)

Owfn

    Studien- und Diplomarbeiten

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

Owfns (15)

Owfns

    Konferenzbeiträge auf Workshops

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

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


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

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

    Studienarbeit, oct 2007
    close
    close
  • Technische Berichte

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

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

Petri Net Analysis; Inductive Invariants; Linear Inequalities; Stable Properties; Traps; Co-traps; Invariants (1)

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

    Publikationen in Zeitschriften und Büchern

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

Petri Net Kernel (13)

Petri Net Kernel

    Dokumentationen

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

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

    J. Desel, A. Oberweis, editors
    In , , oct 1999
    close
  • Kindler, Ekkart, Weber, Michael

    E. Schnieder, editors
    In Entwicklung und Betrieb komplexer Automatisierungssysteme, 6. Fachtagung, Band II, may 1999
    close
  • Kindler, Ekkart, Weber, Michael
    The Petri Net Kernel - An Infrastructure for Building Petri Net Tools
    In 20th International Conference on Application and Theory of Petri Nets - Petri Net Tool Presentations, College of William and Mary, Williamsburg, Virginia, USA, jun 1999
    The Petri Net Kernel is an infrastructure for building Petri net tools. It relieves the programmer of a Petri net tool from implementing standard functionality on Petri nets. In this paper, we briefly discuss the motivation, the concepts, and the realization of the Petri Net Kernel.
    close
    close
  • Kindler, Ekkart
    Der Petrinetz-Kern: Ein Traum wird wahr
    1997
    close
  • Kindler, Ekkart,
    Der Traum von einem universellen Petrinetz-Werkzeug - Der Petrinetz-Kern
    , editors
    In , , oct 1996
    close
  • Publikationen in Zeitschriften und Büchern

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

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

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

Petrinetze (22)

Petrinetze

    Konferenzbeiträge auf Workshops

  • Fahland, Dirk, Weidlich, Matthias
    Scenario-based process modeling with Greta
    Marcello La Rosa, editors
    In Proc. of BPM Demonstration Track 2010, Hoboken, USA, September 14-16, 2010, volume 615 of CEUR-WS.org, Hoboken, USA, September 2010
    Designing understandable business process models is one of the key factors to successful business process management. Current modeling practices advocate the use of block-oriented concepts and subprocesses to structure complex process models. However, such guidelines cannot be applied in any case as case studies in process mining have shown. Previously, we proposed the scenario-based paradigm to structure models of complex processes in behavioral fragments, i.e., scenarios. This paper presents GRETA as a tool that supports scenario-based process modeling and execution.
    close
    close
  • Fahland, Dirk
    Oclets - scenario-based modeling with Petri nets
    Giuliana Franceschinis and Karsten Wolf, editors
    In Proceedings of the 30th International Conference on Petri Nets and Other Models Of Concurrency, 22-26 May 2009, volume 5606 of Lecture Notes in Computer Science, Springer-Verlag, Paris, France, jun 2009
    We present a novel, operational, formal model for scenario-based modeling with Petri nets. A scenario-based model describes the system behavior in terms of partial runs, called scenarios. This paradigm has been formalized in message sequence charts (MSCs) and live sequence charts (LSCs) which are in industrial and academic use. A particular application for scenarios are process models in disaster management where system behavior has to be adapted frequently, occasionally at run-time. An operational semantics of scenarios would allow to execute and adapt such systems on a formal basis. In this paper, we present a class of Petri nets for specifying and modeling systems with scenarios and anti-scenarios. We provide an operational semantics allowing to iteratively construct partially ordered runs that satisfy a given specification. We prove the correctness of our results.
    close
    close
  • Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
    Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
    John Krogstie and Terry Halpin and Erik Proper, editors
    In Proceedings of the 14th International Conference on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD'09), volume 29 of Lecture Notes in Business Information Processing, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
    Advantages and shortcomings of different process modeling languages are heavily debated, both in academia and industry, but little evidence is presented to support judgements. With this paper we aim to contribute to a more rigorous, theoretical discussion of the topic by drawing a link to well-established research on program comprehension. In particular, we focus on imperative and declarative techniques of modeling a process. Cognitive research has demonstrated that imperative programs deliver sequential information much better while declarative programs offer clear insight into circumstantial information. In this paper we show that in principle this argument can be transferred to respective features of process modeling languages. Our contribution is a pair of propositions that are routed in the cognitive dimensions framework. In future research, we aim to challenge these propositions by an experiment.
    close
    close
  • Fahland, Dirk, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
    Declarative vs. Imperative Process Modeling Languages: The Issue of Maintainability
    Stefanie Rinderle-Ma and Shazia Wasim Sadiq and Frank Leymann, editors
    In Business Process Management Workshops, BPM 2009 International Workshops, Ulm, Germany, September 7, 2009. Revised Papers, volume 43 of Lecture Notes in Business Information Processing, Springer, Ulm, Germany, sep 2009
    The rise of interest in declarative languages for process modeling both justifies and demands empirical investigations into their presumed advantages over more traditional, imperative alternatives. Our concern in this paper is with the ease of maintaining business process models, for example due to changing performance or conformance demands. We aim to contribute to a rigorous, theoretical discussion of this topic by drawing a link to well-established research on maintainability of information artifacts.
    close
    close
  • Fahland, Dirk
    A scenario is a behavioral view - Orchestrating services by scenario integration
    Oliver Kopp and Niels Lohmann, editors
    In Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, mar 2009
    The construction of a complex service orchestration is a tedious and error-prone task as multiple service interactions with a single orchestrating service must be specifi ed and combined. We suggest to specify a service orchestration in terms of behavioral scenarios that capture a specifi c aspect of service interaction, a behavioral view in isolation. By synchronizing the different scenarios, the views get integrated and define the behavior of a complex service orchestration. Our formal model for scenarios and their integration is a class of Petri nets called oclets.
    close
    close
  • Fahland, Dirk, Favre, C\'edric, Jobstmann, Barbara, Koehler, Jana, Lohmann, Niels, Völzer, Hagen, Wolf, Karsten
    Instantaneous Soundness Checking of Industrial Business Process Models
    Umeshwar Dayal and Johann Eder and Jana Koehler and Hajo Reijers, editors
    In Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings, volume 5701 of Lecture Notes in Computer Science, Springer-Verlag, sep 2009
    close
  • Fahland, Dirk, Woith, Heiko
    Towards Process Models for Disaster Response
    In Business Process Management Workshops, International Workshop on Process Management for Highly Dynamic and Pervasive Scenarios (PM4HDPS), co-located with 6th International Conference on Business Process Management (BPM'08), volume 17 of Lecture Notes in Business Information Processing, Springer, Milan, Italy, September 2008
    In the immediate aftermath of a disaster routine processes, even if specifically designed for such a situation, are not enacted blindly. Actions and processes rather adapt their behavior based on observations and available information. Attempts to support these processes by technology rely on process models that faithfully capture process execution and adaptation. Based on experiences from actual disaster response settings, we propose to specify an adaptive process as a set of scenarios using a Petri net syntax. Our operational model provides an adaptation operator that synthesizes and adapts the system behavior at run-time based on the given scenarios. An example illustrates our approach.
    close
    close
  • Fahland, Dirk
    Adaptive und Selbststabilisierende Workflows
    Diehl, Malte and Lipskoch, Henrik and Meyer, Roland and Storm, Christian, editors
    In Proceedings des gemeinsamen Workshops der Graduiertenkollegs, Trustworthy Software Systems, Gito-Verlag, Berlin, 2008
    close
  • Fahland, Dirk
    Oclets -- Scenario-Based Modeling with Petri Nets
    Niels Lohmann and Karsten Wolf, editors
    In Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008, volume 380 of CEUR Workshop Proceedings, CEUR-WS.org, sep 2008
    Scenario-based specifications are used for modeling highly-complex, distributed systems in terms of partial runs (scenarios) the system shall have. But it is difficult to derive an implementing, operational model from a given set of scenarios, especially if concepts like anti-scenarios which must not occur are used. In this paper, we present a novel model for scenario-based specifications with Petri nets including anti-scenarios; we provide an operational semantics for our model.
    close
    close
  • Fahland, Dirk
    Towards Analyzing Declarative Workflows
    Jana Koehler and Marco Pistore and Amit P. Sheth and Paolo Traverso and Martin Wirsing, editors
    In Autonomous and Adaptive Web Services, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007
    Enacting tasks in a workflow cannot always follow a pre-defined process model. In application domains like disaster management workflows are partially specified and circumstances of their enactment change. There exist various approaches for formal workflow models that are effective in such situations, like declarative specifications instead of operational models for formalizing flexible workflow process. These powerful models leave a gap to existing techniques in the domain of workflow modeling, workflow analysis, and workflow management. In this paper we bridge this gap with a compositional mechanism for translating declarative workflow models to operational workflow models. The mechanism is of a general nature and we reveal its principles as we provide an exemplary definition for translating DecSerFlow models based on LTL to Petri nets. We then demonstrate its use in analyzing and refining declarative models.
    close
    close
  • Fahland, Dirk
    Synthesizing Petri nets from LTL specifications - An engineering approach
    Philippi, Stephan and Pinl, Alexander, editors
    In , , September 2007
    close
    close
  • Fahland, Dirk
    Modeling and Verifying Declarative Workflows
    In Dagstuhl ''zehn plus eins'', Verlagshaus Mainz, Aachen, 2007
    close
  • Glausch, Andreas
    Eine Charakterisierung einfacher Petrinetz-Schemata
    Karsten Schmidt and Christian Stahl, editors
    In , , sep 2005
    close
    close
  • Publikationen in Zeitschriften und Büchern

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

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

    Diplomarbeit, sep 2008
    close
    close
  • Pillat, Thomas

    Diplomarbeit, mar 2008
    close
    close
  • Technische Berichte

  • Fahland, Dirk
    Translating UML2 Activity Diagrams Petri Nets for analyzing IBM WebSphere Business Modeler process models
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2008
    We present a formal semantics for a variant of UML2 Activity Diagrams that is used in the IBM WebSphere Business Modeler for modeling business processes. Business process models created in the IBM WebSphere Business Modeler or with other UML2 modeling tools often constitutes one of the key specification artifacts for building an information system that implements or supports the specified processes. As UML2 Activity Diagrams lack a universally agreed semantics, the step from specification to implementation usually faces a semantical impedance caused by different interpretation of the same diagram. A well-defined formal semantics for the specification language determines the interpretation of a diagram and allows for reasoning about as well as validating and verifying a given specification on common (formal) grounds. We adapt approaches for formalizing semantics of UML2 Activity Diagrams and apply them to the core features of the IBM WebSphere Business Modeler language for purpose of formal verification. We provide a parameterized Petri net pattern for each language concepts. A diagram is translated by instantiating a pattern for each use of a concept; merging the resulting Petri net fragments according to the structure of the original diagram yields a Petri net that specifies the behavioral semantics of the diagram. The resulting Petri net can be verified for control-flow errors using the model checker LoLA. The semantics has been implemented in a tool that is available at http://www.service-technology.org/uml2owfn/.
    close
    close
  • Fahland, Dirk
    Oclets - a formal approach to adaptive systems using scenario-based concepts
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2008
    Usually, a component in a distributed system has assumptions about the remaining components of the system. A change in one component might require to change other components as well. It may happen that the change has to be performed in the running system. In this paper, we propose a formal model for systems that change their behavior at run-time: An adaptive system is denoted as a set of scenarios using a Petri net syntax. Our operational model provides an adaptation operator that synthesizes and adapts the system behavior as a Petri net branching-process at run-time based on the given scenarios. We show the feasibility of our approach by the help of an example.
    close
    close
  • Schmidt, Karsten, Stahl, Christian

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

    Informatik-Berichte, , feb 2005
    close
    close

Sca (3)

Sca

    Konferenzbeiträge auf Workshops

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

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

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

Serviceautomat (5)

Serviceautomat

    Konferenzbeiträge auf Workshops

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

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

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

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

Services (35)

Services

    Dissertationen und Habilitationen

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

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

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

  • Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
    Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
    volume 53 of The Computer Journal 53 (1), 2010
    To implement an interorganizational process between different enterprizes, one needs to agree on the ``rules of engagement''. These can be specified in terms of a contract that describes the overall intended process and the duties of all parties involved. We propose to use such a process-oriented contract which can be seen as the composition of the public views of all participating parties. Based on this contract each party may locally implement its part of the contract such that the implementation (the private view) agrees on the contract. In this paper, we propose a formal notion for such process-oriented contracts and give a criterion for accordance between a private view and its public view. The public view of a party can be substituted by a private view if and only if the private view accords with the public view. Using the notion of accordance the overall implemented process is guaranteed to be deadlock-free and it is always possible to terminate properly. In addition, we present a technique for automatically checking our accordance criterion. A case study illustrates how our proposed approach can be used in practice.
    close
    close
  • Stahl, Christian, Massuthe, Peter, Bretschneider, Jan
    Deciding Substitutability of Services with Operating Guidelines
    Kurt Jensen and Wil M. P. van der Aalst, editors
    volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2 (5460), Springer-Verlag, mar 2009
    Deciding whether a service S can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of restriction can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
    close
    close
  • Stahl, Christian, Wolf, Karsten
    Deciding Service Composition and Substitutability Using Extended Operating Guidelines
    volume 68 of Data Knowl. Eng. 68 (9), 2009
    We study the correct interaction between services using the following notion for correctness: there is no deadlock in the interaction of the services, and a given set of activities is not dead, that is, each activity in this set is executed in at least one run. The second condition has not been studied before. An operating guideline of a service P is an operational characterization of all deadlock-free interacting partners of P. In this paper, we present an extension of the concept of an operating guideline to characterize all correctly interacting partners of a service P. This extension can be used for answering at least the following two questions. First, given a service R, does R interact correctly with P? Second, given a service P', can P be substituted by P', that is, is every correctly interacting partner of P a correctly interacting partner of P', too?
    close
    close
  • Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela
    Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation
    volume 64 of Data Knowl. Eng. 64 (1), jan 2008
    We address the problem of analyzing the interaction between WS-BPEL processes. We present a technology chain that starts out with a WS-BPEL process and translates it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). To manage processes of realistic size, we present a concept of a \emphflexible model generation which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.
    close
    close
  • Massuthe, Peter, Serebrenik, Alexander, Sidorova, Natalia, Wolf, Karsten
    Can I find a Partner? Undecidablity of Partner Existence for Open Nets
    volume 108 of Information Processing Letters 108 (6), Nov 2008
    close
  • Kaschner, Kathrin, Massuthe, Peter, Wolf, Karsten
    Symbolic Representation of Operating Guidelines for Services
    volume 72 of Petri Net Newsletter 72, apr 2007
    close
  • Massuthe, Peter, Wolf, Karsten
    An Algorithm for Matching Non-deterministic Services with Operating Guidelines
    volume 2 of International Journal of Business Process Integration and Management (IJBPIM) 2 (2), 2007
    Interorganisational cooperation is more and more organised by the paradigm of services. Service-Oriented Architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester and the service broker, together with the three operations publish, find and bind. We provide a formal method based on non-deterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artefact to realise the publish operation. In our approach, the find operation reduces to a matching problem between the requesters service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free interaction. In this paper, matching of deterministic as well as non-deterministic automata with operating guidelines is presented.
    close
    close
  • Massuthe, Peter, Wolf, Karsten
    Operating Guidelines for Services
    volume 70 of Petri Net Newsletter 70, apr 2006
    In the service-oriented architecture (SOA), we distinguish three roles of service owners: service providers, service requesters, and service brokers, and the three standard operations publish, find, and bind. We provide a formal method based on Petri nets to model services. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester's service and the operating guideline.
    close
    close
  • Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
    An Operating Guideline Approach to the SOA
    volume 1 of Annals of Mathematics, Computing \& Teleinformatics 1 (3), 2005
    Interorganizational cooperation is more andmore organized by the paradigm of services. The serviceoriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester's and provider's services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester's service and the operating guideline. Binding of a requester's and a provider's service is therefore guaranteed to result in a well-behaving cooperating service. At this time, the approach is limited to acyclic Petri nets.
    close
    close
  • Studien- und Diplomarbeiten

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

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

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

Soa (18)

Soa

    Dissertationen und Habilitationen

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

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

  • Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
    Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
    volume 53 of The Computer Journal 53 (1), 2010
    To implement an interorganizational process between different enterprizes, one needs to agree on the ``rules of engagement''. These can be specified in terms of a contract that describes the overall intended process and the duties of all parties involved. We propose to use such a process-oriented contract which can be seen as the composition of the public views of all participating parties. Based on this contract each party may locally implement its part of the contract such that the implementation (the private view) agrees on the contract. In this paper, we propose a formal notion for such process-oriented contracts and give a criterion for accordance between a private view and its public view. The public view of a party can be substituted by a private view if and only if the private view accords with the public view. Using the notion of accordance the overall implemented process is guaranteed to be deadlock-free and it is always possible to terminate properly. In addition, we present a technique for automatically checking our accordance criterion. A case study illustrates how our proposed approach can be used in practice.
    close
    close
  • Mooij, Arjan J., Stahl, Christian, Voorhoeve, Marc
    Relating Fair Testing and Accordance for Service Replaceability
    Journal of Logic and Algebraic Programming, 2010
    The accordance pre-order describes whether a service can safely be replaced by another service. That is, all partners for the original service should be partners for the new service. Partners for a service interact with the service in such a way that always a certain common goal can be reached. We relate the accordance pre-order to the pre-orders known from the linear-branching time spectrum, notably fair testing. The differences between accordance and fair testing include the modeling of termination and success, and the parts of the services that cannot be used reliably by any partner. Apart from the theoretical results, we address the practical relevance of the introduced concepts.
    close
    close
  • Hee, Kees van, Verbeek, Eric, Stahl, Christian, Sidorova, Natalia
    A Framework for Linking and Pricing No-Cure-No-Pay Services
    Kurt Jensen and Wil M. P. van der Aalst, editors
    volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2, Springer-Verlag, mar 2009
    In this paper, we present a framework that allows us to orchestrate web services such that the web services involved in this orchestration interact properly. To achieve this, we predefine service interfaces and certain routing constructs. Furthermore, we define a number of rules to incrementally compute the price of such a properly interacting orchestration (i.e. a web service) from the price of its web services. The fact that a web service gets only payed after its service is delivered (no-cure-no-pay) is reflected by considering a probability of success. To determine a safe price that includes the risk a web service takes, we consider the variance of costs.
    close
    close
  • Stahl, Christian, Massuthe, Peter, Bretschneider, Jan
    Deciding Substitutability of Services with Operating Guidelines
    Kurt Jensen and Wil M. P. van der Aalst, editors
    volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2 (5460), Springer-Verlag, mar 2009
    Deciding whether a service S can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of restriction can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.
    close
    close
  • Aalst, Wil M. P. van der, Beisiegel, Michael, Hee, Kees M. van, König, Dieter, Stahl, Christian
    An SOA-based architecture framework
    volume 2 of International Journal of Business Process Integration and Management (IJBPIM) 2 (2), 2007
    We present an Service-Oriented Architecture (SOA)-based architecture framework. The architecture framework is designed to be close to industry standards, especially to the Service ComponentArchitecture (SCA).The framework is language independent and the building blocks of each system, activities and data, are first class citizens.We present a meta model of the architecture framework and discuss its concepts in detail. Through the framework, concepts of an SOA such as wiring, correlation and instantiation can be clarified.
    close
    close
  • Studien- und Diplomarbeiten

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

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

Soundness (1)

Soundness

    Konferenzbeiträge auf Workshops

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

Szenario-basierte Modelle (11)

Szenario-basierte Modelle

    Konferenzbeiträge auf Workshops

  • Fahland, Dirk, Weidlich, Matthias
    Scenario-based process modeling with Greta
    Marcello La Rosa, editors
    In Proc. of BPM Demonstration Track 2010, Hoboken, USA, September 14-16, 2010, volume 615 of CEUR-WS.org, Hoboken, USA, September 2010
    Designing understandable business process models is one of the key factors to successful business process management. Current modeling practices advocate the use of block-oriented concepts and subprocesses to structure complex process models. However, such guidelines cannot be applied in any case as case studies in process mining have shown. Previously, we proposed the scenario-based paradigm to structure models of complex processes in behavioral fragments, i.e., scenarios. This paper presents GRETA as a tool that supports scenario-based process modeling and execution.
    close
    close
  • Fahland, Dirk
    Oclets - scenario-based modeling with Petri nets
    Giuliana Franceschinis and Karsten Wolf, editors
    In Proceedings of the 30th International Conference on Petri Nets and Other Models Of Concurrency, 22-26 May 2009, volume 5606 of Lecture Notes in Computer Science, Springer-Verlag, Paris, France, jun 2009
    We present a novel, operational, formal model for scenario-based modeling with Petri nets. A scenario-based model describes the system behavior in terms of partial runs, called scenarios. This paradigm has been formalized in message sequence charts (MSCs) and live sequence charts (LSCs) which are in industrial and academic use. A particular application for scenarios are process models in disaster management where system behavior has to be adapted frequently, occasionally at run-time. An operational semantics of scenarios would allow to execute and adapt such systems on a formal basis. In this paper, we present a class of Petri nets for specifying and modeling systems with scenarios and anti-scenarios. We provide an operational semantics allowing to iteratively construct partially ordered runs that satisfy a given specification. We prove the correctness of our results.
    close
    close
  • Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
    Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
    John Krogstie and Terry Halpin and Erik Proper, editors
    In Proceedings of the 14th International Conference on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD'09), volume 29 of Lecture Notes in Business Information Processing, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
    Advantages and shortcomings of different process modeling languages are heavily debated, both in academia and industry, but little evidence is presented to support judgements. With this paper we aim to contribute to a more rigorous, theoretical discussion of the topic by drawing a link to well-established research on program comprehension. In particular, we focus on imperative and declarative techniques of modeling a process. Cognitive research has demonstrated that imperative programs deliver sequential information much better while declarative programs offer clear insight into circumstantial information. In this paper we show that in principle this argument can be transferred to respective features of process modeling languages. Our contribution is a pair of propositions that are routed in the cognitive dimensions framework. In future research, we aim to challenge these propositions by an experiment.
    close
    close
  • Fahland, Dirk
    A scenario is a behavioral view - Orchestrating services by scenario integration
    Oliver Kopp and Niels Lohmann, editors
    In Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, mar 2009
    The construction of a complex service orchestration is a tedious and error-prone task as multiple service interactions with a single orchestrating service must be specifi ed and combined. We suggest to specify a service orchestration in terms of behavioral scenarios that capture a specifi c aspect of service interaction, a behavioral view in isolation. By synchronizing the different scenarios, the views get integrated and define the behavior of a complex service orchestration. Our formal model for scenarios and their integration is a class of Petri nets called oclets.
    close
    close
  • Fahland, Dirk, Woith, Heiko
    Towards Process Models for Disaster Response
    In Business Process Management Workshops, International Workshop on Process Management for Highly Dynamic and Pervasive Scenarios (PM4HDPS), co-located with 6th International Conference on Business Process Management (BPM'08), volume 17 of Lecture Notes in Business Information Processing, Springer, Milan, Italy, September 2008
    In the immediate aftermath of a disaster routine processes, even if specifically designed for such a situation, are not enacted blindly. Actions and processes rather adapt their behavior based on observations and available information. Attempts to support these processes by technology rely on process models that faithfully capture process execution and adaptation. Based on experiences from actual disaster response settings, we propose to specify an adaptive process as a set of scenarios using a Petri net syntax. Our operational model provides an adaptation operator that synthesizes and adapts the system behavior at run-time based on the given scenarios. An example illustrates our approach.
    close
    close
  • Fahland, Dirk
    Oclets -- Scenario-Based Modeling with Petri Nets
    Niels Lohmann and Karsten Wolf, editors
    In Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008, volume 380 of CEUR Workshop Proceedings, CEUR-WS.org, sep 2008
    Scenario-based specifications are used for modeling highly-complex, distributed systems in terms of partial runs (scenarios) the system shall have. But it is difficult to derive an implementing, operational model from a given set of scenarios, especially if concepts like anti-scenarios which must not occur are used. In this paper, we present a novel model for scenario-based specifications with Petri nets including anti-scenarios; we provide an operational semantics for our model.
    close
    close
  • Fahland, Dirk
    Adaptive und Selbststabilisierende Workflows
    Diehl, Malte and Lipskoch, Henrik and Meyer, Roland and Storm, Christian, editors
    In Proceedings des gemeinsamen Workshops der Graduiertenkollegs, Trustworthy Software Systems, Gito-Verlag, Berlin, 2008
    close
  • Fahland, Dirk
    Modeling and Verifying Declarative Workflows
    In Dagstuhl ''zehn plus eins'', Verlagshaus Mainz, Aachen, 2007
    close
  • Fahland, Dirk
    A Formal Approach to Adaptive Processes using Scenario-based Concepts.
    Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
    In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, Siedlce, Poland, jun 2007
    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
  • Studien- und Diplomarbeiten

  • Wolf, Manja

    Diplomarbeit, sep 2008
    close
    close
  • Technische Berichte

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

Temporale Logik (12)

Temporale Logik

    Konferenzbeiträge auf Workshops

  • Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
    Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
    John Krogstie and Terry Halpin and Erik Proper, editors
    In Proceedings of the 14th International Conference on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD'09), volume 29 of Lecture Notes in Business Information Processing, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
    Advantages and shortcomings of different process modeling languages are heavily debated, both in academia and industry, but little evidence is presented to support judgements. With this paper we aim to contribute to a more rigorous, theoretical discussion of the topic by drawing a link to well-established research on program comprehension. In particular, we focus on imperative and declarative techniques of modeling a process. Cognitive research has demonstrated that imperative programs deliver sequential information much better while declarative programs offer clear insight into circumstantial information. In this paper we show that in principle this argument can be transferred to respective features of process modeling languages. Our contribution is a pair of propositions that are routed in the cognitive dimensions framework. In future research, we aim to challenge these propositions by an experiment.
    close
    close
  • Fahland, Dirk
    Modeling and Verifying Declarative Workflows
    In Dagstuhl ''zehn plus eins'', Verlagshaus Mainz, Aachen, 2007
    close
  • Fahland, Dirk
    Synthesizing Petri nets from LTL specifications - An engineering approach
    Philippi, Stephan and Pinl, Alexander, editors
    In , , September 2007
    close
    close
  • Fahland, Dirk
    Towards Analyzing Declarative Workflows
    Jana Koehler and Marco Pistore and Amit P. Sheth and Paolo Traverso and Martin Wirsing, editors
    In Autonomous and Adaptive Web Services, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007
    Enacting tasks in a workflow cannot always follow a pre-defined process model. In application domains like disaster management workflows are partially specified and circumstances of their enactment change. There exist various approaches for formal workflow models that are effective in such situations, like declarative specifications instead of operational models for formalizing flexible workflow process. These powerful models leave a gap to existing techniques in the domain of workflow modeling, workflow analysis, and workflow management. In this paper we bridge this gap with a compositional mechanism for translating declarative workflow models to operational workflow models. The mechanism is of a general nature and we reveal its principles as we provide an exemplary definition for translating DecSerFlow models based on LTL to Petri nets. We then demonstrate its use in analyzing and refining declarative models.
    close
    close
  • Alexander, Adrianna, Reisig, Wolfgang
    Compositional Temporal Logic Based on Partial Order
    In 11th International Symposium on Temporal Representation and Reasoning (TIME'04), IEEE Computer Society, 2004
    The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. The logic supports a compositional design of systems: subsystems can be specified separately and then be integrated into one system. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.
    close
    close
  • Alexander, Adrianna, Reisig, Wolfgang
    Logic of Involved Variables - System Specification with Temporal Logic of Distributed Actions
    In Proc. of the 3rd International Conference on Application of Concurrency to System Design (ACSD'03), Guimaraes, Portugal , IEEE Computer Society, jun 2003
    The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA can be syntactically viewed as a slight extension of TLA. We propose a different semantical model based on partial order which evidently increases the expressiveness of the logic. Local variable updates in a system are explicitly modeled and expressed by TLDA formulas. Consequently, we can distinguish between concurrency and nondeterministic choice. All valuable features of TLA (composition is conjunction, implementation is implication) are retained. In addition, we are able to describe some important phenomena and properties typical for distributed systems.
    close
    close
  • Studien- und Diplomarbeiten

  • Lohmann, Niels

    Diplomarbeit, sep 2005
    close
    close
  • Lohmann, Niels

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

  • Foremniak, Adrianna, Reisig, Wolfgang
    A Temporal Logic of Distributed Actions (TLDA)
    Informatik-Berichte, , 2000
    close

Tlda (7)

Tlda

    Konferenzbeiträge auf Workshops

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

  • Lohmann, Niels

    Diplomarbeit, sep 2005
    close
    close
  • Lohmann, Niels

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