Publikationen (nach name sortiert)

Acu, Baver (1)

Acu, Baver

    2006

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

Bretschneider, Jan (6)

Bretschneider, Jan

    2009

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

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

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

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

Fahland, Dirk (29)

Fahland, Dirk

    2013

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

  • Fahland, Dirk, Gierds, Christian
    Using Petri Nets for Modeling Enterprise Integration Patterns
    bpmcenter.org, 2012
    close
  • Fahland, Dirk, Prüfer, Robert
    Data and Abstraction for Scenario-Based Modeling with Petri Nets
    In Petri Nets, 2012
    close
  • 2010

  • Pinggera, Jakob, Zugal, Stefan, Weber, Barbara, Fahland, Dirk, Weidlich, Matthias, Mendling, Jan, Reijers, Hajo
    How the Structuring of Domain Knowledge Can Help Casual Process Modelers
    In ER 2010, 2010
    close
    close
  • Weidlich, Matthias, Zugal, Stefan, Pinggera, Jakob, Fahland, Dirk, Weber, Barbara, Reijers, Hajo, Mendling, Jan
    The Impact of Sequential and Circumstantial Changes on Process Models
    Bela Mutschler and Jan Recker and Roel Wieringa, editors
    In Proc. ER-POIS 2010, held in conjunction with CAiSE 2010, volume 603 of CEUR-WS, 2010
    While process modeling has become important for documenting business operations and automating workflow execution, there are serious issues with efficiently and effectively creating and modifying process models. While prior research has mainly investigated process model comprehension, there is hardly any work on maintainability of process models. Cognitive research into software program comprehension has demonstrated that imperative programs are strong in conveying sequential information while obfuscating circumstantial information. This paper addresses the question whether these findings can be transferred to process model maintenance. In particular, it investigates whether it is easier to incorporate sequential change requirements in imperative process models compared to circumstantial change requirements. To address this question this paper presents results from a controlled experiment providing evidence that the type of change (sequential versus circumstantial) has an effect on the accuracy of process models. For performance indicators modeling speed, correctness, and cognitive load no statistically significant differences could be identified.
    close
    close
  • Fahland, Dirk, Weidlich, Matthias
    Scenario-based process modeling with Greta
    Marcello La Rosa, editors
    In Proc. of BPM Demonstration Track 2010, Hoboken, USA, September 14-16, 2010, volume 615 of CEUR-WS.org, Hoboken, USA, September 2010
    Designing understandable business process models is one of the key factors to successful business process management. Current modeling practices advocate the use of block-oriented concepts and subprocesses to structure complex process models. However, such guidelines cannot be applied in any case as case studies in process mining have shown. Previously, we proposed the scenario-based paradigm to structure models of complex processes in behavioral fragments, i.e., scenarios. This paper presents GRETA as a tool that supports scenario-based process modeling and execution.
    close
    close
  • 2009

  • Fahland, Dirk, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
    Declarative vs. Imperative Process Modeling Languages: The Issue of Maintainability
    Stefanie Rinderle-Ma and Shazia Wasim Sadiq and Frank Leymann, editors
    In Business Process Management Workshops, BPM 2009 International Workshops, Ulm, Germany, September 7, 2009. Revised Papers, volume 43 of Lecture Notes in Business Information Processing, Springer, Ulm, Germany, sep 2009
    The rise of interest in declarative languages for process modeling both justifies and demands empirical investigations into their presumed advantages over more traditional, imperative alternatives. Our concern in this paper is with the ease of maintaining business process models, for example due to changing performance or conformance demands. We aim to contribute to a rigorous, theoretical discussion of this topic by drawing a link to well-established research on maintainability of information artifacts.
    close
    close
  • Fahland, Dirk, Favre, C\'edric, Jobstmann, Barbara, Koehler, Jana, Lohmann, Niels, Völzer, Hagen, Wolf, Karsten
    Instantaneous Soundness Checking of Industrial Business Process Models
    Umeshwar Dayal and Johann Eder and Jana Koehler and Hajo Reijers, editors
    In Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings, volume 5701 of Lecture Notes in Computer Science, Springer-Verlag, sep 2009
    close
  • Fahland, Dirk, Lübke, Daniel, Mendling, Jan, Reijers, Hajo, Weber, Barbara, Weidlich, Matthias, Zugal, Stefan
    Declarative versus Imperative Process Modeling Languages: The Issue of Understandability
    John Krogstie and Terry Halpin and Erik Proper, editors
    In Proceedings of the 14th International Conference on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD'09), volume 29 of Lecture Notes in Business Information Processing, Springer-Verlag, Amsterdam, The Netherlands, jun 2009
    Advantages and shortcomings of different process modeling languages are heavily debated, both in academia and industry, but little evidence is presented to support judgements. With this paper we aim to contribute to a more rigorous, theoretical discussion of the topic by drawing a link to well-established research on program comprehension. In particular, we focus on imperative and declarative techniques of modeling a process. Cognitive research has demonstrated that imperative programs deliver sequential information much better while declarative programs offer clear insight into circumstantial information. In this paper we show that in principle this argument can be transferred to respective features of process modeling languages. Our contribution is a pair of propositions that are routed in the cognitive dimensions framework. In future research, we aim to challenge these propositions by an experiment.
    close
    close
  • Fahland, Dirk
    Oclets - scenario-based modeling with Petri nets
    Giuliana Franceschinis and Karsten Wolf, editors
    In Proceedings of the 30th International Conference on Petri Nets and Other Models Of Concurrency, 22-26 May 2009, volume 5606 of Lecture Notes in Computer Science, Springer-Verlag, Paris, France, jun 2009
    We present a novel, operational, formal model for scenario-based modeling with Petri nets. A scenario-based model describes the system behavior in terms of partial runs, called scenarios. This paradigm has been formalized in message sequence charts (MSCs) and live sequence charts (LSCs) which are in industrial and academic use. A particular application for scenarios are process models in disaster management where system behavior has to be adapted frequently, occasionally at run-time. An operational semantics of scenarios would allow to execute and adapt such systems on a formal basis. In this paper, we present a class of Petri nets for specifying and modeling systems with scenarios and anti-scenarios. We provide an operational semantics allowing to iteratively construct partially ordered runs that satisfy a given specification. We prove the correctness of our results.
    close
    close
  • Fahland, Dirk
    A scenario is a behavioral view - Orchestrating services by scenario integration
    Oliver Kopp and Niels Lohmann, editors
    In Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, mar 2009
    The construction of a complex service orchestration is a tedious and error-prone task as multiple service interactions with a single orchestrating service must be specifi ed and combined. We suggest to specify a service orchestration in terms of behavioral scenarios that capture a specifi c aspect of service interaction, a behavioral view in isolation. By synchronizing the different scenarios, the views get integrated and define the behavior of a complex service orchestration. Our formal model for scenarios and their integration is a class of Petri nets called oclets.
    close
    close
  • 2008

  • Fahland, Dirk
    Translating UML2 Activity Diagrams Petri Nets for analyzing IBM WebSphere Business Modeler process models
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2008
    We present a formal semantics for a variant of UML2 Activity Diagrams that is used in the IBM WebSphere Business Modeler for modeling business processes. Business process models created in the IBM WebSphere Business Modeler or with other UML2 modeling tools often constitutes one of the key specification artifacts for building an information system that implements or supports the specified processes. As UML2 Activity Diagrams lack a universally agreed semantics, the step from specification to implementation usually faces a semantical impedance caused by different interpretation of the same diagram. A well-defined formal semantics for the specification language determines the interpretation of a diagram and allows for reasoning about as well as validating and verifying a given specification on common (formal) grounds. We adapt approaches for formalizing semantics of UML2 Activity Diagrams and apply them to the core features of the IBM WebSphere Business Modeler language for purpose of formal verification. We provide a parameterized Petri net pattern for each language concepts. A diagram is translated by instantiating a pattern for each use of a concept; merging the resulting Petri net fragments according to the structure of the original diagram yields a Petri net that specifies the behavioral semantics of the diagram. The resulting Petri net can be verified for control-flow errors using the model checker LoLA. The semantics has been implemented in a tool that is available at http://www.service-technology.org/uml2owfn/.
    close
    close
  • Fahland, Dirk, Woith, Heiko
    Towards Process Models for Disaster Response
    In Business Process Management Workshops, International Workshop on Process Management for Highly Dynamic and Pervasive Scenarios (PM4HDPS), co-located with 6th International Conference on Business Process Management (BPM'08), volume 17 of Lecture Notes in Business Information Processing, Springer, Milan, Italy, September 2008
    In the immediate aftermath of a disaster routine processes, even if specifically designed for such a situation, are not enacted blindly. Actions and processes rather adapt their behavior based on observations and available information. Attempts to support these processes by technology rely on process models that faithfully capture process execution and adaptation. Based on experiences from actual disaster response settings, we propose to specify an adaptive process as a set of scenarios using a Petri net syntax. Our operational model provides an adaptation operator that synthesizes and adapts the system behavior at run-time based on the given scenarios. An example illustrates our approach.
    close
    close
  • Fahland, Dirk
    Adaptive und Selbststabilisierende Workflows
    Diehl, Malte and Lipskoch, Henrik and Meyer, Roland and Storm, Christian, editors
    In Proceedings des gemeinsamen Workshops der Graduiertenkollegs, Trustworthy Software Systems, Gito-Verlag, Berlin, 2008
    close
  • Fahland, Dirk
    Oclets - a formal approach to adaptive systems using scenario-based concepts
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2008
    Usually, a component in a distributed system has assumptions about the remaining components of the system. A change in one component might require to change other components as well. It may happen that the change has to be performed in the running system. In this paper, we propose a formal model for systems that change their behavior at run-time: An adaptive system is denoted as a set of scenarios using a Petri net syntax. Our operational model provides an adaptation operator that synthesizes and adapts the system behavior as a Petri net branching-process at run-time based on the given scenarios. We show the feasibility of our approach by the help of an example.
    close
    close
  • Fahland, Dirk
    Oclets -- Scenario-Based Modeling with Petri Nets
    Niels Lohmann and Karsten Wolf, editors
    In Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008, volume 380 of CEUR Workshop Proceedings, CEUR-WS.org, sep 2008
    Scenario-based specifications are used for modeling highly-complex, distributed systems in terms of partial runs (scenarios) the system shall have. But it is difficult to derive an implementing, operational model from a given set of scenarios, especially if concepts like anti-scenarios which must not occur are used. In this paper, we present a novel model for scenario-based specifications with Petri nets including anti-scenarios; we provide an operational semantics for our model.
    close
    close
  • 2007

  • Fahland, Dirk
    Modeling and Verifying Declarative Workflows
    In Dagstuhl ''zehn plus eins'', Verlagshaus Mainz, Aachen, 2007
    close
  • Reisig, Wolfgang, Bretschneider, Jan, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
    Services as a Paradigm of Computation
    Cliff B. Jones and Zhiming Liu and Jim Woodcock, editors
    In Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj\orner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, volume 4700 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
    The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.
    close
    close
  • Fahland, Dirk
    Synthesizing Petri nets from LTL specifications - An engineering approach
    Philippi, Stephan and Pinl, Alexander, editors
    In , , September 2007
    close
    close
  • Fahland, Dirk
    A Formal Approach to Adaptive Processes using Scenario-based Concepts.
    Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
    In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, Siedlce, Poland, jun 2007
    The problem and need for adapting business processes and service behavior to cope with changing circumstances is identified well. Standard models for business processes still rely on a fixed process logic, the change of which is rather hard to achieve. Ad-hoc changes to a standard model are usually considered too `dangerous' as they are performed in not well-defined manner. Other models for adaptive processes deviate to some extent from established business process models. This deviation comes at the price of limited understandability and loss in analysis capabilities. We propose a model for adaptive processes based on Petri nets which have successfully been applied in modeling and analyzing business process and web services. Our operator to adapt the behavior of such models is formalized by the help of scenario-based concepts known from live-sequence charts in purely mathematical terms. This combination of concepts allows to write down the result of the adaptation rather than how adaptation shall be performed.
    close
    close
  • Fahland, Dirk
    Towards Analyzing Declarative Workflows
    Jana Koehler and Marco Pistore and Amit P. Sheth and Paolo Traverso and Martin Wirsing, editors
    In Autonomous and Adaptive Web Services, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007
    Enacting tasks in a workflow cannot always follow a pre-defined process model. In application domains like disaster management workflows are partially specified and circumstances of their enactment change. There exist various approaches for formal workflow models that are effective in such situations, like declarative specifications instead of operational models for formalizing flexible workflow process. These powerful models leave a gap to existing techniques in the domain of workflow modeling, workflow analysis, and workflow management. In this paper we bridge this gap with a compositional mechanism for translating declarative workflow models to operational workflow models. The mechanism is of a general nature and we reveal its principles as we provide an exemplary definition for translating DecSerFlow models based on LTL to Petri nets. We then demonstrate its use in analyzing and refining declarative models.
    close
    close
  • Fahland, Dirk, , Quilitz, Bastian, , Leser, Ulf
    HUODINI - Flexible Information Integration for Disaster Management
    In 4th International Conference on Information Systems for Crisis Response and Management (ISCRAM), Delft, NL, 2007
    Fast and effective disaster management requires access to a multitude of heterogeneous, distributed, and quickly changing data sets, such as maps, satellite images, or governmental databases. In the last years, also the information created by affected persons on web sites such as flickr.com or blogger.com became an important and very quickly adapting source of information. We developed HUODINI, a prototype system for the flexible integration and visualization of heterogeneous data sources for disaster management. HUODINI is based on Semantic Web technologies, and in particular RDF, to offer maximal flexibility in the types of data sources it can integrate. It supports a hybrid push/pull approach to cater for the requirements of fast-changing sources, such as news feeds, and maximum performance for querying the integrated data set. In this paper, we describe the design goals underlying our approach, its architecture, and report on first experiences with the system.
    close
    close
  • 2006

  • Reisig, Wolfgang, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela, Wolf, Karsten, Kaschner, Kathrin
    Analysis Techniques for Service Models
    In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, IEEE Computer Society, nov 2006
    The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.
    close
    close
  • Fahland, Dirk
    Unfoldings for Timed Automata
    Diplomarbeit, July 2006
    In this thesis we develop a state space reduction technique for networks of timed automata based on unfoldings to alleviate the state space explosion problem due to concurrently enabled actions. For the purpose of verifying a system, standard model checking techniques construct its sequential state space that suffers an exponential growth when applied to distributed systems because of concurrently enabled, independent actions: during the construction of the state space these actions are ordered arbitrarily to simulate concurrency in the sequential model. For untimed systems, state space reduction techniques like stubborn sets that omit the construction of redundant information, and unfoldings that represent concurrent events in a partial order have successfully been applied to alleviate the exponential growth. These techniques apply a simple syntactical criterion to identify independent actions. This criterion is not applicable to networks of timed automata as simple examples show, which renders the existing techniques unapplicable. But networks of timed automata face the state space explosion problem as well which raises the demand for a specific reduction technique for these systems. In this thesis, we consider a special, but practically relevant class of networks of timed automata as a formal model for discrete, distributed, timed systems. We develop a novel technique that constructs a complete, finite representation of such a system's state space. This representation is the complete, finite prefix of an unfolding in which concurrently enabled actions are partially ordered. We show that this technique is capable of reducing the size of the state space by magnitude. We are presently not aware of any state space reduction technique for timed automata with similar results.
    close
    close
  • 2005

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

  • Fahland, Dirk
    Ein Ansatz einer formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines
    Studienarbeit, aug 2004
    close
    close
  • Martens, Axel, Stahl, Christian, Weinberg, Daniela, Fahland, Dirk, Heidinger, Thomas
    Business Process Execution Language for Web services - Semantik, Analyse und Visualisierung
    Informatik-Berichte, , jul 2004
    close
    close

Fichte, Johannes Klaus (1)

Fichte, Johannes Klaus

    2009

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

Görlach, Katharina (1)

Görlach, Katharina

    2007

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

Gierds, Christian (10)

Gierds, Christian

    2013

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

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

  • Gierds, Christian, Sürmeli, Jan
    Estimating costs of a service
    Christian Gierds and Jan Sürmeli, editors
    In Proceedings of the 2nd Central-European Workshop on Services and their Composition, ZEUS 2010, Berlin, Germany, February 25--26, 2010, volume 563 of CEUR Workshop Proceedings, CEUR-WS.org, 2010
    When designing a publicly available Web service, a service designer has to take care of costs and revenue caused by this services. In the very beginning possible partners might only be vaguely known, or the service behavior contains arbitrary repetitions. Then the estimation of costs for running this service is difficult and decisions based on them can hardly be made. We propose a static analysis of the service's behavior. We over-approximate possible runs and therefore costs of the service. Our approach provides a basis for reasoning about nonfunctional properties as shown for costs.
    close
    close
  • Gierds, Christian, Lohmann, Niels
    A Graphical User Interface for Service Adaptation
    Martin Schwarick and Monika Heiner, editors
    In Proceedings of the 17th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2010, Cottbus, Germany, October 07-08, 2010, volume 643 of CEUR Workshop Proceedings, CEUR-WS.org, oct 2010
    close
  • 2008

  • Gierds, Christian
    Strukturelle Reduktion von Bedienungsanleitungen
    Diplomarbeit, jan 2008
    close
    close
  • Gierds, Christian, Mooij, Arjan J., Wolf, Karsten
    Specifying and generating behavioral service adapter based on transformation rules
    Preprint, Universität Rostock, Rostock, Germany, aug 2008
    Behavioral adapters are a way to establish proper interaction between services that have been developed independently. We present a novel approach for specifying such adapters, based on domain-specific transformation rules that reflect the elementary operations that adapters can perform. We show how complex adapters that adhere to these rules can be generated using existing controller generation algorithms. We discuss some example applications, including real-world business processes.
    close
    close
  • Gierds, Christian
    Finding Cost-Efficient Adapters
    Niels Lohmann and Karsten Wolf, editors
    In Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008, volume 380 of CEUR Workshop Proceedings, CEUR-WS.org, sep 2008
    close
  • 2007

  • Gierds, Christian

    Studienarbeit, oct 2007
    close
    close

Glausch, Andreas (10)

Glausch, Andreas

    2007

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

  • 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
  • Glausch, Andreas, Reisig, Wolfgang
    How Expressive are Petri Net Schemata?
    Susanna Donatelli and P. S. Thiagarajan, editors
    In Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, Springer, 2006
    Petri net schemata are an intuitive and expressive approach to describe high-level Petri nets. A Petri net schema is a Petri net with edges and transitions inscribed by terms and Boolean expressions, respectively. A concrete high-level net is gained by interpreting the symbols in the inscriptions by a structure. Its semantics can then be described in terms of a transition system. Therefore, the semantics of a Petri Net schema can be conceived as a family of transition systems indexed by structures. In this paper we characterize the expressive power of a general version of Petri net schemata. For that purpose we examine families of transition systems in general and characterize the families as generated by Petri net schemata. It turns out that these families of transition systems can be characterized by simple and intuitive requirements.
    close
    close
  • Glausch, Andreas, Reisig, Wolfgang
    On the Expressive Power of Unbounded-Nondeterministic Abstract State Machines
    Informatik-Berichte, , dec 2006
    Conventional computational models assume a symbolical representation of states. Gurevich's Abstract State Machines (ASMs) take a more liberal position: any mathematical structure may serve as a state. Gurevich characterizes the expressive power of sequential ASMs in a non-trivial theorem: he defines the class of \emphsequential algorithms by help of only a few, amazingly general requirements and proves this class to be equivalent to sequential ASMs. Later, this result has been extended to the class of bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among infinitely many alternatives. We define the class of unbounded-nondeterministic algorithms by a conservative extension of Gurevich's original requirements to sequential algorithms. We show that this class is equivalent to unbounded-nondeterministic ASMs.
    close
    close
  • Glausch, Andreas
    Distributed Abstract State Machines - Status Report of a Doctoral Thesis
    , editors
    In Proceedings of the Doctoral Consortium ACSD \& PetriNets 2006, , Turku, Finland, jun 2006
    In 1985, Gurevich introduced Abstract State Machines (ASMs) as a computational model more powerful and universal than classical computational models. Since then ASMs have been applied successfully both in theory and practice: On the theoretical side, ASMs evolved to a general basis for the study of different classes of algorithms and their expressive power. On the practical side, ASMs have been extended to a full-fledged design methodology, applied successfully in industry for the specification and analysis of real-world systems. In my doctoral thesis I examine the class of distributed ASMs and study their expressive power. I also intend to develop basic notions of refinement and composition for distributed ASMs.
    close
    close
  • 2005

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

  • Glausch, Andreas
    Abstract-State Machines - Eine Sammlung didaktischer Beispiele
    Studienarbeit, feb 2003
    Diese Studienarbeit versucht durch eine Vielzahl von Beispielen den Begriff Abstract-State Machine und sequenzieller Algorithmus didaktisch sinnvoll darzustellen. Es werden dabei sowohl Beispiele als auch Gegenbeispiele angegeben, um Umfang und Grenzen dieser Begriffe aufzuzeigen.
    close
    close

Kindler, Ekkart (57)

Kindler, Ekkart

    2003

  • 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
  • Weber, Michael, Kindler, Ekkart
    The Petri Net Markup Language
    Hartmut Ehrig and Wolfgang Reisig and Grzegorz Rozenberg and Herbert Weber, editors
    In Petri Net Technology for Communication-Based Systems, volume 2472 of Lecture Notes in Computer Science, Springer-Verlag, 2003
    The Petri Net Markup Language (PNML) is an XML-based interchange format for Petri nets. PNML supports any version of Petri net since new Petri net types can be defined by so-called Petri Net Type Definitions (PNTD). In this paper, we present the syntax and the semantics of PNML as well as the principles underlying its design. Moreover, we present an extension called modular PNML, which is a type independent module concept for Petri nets.
    close
    close
  • 2001

  • Kindler, Ekkart, Weber, Michael
    Modules in Pictures
    volume 61 of Petri Net Newsletter 61, oct 2001
    close
  • Kindler, Ekkart, Weber, Michael
    A universal module Concept for Petri nets
    Gabriel Juhas und Robert Lorenz, editors
    In Proceedings des 8. Workshops AWPN, , oct 2001
    close
  • 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
  • Kindler, Ekkart
    Systematische Spezifikation und Verifikation von Konsistenzprotokollen
    Habilitationsschrift, aug 2001
    close
  • Kindler, Ekkart, Weber, Michael
    A Universal Module Concept for Petri Nets - An Implementation-Oriented Approach
    Informatik-Berichte, , apr 2001
    close
  • 2000

  • Kindler, Ekkart, Shasha, Dennis
    Verifying a Design Pattern for the Fault-Tolerant Execution of Parallel Programs
    Technical Report, New York University, Courant Institute of Mathematical Sciences, Computer Science Department, jun 2000
    close
  • Kindler, Ekkart, Weber, Michael
    The Petri Net Kernel
    , editors
    In Tool Demonstrations, 21. ICATPN, , jun 2000
    close
  • Kindler, Ekkart
    Consistency, Causality, Petri Nets, and Automata
    Hans-Dieter Burkhard and Ludwik Czaja and Andrzej Skowron and Peter H. Starke, editors
    In Workshop Concurrency, Specification \& Programming (CS\&P 2000), oct 2000
    close
  • , Kindler, Ekkart, Weber, Michael
    Towards a Generic Interchange Format for Petri Nets
    Remi Bastide and Jonathan Billington and Ekkart Kindler and Fabrice Kordon and Kjeld H. Mortensen, editors
    In Meeting on XML/SGML based Interchange Formats for Petri Nets, 21. ICATPN, , jun 2000
    close
  • , Kindler, Ekkart, Weber, Michael
    The Petri Net Markup Language
    S. Philippi, editors
    In , , jun 2000
    close
  • Kindler, Ekkart, Martens, Axel
    Cross-talk revisited - What's the problem?
    volume 58 of Petri Net Newsletter 58, 2000
    close
  • Kindler, Ekkart, Martens, Axel, Reisig, Wolfgang
    Inter-operability of Workshop Applications - Local Criteria for Global Soundness
    , editors
    In Business Process Management, volume 1806 of Lecture Notes in Computer Science, Springer-Verlag, 2000
    close
  • Kindler, Ekkart,
    Algebraic Nets with Flexible Arcs
    Theoretical Computer Science, 2000
    close
  • Kindler, Ekkart
    Serializability, concurrency control and replication control
    , editors
    In Transactions and Database Dynamics, Proceedings of the 8th International Workshop on Foundations of Models and Languages for Data and Objects, Selected Papers, volume 1773 of Lecture Notes in Computer Science, Springer-Verlag, 2000
    close
  • 1999

  • 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
  • Martens, Axel, Kindler, Ekkart

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

    E. Schnieder, editors
    In Entwicklung und Betrieb komplexer Automatisierungssysteme, 6. Fachtagung, Band II, may 1999
    close
  • Kindler, Ekkart, Aalst, Wil M. P. van der
    Liveness, Fairness, and Recurrence
    Technical Report, University of Georgia, Department of Computer Science, Athens, USA, apr 1999
    close
  • Baar, Thomas, Kindler, Ekkart,
    Verifying Intuition - ILF Checks DAWN Proofs
    In Application and Theory of Petri Nets, 20th International Conference, ICATPN '99, Proceedings, volume 1639 of Lecture Notes in Computer Science, Springer-Verlag, 1999
    The DAWN approach allows to model and verify distributed algorithms in an intuitive way. At a first glance, a DAWN proof may appear to be informal. In this paper, we argue that DAWN proofs are formal and can be checked for correctness fully automatically by automated theorem provers. The basic technique are proof rules which generate proof obligations. For the definition of the proof rules we adopt assertions and we introduce conflict formulas for algebraic Petri nets. Experiments show that the generated proof obligations can be automatically checked by theorem provers.
    close
    close
  • 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
  • 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
  • Kindler, Ekkart, Peuker, Sibylle
    Integrating distributed algorithms into distributed systems
    volume 37 of Fundamenta Informaticae 37 (3), feb 1999
    close
  • Kindler, Ekkart, Vesper, Tobias, Weber, Michael
    Application-oriented verification scenarios
    1999
    close
  • 1998

  • Kindler, Ekkart, Vesper, Tobias
    ESTL: A Temporal Logic for Events and States
    , editors
    In Application and Theory of Petri Nets, 19th International Conference, ICATPN '98, Proceedings, volume 1420 of Lecture Notes in Computer Science, Springer-Verlag, jun 1998
    close
  • Kindler, Ekkart
    The interplay of transaction models and memory models
    , editors
    In Proceedings of the Third International Conference on Integrated Design and Process Technology, volume 2 of IDPT, Society for Design and Process Science, jul 1998
    close
  • Kindler, Ekkart,
    Flexibility in Algebraic Nets
    , editors
    In Application and Theory of Petri Nets, 19th International Conference, ICATPN '98, Proceedings, volume 1420 of Lecture Notes in Computer Science, Springer-Verlag, jun 1998
    close
  • Kindler, Ekkart
    Database theory - Petri net theory - Workflow theory
    Informatik-Berichte, , may 1998
    close
  • Baar, Thomas, Kindler, Ekkart
    Einsatz von ILF und DAWN zur Verifikation verteilter Algorithmen - Eine Vorstudie
    Informatik-Berichte, , mar 1998
    close
  • , Kindler, Ekkart
    Proving Correctness of Distributed Algorithms Using High-Level Petri Nets - A Case Study
    In First International Conference on Application of Concurrency to System Design (ACSD'98), IEEE Computer Society Press, Fukushima, Japan, mar 1998
    close
  • Hauptmann, Jens, Hohberg, Bodo, Kindler, Ekkart, Schwenzer, Ines, Weber, Michael
    Der Petrinetz-Kern - Dokumentation der Anwendungs-Schnittstelle
    Informatik-Berichte, , feb 1998
    close
  • 1997

  • Kindler, Ekkart
    Inhibitor arcs: A philosophical view
    volume 53 of Petri Net Newsletter 53, oct 1997
    close
  • Kindler, Ekkart, Vesper, Tobias
    A temporal logic for events and states in Petri nets
    B. Farwer and D. Moldt and M.-O. Stehr, editors
    In Petri Nets in System Engineering (PNSE'97) Modelling, Verification, and Validation, Fachberichte, , sep 1997
    close
  • Kindler, Ekkart, Vesper, Tobias
    ESTL: A temporal logic for events and states
    Informatik-Berichte, , nov 1997
    close
  • Kindler, Ekkart,
    Flexibility in algebraic nets
    Informatik-Berichte, , nov 1997
    close
  • Weber, Michael, Walter, Rolf, , Vesper, Tobias, Reisig, Wolfgang, Peuker, Sibylle, Kindler, Ekkart, ,
    DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen
    Informatik-Berichte, , dec 1997
    close
  • , Kindler, Ekkart, Oberweis, Andreas

    Informatik-Berichte, , sep 1997
    close
  • Kindler, Ekkart
    A compositional partial order semantics for Petri net components
    , editors
    In Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN '97, Proceedings, volume 1248 of Lecture Notes in Computer Science, Springer-Verlag, jun 1997
    close
  • Kindler, Ekkart, Reisig, Wolfgang
    Verification of Distributed Algorithms with Algebraic Petri Nets
    , editors
    In Foundations of Computer Science: Potential - Theory - Cognition, volume 1337 of Lecture Notes in Computer Science, Springer-Verlag, 1997
    close
  • Kindler, Ekkart
    Der Petrinetz-Kern: Ein Traum wird wahr
    1997
    close
  • Kindler, Ekkart, Reisig, Wolfgang, , Walter, Rolf
    Petri Net Based Verification of Distributed Algorithms: An Example
    volume 9 of Formal Aspects of Computing 9 (4), Springer-Verlag, 1997
    close
  • Kindler, Ekkart, Walter, Rolf
    Mutex Needs Fairness
    volume 62 of Information Processing Letters 62 (1), ELSEVIER, 1997
    close
  • , Kindler, Ekkart
    Proving correctness of distributed algorithms: A Petrinet approach
    Bericht, , feb 1997
    close
  • Fricke, Olaf, Borusan, Alexander, Vesper, Tobias, Kindler, Ekkart
    Verifikation im Vorgehensmodell anhand eines Beispiels
    1997
    close
  • 1996

  • Walter, Rolf, , Vesper, Tobias, Reisig, Wolfgang, Kindler, Ekkart, ,
    Memorandum: Petrinetzmodelle zur Verifikation verteilter Algorithmen
    Informatik-Berichte, , aug 1996
    close
  • Kindler, Ekkart,
    Der Traum von einem universellen Petrinetz-Werkzeug - Der Petrinetz-Kern
    , editors
    In , , oct 1996
    close
  • Kindler, Ekkart, Vesper, Tobias

    , editors
    In , , oct 1996
    close
  • Kindler, Ekkart, Reisig, Wolfgang
    Algebraic System Nets for Modelling Distributed Algorithms
    volume 51 of Petri Net Newsletter 51, nov 1996
    close
  • Kindler, Ekkart
    A Specification and Verification Method for Caching Protocols
    , editors
    In Formal Methods for Concurrency, GI-Kolloquium, Fachberichte der TU Dresden, , jul 1996
    close
  • Kindler, Ekkart, Walter, Rolf
    Arc-Typed Petri Nets
    J. Billington and Wolfgang Reisig, editors
    In Application and Theory of Petri Nets 1996, volume 1091 of Lecture Notes in Computer Science, Springer-Verlag, jun 1996
    close
  • Kindler, Ekkart
    A Compositional Partial Order Semantics for Petri Net Components
    SFB-Bericht, , mar 1996
    close
  • Kindler, Ekkart, Listl, Andreas, Walter, Rolf
    A Specification Method for Transaction Models with Data Replication
    Informatik-Berichte, , mar 1996
    close
  • Kindler, Ekkart, Reisig, Wolfgang, , Walter, Rolf
    Petri Net Based Verification of Distributed Algorithms: An Example
    Informatik-Berichte, , may 1996
    close
  • Reisig, Wolfgang, Kindler, Ekkart, Vesper, Tobias, Völzer, Hagen, Walter, Rolf
    Distributed Algorithms for Networks of Agents.
    In Petri Nets (2), 1996
    close

Lohmann, Niels (31)

Lohmann, Niels

    2010

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

  • Fahland, Dirk, Favre, C\'edric, Jobstmann, Barbara, Koehler, Jana, Lohmann, Niels, Völzer, Hagen, Wolf, Karsten
    Instantaneous Soundness Checking of Industrial Business Process Models
    Umeshwar Dayal and Johann Eder and Jana Koehler and Hajo Reijers, editors
    In Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings, volume 5701 of Lecture Notes in Computer Science, Springer-Verlag, sep 2009
    close
  • Liske, Nannette, Lohmann, Niels, Stahl, Christian, Wolf, Karsten
    Another Approach to Service Instance Migration
    Luciano Baresi and Chi-Hung Chi and Jun Suzuki, editors
    In Service-Oriented Computing - ICSOC 2009, 7th International Conference, Stockholm, Sweden, November 24-27, 2009. Proceedings, Lecture Notes in Computer Science, Springer-Verlag, nov 2009
    Services change over time, be it for internal improvements, be it for external requirements such as new legal regulations. For long running services, it may even be necessary to change a service while instances are actually running and interacting with other services. This problem is referred to as instance migration. We present a novel approach to the behavioral (service protocol) aspects of instance migration. We apply techniques for finitely characterizing the set of all correctly interacting partners to a given service. The approach assures that migration does not introduce behavioral problems with any running partner of the original service. Our technique scales up to services with thousands of states, including models of real WS-BPEL processes.
    close
    close
  • Lohmann, Niels, Verbeek, Eric, Ouyang, Chun, Stahl, Christian
    Comparing and Evaluating Petri Net Semantics for BPEL
    volume 4 of International Journal of Business Process Integration and Management (IJBPIM) 4 (1), 2009
    We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modelling decisions. These decisions together with their consequences are discussed. We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.
    close
    close
  • Lohmann, Niels, Verbeek, Eric, Dijkman, Remco
    Petri Net Transformations for Business Processes -- A Survey
    Kurt Jensen and Wil M. P. van der Aalst, editors
    volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2, Springer-Verlag, mar 2009
    In Process-Aware Information Systems, business processes are often modeled in an explicit way. Roughly spoken, the available business process modeling languages can be divided into two groups. Languages from the first group are preferred by academic people but shunned by business people, and include Petri nets and process algebras. These academic languages have a proper formal semantics, which allows the corresponding academic models to be verified in a formal way. Languages from the second group are preferred by business people but disliked by academic people, and include BPEL, BPMN, and EPCs. These business languages often lack any proper semantics, which often leads to debates on how to interpret certain business models. Nevertheless, business models are used in practice, whereas academic models are hardly used. To be able to use, for example, the abundance of Petri net verification techniques on business models, we need to be able to transform these models to Petri nets. In this paper, we investigate a number of Petri net transformations that already exist. For every transformation, we investigate the transformation itself, the constructs in the business models that are problematic for the transformation and the main applications for the transformation.
    close
    close
  • 2008

  • Lohmann, Niels, Kleine, Jens
    Fully-automatic Translation of Open Workflow Net Models into Human-readable Abstract BPEL Processes
    Thomas Kühne and Wolfgang Reisig and Friedrich Steimann, editors
    In Modellierung 2008, 12.-14. März 2008, Berlin, Proceedings, volume P-127 of Lecture Notes in Informatics (LNI), GI, mar 2008
    On the one hand, Petri net models have a successful history in the modeling, simulation, and verification of workflows and business processes. On the other hand, BPEL is the de facto standard for describing executable Web service-based business processes. With abstract BPEL processes, BPEL can also be used as modeling language. However, being a complicated language with many syntactic constraints, abstract BPEL processes impede a straightforward modeling. In this paper, we introduce a fully-automatic translation of Petri net models into abstract BPEL processes which can be refined to executable BPEL processes. This approach combines strengths of Petri nets in modeling and verification with the ability to execute BPEL processes. Furthermore, it completes the Tools4BPEL framework to synthesize BPEL processes which are correct by design.
    close
    close
  • 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
  • König, Dieter, Lohmann, Niels, Moser, Simon, Stahl, Christian, Wolf, Karsten
    Extending the Compatibility Notion for Abstract WS-BPEL Processes
    Wei-Ying Ma and Andrew Tomkins and Xiaodong Zhang, editors
    In Proceedings of the 17th International Conference on World Wide Web, WWW 2008, Beijing, China, April 21--25, 2008, apr 2008
    WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.
    close
    close
  • Lohmann, Niels
    Correcting Deadlocking Service Choreographies Using a Simulation-Based Graph Edit Distance
    Marlon Dumas and Manfred Reichert, editors
    In Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1--4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, Springer-Verlag, sep 2008
    Many work has been conducted to analyze service choreographies to assert manyfold correctness criteria. While errors can be detected automatically, the correction of defective services is usually done manually. This paper introduces a graph-based approach to calculate the minimal edit distance between a given defective service and synthesized correct services. This edit distance helps to automatically fix found errors while keeping the rest of the service untouched. A prototypic implementation shows that the approach is applicable to real-life services.
    close
    close
  • Lohmann, Niels
    Why does my service have no partners?
    Roberto Bruni and Karsten Wolf, editors
    In Web Services and Formal Methods, Fifth International Workshop, WS-FM 2008, Milan, Italy, September 4-5, 2008, Proceedings, Lecture Notes in Computer Science, Springer-Verlag, sep 2008
    Controllability is a fundamental correctness criterion for interacting service models. A service model is controllable if there exists a partner service such that their composition is free of deadlocks and livelocks. Whereas controllability can be automatically decided, the existing decision algorithm gives no information about the reasons of why a service model is uncontrollable. This paper introduces a diagnosis framework to find these reasons which can help to fix uncontrollable service models.
    close
    close
  • Lohmann, Niels
    A Feature-Complete Petri Net Semantics for WS-BPEL 2.0
    Marlon Dumas and Reiko Heckel, editors
    In Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, Springer-Verlag, 2008
    We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.
    close
    close
  • Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
    From Public Views to Private Views -- Correctness-by-Design for Services
    Marlon Dumas and Reiko Heckel, editors
    In Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, Springer-Verlag, 2008
    Service orientation is a means for integrating across diverse systems. Each resource, whether an application, system, or trading partner, can be accessed as a service. The resulting architecture, often referred to as SOA, has been an important enabler for interorganizational processes. Apart from technological issues that need to be addressed, it is important that all parties involved in such processes agree on the "rules of engagement". Therefore, we propose to use a contract that specifies the composition of the public views of all participating parties. Each party may then implement its part of the contract such that the implementation (i.e., the private view) accords with the contract. In this paper, we define a suitable notion of accordance inspired by the asynchronous nature of services. Moreover, we present several transformation rules for incrementally building a private view such that accordance with the contract is guaranteed by construction. These rules include adding internal tasks as well as the reordering of messages and are therefore much more powerful than existing correctness-preserving construction rules.
    close
    close
  • Lohmann, Niels
    Decompositional Calculation of Operating Guidelines Using Free Choice Conflicts
    Niels Lohmann and Karsten Wolf, editors
    In Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008, volume 380 of CEUR Workshop Proceedings, CEUR-WS.org, sep 2008
    close
  • Lohmann, Niels, Kopp, Oliver, Leymann, Frank, Reisig, Wolfgang
    Analyzing BPEL4Chor: Verification and Participant Synthesis
    Marlon Dumas and Reiko Heckel, editors
    In Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, Springer-Verlag, 2008
    Choreographies offer means to capture global interactions between business processes of different partners. BPEL4Chor has been introduced to describe these interactions using BPEL. Currently, there are no formal methods available to verify BPEL4Chor choreographies. In this paper, we present how BPEL4Chor choreographies can be completely verified using Petri nets. A case study undermines that our verification techniques scale. Additionally, we show how the verification techniques can be used to generate a stub process for a partner taking part in a choreography. This is especially useful when the behavior of one participant is intended to follow the corresponding requirements of the other participants. Thus, the missing participant behavior can be generated and the error-prone design of that participant can be skipped.
    close
    close
  • 2007

  • Reisig, Wolfgang, Bretschneider, Jan, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
    Services as a Paradigm of Computation
    Cliff B. Jones and Zhiming Liu and Jim Woodcock, editors
    In Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj\orner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, volume 4700 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
    The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.
    close
    close
  • Lohmann, Niels, Verbeek, H. M. W., Ouyang, Chun, Stahl, Christian, Aalst, Wil M. P. van der
    Comparing and Evaluating Petri Net Semantics for BPEL
    Computer Science Report, Technische Universiteit Eindhoven, The Netherlands, aug 2007
    We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modeling decisions. These decisions together with their consequences are discussed.We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.
    close
    close
  • König, Dieter, Lohmann, Niels, Moser, Simon, Stahl, Christian, Wolf, Karsten
    Extending the Compatibility Notion for Abstract WS-BPEL Processes
    Preprint, Universität Rostock, Rostock, Germany, nov 2007
    WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.
    close
    close
  • Reisig, Wolfgang, Wolf, Karsten, Bretschneider, Jan, Kaschner, Kathrin, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
    Challenges in a Service-Oriented World
    volume 70 of ERCIM News 70, jul 2007
    Interacting services raise a number of new software engineering challenges. To meet these challenges, the behaviour of the involved services must be considered. We present results regarding the behaviour of services in isolation, the interaction of services in choreographies, the exchangeability of a service, and the synthesis of desired partner services.
    close
    close
  • Lohmann, Niels
    A Feature-Complete Petri Net Semantics for WS-BPEL 2.0
    Kees van Hee and Wolfgang Reisig and Karsten Wolf, editors
    In Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), University of Podlasie, jun 2007
    We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.
    close
    close
  • Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
    Operating Guidelines for Finite-State Services
    Jetty Kleijn and Alex Yakovlev, editors
    In 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007, Proceedings, volume 4546 of Lecture Notes in Computer Science, Springer-Verlag, 2007
    We study services modeled as open workflow nets (oWFN) and describe their behavior as service automata. Based on service automata, we introduce the concept of an operating guideline, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to properly interact (in this paper: deadlock-freely and with limited communication) with an oWFN N. It can be executed thus forming a properly interacting partner of N, or it can be used to support service discovery. An operating guideline for N is a particular service automaton S that is enriched with Boolean annotations. S interacts properly with the service automaton Prov, representing the behavior of N , and is able to simulate every other service that interacts properly with Prov . The attached annotations give complete information about whether or not a simulated service interacts properly with Prov, too.
    close
    close
  • Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
    Behavioral Constraints for Services
    Informatik-Berichte, Humboldt-Universität zu Berlin, may 2007
    Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be ``filtered'' yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.
    close
    close
  • Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
    Behavioral Constraints for Services
    Gustavo Alonso and Peter Dadam and Michael Rosemann, editors
    In Business Process Management, 5th International Conference, BPM 2007, Brisbane, Australia, September 24-28, 2007, Proceedings, volume 4714 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
    Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be "filtered" yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.
    close
    close
  • Lohmann, Niels
    A Feature-Complete Petri Net Semantics for WS-BPEL 2.0 and its Compiler BPEL2oWFN
    Informatik-Berichte, Humboldt-Universität zu Berlin, aug 2007
    We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification. This technical report is the extended version of the papers [1, 2] and can be seen as the sequel of [3].
    close
    close
  • 2006

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

    In Forschungsoffensive ''Software Engineering 2006'', Statuskonferenz, 26.-28. Juni 2006, , jul 2006
    close
  • Lohmann, Niels
    A Local Cut-off Criterion for Unfoldings of Safe Petri Nets
    , editors
    In Proceedings of the Doctoral Consortium ACSD \& Petri Nets 2006, , Turku, Finland, jun 2006
    Finite prefixes of branching processes are a compact way to represent the state space of finite safe systems. McMillan in [1] formulated a cut-off criterion stating under which conditions the (usually infinite) maximal branching process can be truncated without loosing reachable markings. However, this criterion depends on the reachable markings itself and thus suffers the state explosion problem. In this work, we propose local cut-off criteria that base on partial markings.
    close
    close
  • 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
  • Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
    Operating Guidelines for Finite-State Services
    Informatik-Berichte, , dec 2006
    We introduce the concept of an operating guideline for an arbitrary finite-state service P, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to correctly (in this paper: deadlock-free) communicate with P. It can further be executed or used for service discovery. An operating guideline for P is a particular service S that is enriched with annotations. S communicates deadlock-free with P and is able to simulate every other service that communicates deadlock-free with P. The attached annotations give complete information about whether or not a simulated service is deadlock-free, too.
    close
    close
  • 2005

  • Lohmann, Niels

    Diplomarbeit, sep 2005
    close
    close
  • Lohmann, Niels

    Studienarbeit, jun 2005
    close
    close

Müller, Richard (14)

Müller, Richard

    2014

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

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

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

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

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

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

Martens, Axel (19)

Martens, Axel

    2007

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

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

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

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

    Dissertation, 2003
    close
  • 2001

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

  • Kindler, Ekkart, Martens, Axel, Reisig, Wolfgang
    Inter-operability of Workshop Applications - Local Criteria for Global Soundness
    , editors
    In Business Process Management, volume 1806 of Lecture Notes in Computer Science, Springer-Verlag, 2000
    close
  • Kindler, Ekkart, Martens, Axel
    Cross-talk revisited - What's the problem?
    volume 58 of Petri Net Newsletter 58, 2000
    close
  • 1999

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

    , editors
    In , , jun 1999
    close
  • 1997

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

Massuthe, Peter (34)

Massuthe, Peter

    2010

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

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

  • Massuthe, Peter, Serebrenik, Alexander, Sidorova, Natalia, Wolf, Karsten
    Can I find a Partner?
    Preprint, , Rostock, Germany, mar 2008
    We study open nets as Petri net models of web services, with a link to the practically relevant language WS-BPEL. For those nets, we investigate the problem of serviceableness which we consider as fundamental as the successful notion of soundness for workflow nets, i.e. Petri net models of business processes and workflows. While we could give algorithmic solutions to the serviceableness problem for subclasses of open nets in earlier work, this article shows that the problem is in general undecidable.
    close
    close
  • 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
  • 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
  • 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
  • Massuthe, Peter, Weinberg, Daniela
    Fiona: A Tool to Analyze Interacting Open Nets
    Niels Lohmann and Karsten Wolf, editors
    In Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008, volume 380 of CEUR Workshop Proceedings, CEUR-WS.org, sep 2008
    close
  • Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
    From Public Views to Private Views -- Correctness-by-Design for Services
    Marlon Dumas and Reiko Heckel, editors
    In Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, Springer-Verlag, 2008
    Service orientation is a means for integrating across diverse systems. Each resource, whether an application, system, or trading partner, can be accessed as a service. The resulting architecture, often referred to as SOA, has been an important enabler for interorganizational processes. Apart from technological issues that need to be addressed, it is important that all parties involved in such processes agree on the "rules of engagement". Therefore, we propose to use a contract that specifies the composition of the public views of all participating parties. Each party may then implement its part of the contract such that the implementation (i.e., the private view) accords with the contract. In this paper, we define a suitable notion of accordance inspired by the asynchronous nature of services. Moreover, we present several transformation rules for incrementally building a private view such that accordance with the contract is guaranteed by construction. These rules include adding internal tasks as well as the reordering of messages and are therefore much more powerful than existing correctness-preserving construction rules.
    close
    close
  • 2007

  • Reisig, Wolfgang, Bretschneider, Jan, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
    Services as a Paradigm of Computation
    Cliff B. Jones and Zhiming Liu and Jim Woodcock, editors
    In Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj\orner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, volume 4700 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
    The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.
    close
    close
  • Massuthe, Peter, Wolf, Karsten
    An Algorithm for Matching Non-deterministic Services with Operating Guidelines
    volume 2 of International Journal of Business Process Integration and Management (IJBPIM) 2 (2), 2007
    Interorganisational cooperation is more and more organised by the paradigm of services. Service-Oriented Architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester and the service broker, together with the three operations publish, find and bind. We provide a formal method based on non-deterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artefact to realise the publish operation. In our approach, the find operation reduces to a matching problem between the requesters service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free interaction. In this paper, matching of deterministic as well as non-deterministic automata with operating guidelines is presented.
    close
    close
  • Aalst, Wil M. P. van der, Massuthe, Peter, Mooij, Arjan J., Stahl, Christian, Wolf, Karsten
    Erratum -- Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
    Informatik-Berichte, Humboldt-Universität zu Berlin, jun 2007
    close
  • Reisig, Wolfgang, Wolf, Karsten, Bretschneider, Jan, Kaschner, Kathrin, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
    Challenges in a Service-Oriented World
    volume 70 of ERCIM News 70, jul 2007
    Interacting services raise a number of new software engineering challenges. To meet these challenges, the behaviour of the involved services must be considered. We present results regarding the behaviour of services in isolation, the interaction of services in choreographies, the exchangeability of a service, and the synthesis of desired partner services.
    close
    close
  • Kaschner, Kathrin, Massuthe, Peter, Wolf, Karsten
    Symbolic Representation of Operating Guidelines for Services
    volume 72 of Petri Net Newsletter 72, apr 2007
    close
  • Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
    Behavioral Constraints for Services
    Informatik-Berichte, Humboldt-Universität zu Berlin, may 2007
    Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be ``filtered'' yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.
    close
    close
  • Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
    Behavioral Constraints for Services
    Gustavo Alonso and Peter Dadam and Michael Rosemann, editors
    In Business Process Management, 5th International Conference, BPM 2007, Brisbane, Australia, September 24-28, 2007, Proceedings, volume 4714 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
    Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be "filtered" yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.
    close
    close
  • Aalst, Wil M. P. van der, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
    Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
    Informatik-Berichte, Humboldt-Universität zu Berlin, jun 2007
    A contract specifies an interorganizational process together with a distribution of responsibilities for the activities among the parties involved. In this paper, we formally show how a party can implement its part of the contract such that the implementation accords with the contract. We propose a formal notion of a contract and give a criterion for accordance between a local implementation and a contract such that, if all local implementations accord with the contract, the overall process is deadlock-free and it is always possible to terminate properly. Then, we sketch a technique for automatically checking the proposed accordance criterion. Finally, we present accordance-preserving transformation rules. These rules can be used to implement a part of the contract while preserving the accordance criterion.
    close
    close
  • Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
    Operating Guidelines for Finite-State Services
    Jetty Kleijn and Alex Yakovlev, editors
    In 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007, Proceedings, volume 4546 of Lecture Notes in Computer Science, Springer-Verlag, 2007
    We study services modeled as open workflow nets (oWFN) and describe their behavior as service automata. Based on service automata, we introduce the concept of an operating guideline, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to properly interact (in this paper: deadlock-freely and with limited communication) with an oWFN N. It can be executed thus forming a properly interacting partner of N, or it can be used to support service discovery. An operating guideline for N is a particular service automaton S that is enriched with Boolean annotations. S interacts properly with the service automaton Prov, representing the behavior of N , and is able to simulate every other service that interacts properly with Prov . The attached annotations give complete information about whether or not a simulated service interacts properly with Prov, too.
    close
    close
  • 2006

  • 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, Wolf, Karsten
    An Algorithm for Matching Nondeterministic Services with Operating Guidelines
    Informatik-Berichte, , 2006
    Interorganizational cooperation is more and more organizedby the paradigm of services. Service-oriented architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester, and the service broker, together with the three operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artifact to realize the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlockfree communication. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.
    close
    close
  • Massuthe, Peter, Wolf, Karsten
    Operating Guidelines for Services
    volume 70 of Petri Net Newsletter 70, apr 2006
    In the service-oriented architecture (SOA), we distinguish three roles of service owners: service providers, service requesters, and service brokers, and the three standard operations publish, find, and bind. We provide a formal method based on Petri nets to model services. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester's service and the operating guideline.
    close
    close
  • Massuthe, Peter, Wolf, Karsten
    An Algorithm for Matching Nondeterministic Services with Operating Guidelines
    Frank Leymann and Wolfgang Reisig and Satish R. Thatte and Wil M. P. van der Aalst, editors
    In The Role of Business Processes in Service Oriented Architectures, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2006
    Interorganizational cooperation is more and more organized by the paradigm of services. Service-oriented architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester, and the service broker, together with the three operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artifact to realize the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free communication. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.
    close
    close
  • Kaschner, Kathrin, Massuthe, Peter, Wolf, Karsten

    Daniel Moldt, editors
    In , , sep 2006
    close
  • Lohmann, Niels, Massuthe, Peter, Wolf, Karsten
    Operating Guidelines for Finite-State Services
    Informatik-Berichte, , dec 2006
    We introduce the concept of an operating guideline for an arbitrary finite-state service P, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to correctly (in this paper: deadlock-free) communicate with P. It can further be executed or used for service discovery. An operating guideline for P is a particular service S that is enriched with annotations. S communicates deadlock-free with P and is able to simulate every other service that communicates deadlock-free with P. The attached annotations give complete information about whether or not a simulated service is deadlock-free, too.
    close
    close
  • 2005

  • Massuthe, Peter, Schmidt, Karsten
    Operating Guidelines for Services
    Karsten Schmidt and Christian Stahl, editors
    In , , sep 2005
    In the service-oriented architecture (SOA), we distinguish three roles of service owners:service providers, service requesters, and service brokers, and the three standard operations publish, find, and bind. We provide a formal method based on Petri nets to model services. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline.
    close
    close
  • Massuthe, Peter, Schmidt, Karsten
    Operating Guidelines - an Automata-Theoretic Foundation for the Service-Oriented Architecture
    Kai-Yuan Cai and Atsushi Ohnishi and M.F. Lau, editors
    In Proceedings of the Fifth International Conference on Quality Software (QSIC 2005), IEEE Computer Society, Melbourne, Australia, sep 2005
    In the service-oriented architecture (SOA), we distinguish three roles of service owners: service providers, service requesters, and service brokers. Each service provider publishes information to the broker about how requesters can interact with its service. Thus, the broker can assign a fitting service provider to a querying requester. We propose the information published to the broker to be operating guidelines. Operating guidelines are essentially communication instructions for the service requester. We present an automata-theoretic approach that is centered around operating guidelines and is capable of implementing all tasks arising in the SOA.
    close
    close
  • Massuthe, Peter, Schmidt, Karsten
    Matching Nondeterministic Services with Operating Guidelines
    Informatik-Berichte, , jun 2005
    Abstract Interorganizational cooperation is more and more organizedby the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester?s service and operating guidelines. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.
    close
    close
  • Massuthe, Peter, Schmidt, Karsten
    Operating Guidelines - an Alternative to Public View
    Informatik-Berichte, , 2005
    We propose operating guidelines as artifacts for publishing information about how to communicate with a business process that is intended to be provided as a service. We present an approach to compute operating guidelines fully automatically. We compare operating guidelines with the concept of public view.
    close
    close
  • Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
    An Operating Guideline Approach to the SOA
    Informatik-Berichte, , 2005
    Interorganizational cooperation is more and more organized by the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester?s and provider?s services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline. Binding of a requester?s and a provider?s service is therefore guaranteed to result in a well-behaving cooperating service.
    close
    close
  • Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
    An Operating Guideline Approach to the SOA
    In 2nd South-East European Workshop on Formal Methods 2005 (SEEFM05), Ohrid, Republic of Macedonia, 2005
    close
  • Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
    An Operating Guideline Approach to the SOA
    volume 1 of Annals of Mathematics, Computing \& Teleinformatics 1 (3), 2005
    Interorganizational cooperation is more andmore organized by the paradigm of services. The serviceoriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester's and provider's services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester's service and the operating guideline. Binding of a requester's and a provider's service is therefore guaranteed to result in a well-behaving cooperating service. At this time, the approach is limited to acyclic Petri nets.
    close
    close
  • 2004

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

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

Parnjai, Jarungjit (3)

Parnjai, Jarungjit

    2011

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

  • Parnjai, Jarungjit, Stahl, Christian, Wolf, Karsten
    A finite representation of all substitutable services and its applications
    Oliver Kopp and Niels Lohmann, editors
    In Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, mar 2009
    We present a finite representation of all substitutable services P' of a given service P. We show that our approach can be used for at least two applications: (1) given a finite set of services \mathcalP = P1, ..., Pn, we provide a representation of all services P' that can substitute every Pi \in \mathcalP, and (2) given a service P'' that cannot substitute a service P, we find the most similar service P* to P'' that can substitute P.
    close
    close

Peuker, Sibylle (7)

Peuker, Sibylle

    2001

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

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

  • Peuker, Sibylle
    Phased Decomposition of Distributed Algorithms
    Informatik-Berichte, , apr 1999
    close
  • Kindler, Ekkart, Peuker, Sibylle
    Integrating distributed algorithms into distributed systems
    volume 37 of Fundamenta Informaticae 37 (3), feb 1999
    close
  • 1997

  • Weber, Michael, Walter, Rolf, , Vesper, Tobias, Reisig, Wolfgang, Peuker, Sibylle, Kindler, Ekkart, ,
    DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen
    Informatik-Berichte, , dec 1997
    close
  • Peuker, Sibylle
    Invariant property preserving extensions of elementary Petri nets
    1997
    close

Prüfer, Robert (6)

Prüfer, Robert

    2014

  • Duske, Kristian, Müller, Richard, Prüfer, Robert, Stöhr, Daniel
    A BPMN Model of the Charite Stroke Treatment Process
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2014
    close
  • Prüfer, Robert, Sürmeli, Jan
    Introducing Configurability into Scenario-Based Specification of Business Processes
    In ZEUS, 2014
    close
  • 2012

  • Fahland, Dirk, Prüfer, Robert
    Data and Abstraction for Scenario-Based Modeling with Petri Nets
    In Petri Nets, 2012
    close
  • 2010

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

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

Reisig, Wolfgang (138)

Reisig, Wolfgang

    2017

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

  • Völlinger, Kim, Reisig, Wolfgang
    Certifcation of Distributed Algorithms Solving Problems with Optimal Substructure
    In Software Engineering and Formal Methods, 2015
    close
  • 2013

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

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

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

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

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

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

  • Reisig, Wolfgang, Bretschneider, Jan, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
    Services as a Paradigm of Computation
    Cliff B. Jones and Zhiming Liu and Jim Woodcock, editors
    In Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj\orner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, volume 4700 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
    The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.
    close
    close
  • Hohberg, Bodo, Reisig, Wolfgang, Wu, Bixia
    Entwurf und Verifikation nachrichtenbasierter verteilter Algorithmen durch verteilende Verfeinerung
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2007
    close
    close
  • Reisig, Wolfgang, Wolf, Karsten, Bretschneider, Jan, Kaschner, Kathrin, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
    Challenges in a Service-Oriented World
    volume 70 of ERCIM News 70, jul 2007
    Interacting services raise a number of new software engineering challenges. To meet these challenges, the behaviour of the involved services must be considered. We present results regarding the behaviour of services in isolation, the interaction of services in choreographies, the exchangeability of a service, and the synthesis of desired partner services.
    close
    close
  • 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, Reisig, Wolfgang
    An ASM-Characterization of a Class of Distributed Algorithms
    In Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis, Festschrift volume of Lecture Notes in Computer Science, Springer, 2007
    close
  • Reisig, Wolfgang
    The Decent Philosophers: An Exercise in Concurrent Behaviour
    volume 80 of Fundamenta Informaticae 80 (1-3), nov 2007
    Concurrent runs reveal more insight into distributed systems than interleaved runs. This is shown by help of Dijkstra's paradigm of five philosophers.
    close
    close
  • 2006

  • 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
  • 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
  • Glausch, Andreas, Reisig, Wolfgang
    How Expressive are Petri Net Schemata?
    Susanna Donatelli and P. S. Thiagarajan, editors
    In Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, Springer, 2006
    Petri net schemata are an intuitive and expressive approach to describe high-level Petri nets. A Petri net schema is a Petri net with edges and transitions inscribed by terms and Boolean expressions, respectively. A concrete high-level net is gained by interpreting the symbols in the inscriptions by a structure. Its semantics can then be described in terms of a transition system. Therefore, the semantics of a Petri Net schema can be conceived as a family of transition systems indexed by structures. In this paper we characterize the expressive power of a general version of Petri net schemata. For that purpose we examine families of transition systems in general and characterize the families as generated by Petri net schemata. It turns out that these families of transition systems can be characterized by simple and intuitive requirements.
    close
    close
  • Acu, Baver, Reisig, Wolfgang
    Compensation in Workflow Nets
    Susanna Donatelli and P. S. Thiagarajan, editors
    In Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, Springer, 2006
    close
  • Brauer, Wilfried, Reisig, Wolfgang
    Carl Adam Petri und die ``Petrinetze''
    volume 29 of Informatik-Spektrum 29 (5), oct 2006
    close
  • Glausch, Andreas, Reisig, Wolfgang
    On the Expressive Power of Unbounded-Nondeterministic Abstract State Machines
    Informatik-Berichte, , dec 2006
    Conventional computational models assume a symbolical representation of states. Gurevich's Abstract State Machines (ASMs) take a more liberal position: any mathematical structure may serve as a state. Gurevich characterizes the expressive power of sequential ASMs in a non-trivial theorem: he defines the class of \emphsequential algorithms by help of only a few, amazingly general requirements and proves this class to be equivalent to sequential ASMs. Later, this result has been extended to the class of bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among infinitely many alternatives. We define the class of unbounded-nondeterministic algorithms by a conservative extension of Gurevich's original requirements to sequential algorithms. We show that this class is equivalent to unbounded-nondeterministic ASMs.
    close
    close
  • 2005

  • Reisig, Wolfgang
    Modeling- and Analysis Techniques for Web Services and Business Processes
    Martin Steffen and Gianluigi Zavattaro, editors
    In Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings, volume 3535 of Lecture Notes in Computer Science, Springer Verlag, may 2005
    Open distributed systems include in particular Web services and business processes. There is a need of techniques to model such systems formally, and to derive decisive properties from such models. Three such techniques are presented in this paper, exemplified by help of realistic examples, and mutually related w.r.t. their respective expressive power and the availability of analysis techniques.
    close
    close
  • Reisig, Wolfgang
    On the Expressive Power of Petri Net Schemata
    Gianfranco Ciardo and Philippe Darondeau, editors
    In Applications and Theory of Petri Nets 2005: 26th International Conference, ICATPN 2005, Miami, USA, June 20-25, 2005. Proceedings, volume 3536 of Lecture Notes in Computer Science, Springer Verlag, may 2005
    High-level Petri nets are frequently represented as Petri net schemas, with places, transitions and arcs inscribed by terms. A concrete system is then gained by interpreting the symbols in those terms. The behavior of a concrete system is a transition system. The composition of all those transition systems represents the behavior of the Petri net schema. This paper characterizes the expressive power of (a basic class of) Petri net schemas. It turns out that quite simple as well as quite general requirements at a transition system suffice to generate it by such a Petri net schema.
    close
    close
  • Stahl, Christian, Reisig, Wolfgang, Krstic, Milos
    Hazard Detection in a GALS Wrapper: A Case Study
    , editors
    In Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD'05), IEEE Computer Society, St. Malo, France, jun 2005
    An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion two techniques to reduce the model's state space are presented. By use of these techniques we detected several potential hazards and a deadlock in the wrapper.
    close
    close
  • Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian
    Kommunizierende Workflow-Services modellieren und analysieren
    Informatik - Forschung und Entwicklung, Springer-Verlag, oct 2005
    close
    close
  • 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
  • Stahl, Christian, Reisig, Wolfgang, Krstic, Milos
    Hazard Detection in a GALS Wrapper: a Case study
    Informatik-Berichte, , feb 2005
    An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion three techniques to reduce the model?s state space are presented. By use of these techniques we detected several potential hazards in the wrapper.
    close
    close
  • Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
    An Operating Guideline Approach to the SOA
    Informatik-Berichte, , 2005
    Interorganizational cooperation is more and more organized by the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester?s and provider?s services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline. Binding of a requester?s and a provider?s service is therefore guaranteed to result in a well-behaving cooperating service.
    close
    close
  • Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
    An Operating Guideline Approach to the SOA
    In 2nd South-East European Workshop on Formal Methods 2005 (SEEFM05), Ohrid, Republic of Macedonia, 2005
    close
  • Reisig, Wolfgang
    Modeling- and Analysis Techniques for Web Services and Business Processes
    Informatik-Berichte, , 2005
    close
  • Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian

    Informatik-Berichte, , feb 2005
    close
    close
  • Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
    An Operating Guideline Approach to the SOA
    volume 1 of Annals of Mathematics, Computing \& Teleinformatics 1 (3), 2005
    Interorganizational cooperation is more andmore organized by the paradigm of services. The serviceoriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester's and provider's services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester's service and the operating guideline. Binding of a requester's and a provider's service is therefore guaranteed to result in a well-behaving cooperating service. At this time, the approach is limited to acyclic Petri nets.
    close
    close
  • 2004

  • Alexander, Adrianna, Reisig, Wolfgang
    Compositional Temporal Logic Based on Partial Order
    Informatik-Berichte, , dec 2004
    close
  • Reisig, Wolfgang, Brade, A.
    ASM Models for Web Services
    Informatik-Berichte, , 2004
    close
  • Reisig, Wolfgang
    The computable kernel of Sequential Abstract State Machines
    Informatik-Berichte, , 2004
    close
  • Alexander, Adrianna, Reisig, Wolfgang
    Compositional Temporal Logic Based on Partial Order
    In 11th International Symposium on Temporal Representation and Reasoning (TIME'04), IEEE Computer Society, 2004
    The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. The logic supports a compositional design of systems: subsystems can be specified separately and then be integrated into one system. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.
    close
    close
  • 2003

  • Alexander, Adrianna, Reisig, Wolfgang
    Logic of Involved Variables - System Specification with Temporal Logic of Distributed Actions
    In Proc. of the 3rd International Conference on Application of Concurrency to System Design (ACSD'03), Guimaraes, Portugal , IEEE Computer Society, jun 2003
    The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA can be syntactically viewed as a slight extension of TLA. We propose a different semantical model based on partial order which evidently increases the expressiveness of the logic. Local variable updates in a system are explicitly modeled and expressed by TLDA formulas. Consequently, we can distinguish between concurrency and nondeterministic choice. All valuable features of TLA (composition is conjunction, implementation is implication) are retained. In addition, we are able to describe some important phenomena and properties typical for distributed systems.
    close
    close
  • Weber, Herbert, Ehrig, Hartmut, Reisig, Wolfgang, Borusan, Alexander, Lembke, Sabine, Dehnert, Juliane, Weber, Michael, Martens, Axel, Padberg, Julia, Ermel, Claudia, Qemali, A.
    The Petri Net Baukasten of the DFG Forschergruppe PETRI NET TECHNOLOGY
    Hartmut Ehrig and Wolfgang Reisig and Grzegorz Rozenberg and Herbert Weber, editors
    In Petri Net Technology for Communication-Based Systems, volume 2472 of Lecture Notes in Computer Science, Springer-Verlag, 2003
    In the long history of Petri nets a universe of Petri nets has evolved consisting of an enormously rich theory, a wide variety of tools, and numerous successful applications and case studies in various application domains. This vast variety is not any more handable for anyone working with Petri nets, which results in the strong need of a structured access to Petri nets. This structured access has been the main aim of the DFG-Forschergruppe PETRI NET TECHNOLOGY, which has developed the so-called Petri Net Baukasten for this purpose. It is designed to support Petri net experts, application developers and tool developers alike in their specific work with Petri nets. This paper presents an overview of the concepts, initial and 2nd installment of the Petri Net Baukasten, which have been presented at the 1st and 2nd International Colloquium on Petri Net Technologies for Modelling Communication Based Systems in 1999 and 2001, respectively.
    close
    close
  • Reisig, Wolfgang
    The Computable Kernel of ASM
    , editors
    In Abstract State Machines, Advances in Theory and Practice, 10th International Workshop, ASM 2003, Taormina, Italy, volume 2589 of Lecture Notes in Computer Science, 2003
    A rich variety of system models for sequential, deterministic systems has been suggested during recent decades, including automata, process algebras, many versions of Petri Nets, and models to describe the semantics of Programming languages. All models for sequential, deterministic systems assume a set S of states, or configurations, and a next state function $\upsilon: S \rightarrow S$.
    close
    close
  • Reisig, Wolfgang
    The Expressive Power of Abstract State Machines
    volume 22 of Computing and Informatics 22 (3), 2003
    Conventional computation models assume symbolic representations of states and actions. Gurevich's "Abstract-State Machine" model takes a more liberal position: Any mathematical structure may serve as a state. This results in "a computational model that is more powerful and more universal than standard computation models". We characterize the Abstract-State Machine model as a special class of transition systems that widely extends the class of "computable" transition systems. This characterization is based on a fundamental Theorem of Y. Gurevich.
    close
    close
  • Reisig, Wolfgang
    On Gurevich's Theorem on Sequential Algorithms
    volume 39 of Acta Informatica 39 (5), Springer-Verlag, 2003
    Abstract-State Machines have been introduced as ?a computation model that is more powerful and more universal than standard computation models?, by Yuri Gurevich in 1985 ([Gur85]). ASM gained much attention as a specification method, in particular for the description of the semantics of programming languages, communication protocols, distributed algorithms, etc. Gurevich proved recently that a sequential algorithm must only meet a few, liberal requirements, to be representable as an ASM. We re-formulate Gurevich?s requirements for sequential algorithms, as well as the semantics of ASM-programs and the proof of his main theorem. A couple of examples support and explain intuition and motivation of ASM.
    close
    close
  • 2002

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

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

  • Reisig, Wolfgang
    The Linear Theory of Multiset Based Dynamic Systems
    Cristian Calude and Gheorghe Paun and Grzegorz Rozenberg and Arto Salomaa, editors
    In Workshop on Multiset Processing (WMP 2000), volume 2235 of Lecture Notes in Computer Science, Springer-Verlag, 2000
    close
  • Reisig, Wolfgang
    Towards an ASM Thesis for Unconventional Algorithms
    Yuri Gurevich and Philipp W. Kutter and Martin Odersky and Lothar Thiele, editors
    In Abstract State Machines, volume 1912 of Lecture Notes in Computer Science, Springer-Verlag, 2000
    All descriptions of algorithms, be they formal or informal, employ data structures, operations on them, and some policy to cause operations be applied to data. Gurevich calls a formal description technique for algorithms algorithm universal if it allows for each informally described algorithm a formal representation that would essentially make precise the notions used in the informal description, not employing additional data, operations or steps. Gurevich's ASM thesis claims Abstract State Machines be algorithm universal for conventional, sequential algorithms. Here we are behind properties of formal presentations that are algorithm universal for unconventional, distributed algorithms.
    close
    close
  • Kindler, Ekkart, Martens, Axel, Reisig, Wolfgang
    Inter-operability of Workshop Applications - Local Criteria for Global Soundness
    , editors
    In Business Process Management, volume 1806 of Lecture Notes in Computer Science, Springer-Verlag, 2000
    close
  • Foremniak, Adrianna, Reisig, Wolfgang
    A Temporal Logic of Distributed Actions (TLDA)
    Informatik-Berichte, , 2000
    close
  • 1999

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

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

  • Ehrig, Hartmut, Reisig, Wolfgang
    An Algebraic View on Petri Nets.
    volume 61 of Bulletin of the EATCS 61, feb 1997
    close
  • Weber, Michael, Walter, Rolf, , Vesper, Tobias, Reisig, Wolfgang, Peuker, Sibylle, Kindler, Ekkart, ,
    DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen
    Informatik-Berichte, , dec 1997
    close
  • Reisig, Wolfgang
    Verteilte Algorithmen: Nutzen sie der Forschergruppe?
    1997
    close
  • Reisig, Wolfgang
    Interleaved progress, concurrent progress, and local progress
    D. A. Peled and V. R. Pratt and G. J. Holzmann, editors
    In Proceedings of the DIMACS workshop on Partial order methods in verification (POMIV '96), volume 29 of AMS Press, Inc., New York, NY, USA, 1997
    close
  • Kindler, Ekkart, Reisig, Wolfgang, , Walter, Rolf
    Petri Net Based Verification of Distributed Algorithms: An Example
    volume 9 of Formal Aspects of Computing 9 (4), Springer-Verlag, 1997
    close
  • Kindler, Ekkart, Reisig, Wolfgang
    Verification of Distributed Algorithms with Algebraic Petri Nets
    , editors
    In Foundations of Computer Science: Potential - Theory - Cognition, volume 1337 of Lecture Notes in Computer Science, Springer-Verlag, 1997
    close
  • 1996

  • Walter, Rolf, , Vesper, Tobias, Reisig, Wolfgang, Kindler, Ekkart, ,
    Memorandum: Petrinetzmodelle zur Verifikation verteilter Algorithmen
    Informatik-Berichte, , aug 1996
    close
  • Kindler, Ekkart, Reisig, Wolfgang
    Algebraic System Nets for Modelling Distributed Algorithms
    volume 51 of Petri Net Newsletter 51, nov 1996
    close
  • Ehrig, Hartmut, Reisig, Wolfgang, Weber, Herbert
    Kick-Off-Workshop der DFG-Forschergruppe 'Petrinetz-Technologie'
    Informatik-Berichte, , dec 1996
    close
  • Reisig, Wolfgang
    Temporallogische Verifikation verteilter Algortihmen: Mehr als nur eine Variante
    , editors
    In Formal Methods for Concurrency, GI-Kolloquium, Fachberichte der TU Dresden, , jul 1996
    close
  • Kindler, Ekkart, Reisig, Wolfgang, , Walter, Rolf
    Petri Net Based Verification of Distributed Algorithms: An Example
    Informatik-Berichte, , may 1996
    close
  • Reisig, Wolfgang
    Modelling and Verification of Distributed Algorithms
    In CONCUR 96, volume 1119 of Lecture Notes in Computer Science, Springer-Verlag, 1996
    close
  • Reisig, Wolfgang, Kindler, Ekkart, Vesper, Tobias, Völzer, Hagen, Walter, Rolf
    Distributed Algorithms for Networks of Agents.
    In Petri Nets (2), 1996
    close
  • Reisig, Wolfgang, Rozenberg, Grzegorz
    Informal Introduction to Petri Nets
    In Petri Nets, 1996
    close
  • Desel, Jörg, Reisig, Wolfgang
    The Synthesis Problem of Petri Nets.
    volume 33 of Acta Informatica 33 (4), 1996
    close
  • 1995

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Sürmeli, Jan (17)

Sürmeli, Jan

    2016

  • Triebel, Marvin, Sürmeli, Jan
    Homogeneous Equations of Algebraic Petri Nets
    volume abs/1606.05490 of CoRR abs/1606.05490, 2016
    close
  • Triebel, Marvin, Sürmeli, Jan
    Homogeneous Equations of Algebraic Petri Nets
    Jos\'ee Desharnais and Radha Jagadeesan, editors
    In 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Qu\'ebec City, Canada, volume 59 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016
    close
  • Triebel, Marvin, Sürmeli, Jan
    Characterizing Stable and Deriving Valid Inequalities of Petri Nets
    volume 146 of Fundam. Inform. 146 (1), 2016
    close
  • 2014

  • Prüfer, Robert, Sürmeli, Jan
    Introducing Configurability into Scenario-Based Specification of Business Processes
    In ZEUS, 2014
    close
  • 2013

  • Sürmeli, Jan, Triebel, Marvin
    Cost-optimizing compositions of services - analysis and synthesis
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2013
    close
  • Sürmeli, Jan, Triebel, Marvin
    Synthesizing Cost-Minimal Partners for Services
    Basu, Samik and Pautasso, Cesare and Zhang, Liang and Fu, Xiang, editors
    In Service-Oriented Computing, volume 8274 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2013
    close
  • 2012

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

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

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

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

Stahl, Christian (53)

Stahl, Christian

    2013

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

  • Müller, Richard, Aalst, Wil M. P. van der, Stahl, Christian
    Conformance Checking of Services Using the Best Matching Private View
    In Proceedings of the 9th International Workshop on Web Services and Formal Methods, WS-FM 2012 September 6-7, 2012, Tallinn, Estonia, 2012
    close
  • Vogler, Walter, Stahl, Christian, Müller, Richard
    A Trace-Based Semantics for Responsiveness
    Jens Brandt and Keijo Heljanko, editors
    In Proceedings of the 12th International Conference on Application of Concurrency to System Design, ACSD 2012, Hamburg, Germany, June 27-29, 2012, IEEE, 2012
    close
  • Müller, Richard, Stahl, Christian
    Deciding the Precongruence for Deadlock Freedom Using Operating Guidelines
    , editors
    In Proceedings of the 2nd International Workshop on Petri Nets Compositions, CompoNet'12, Hamburg, Germany, June 25-26, 2012, volume 853 of CEUR Workshop Proceedings, CEUR-WS.org, jun 2012
    close
  • 2011

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

  • Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
    Multiparty Contracts: Agreeing and Implementing Interorganizational Processes
    volume 53 of The Computer Journal 53 (1), 2010
    To implement an interorganizational process between different enterprizes, one needs to agree on the ``rules of engagement''. These can be specified in terms of a contract that describes the overall intended process and the duties of all parties involved. We propose to use such a process-oriented contract which can be seen as the composition of the public views of all participating parties. Based on this contract each party may locally implement its part of the contract such that the implementation (the private view) agrees on the contract. In this paper, we propose a formal notion for such process-oriented contracts and give a criterion for accordance between a private view and its public view. The public view of a party can be substituted by a private view if and only if the private view accords with the public view. Using the notion of accordance the overall implemented process is guaranteed to be deadlock-free and it is always possible to terminate properly. In addition, we present a technique for automatically checking our accordance criterion. A case study illustrates how our proposed approach can be used in practice.
    close
    close
  • Mooij, Arjan J., Stahl, Christian, Voorhoeve, Marc
    Relating Fair Testing and Accordance for Service Replaceability
    Journal of Logic and Algebraic Programming, 2010
    The accordance pre-order describes whether a service can safely be replaced by another service. That is, all partners for the original service should be partners for the new service. Partners for a service interact with the service in such a way that always a certain common goal can be reached. We relate the accordance pre-order to the pre-orders known from the linear-branching time spectrum, notably fair testing. The differences between accordance and fair testing include the modeling of termination and success, and the parts of the services that cannot be used reliably by any partner. Apart from the theoretical results, we address the practical relevance of the introduced concepts.
    close
    close
  • 2009

  • Parnjai, Jarungjit, Stahl, Christian, Wolf, Karsten
    A finite representation of all substitutable services and its applications
    Oliver Kopp and Niels Lohmann, editors
    In Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, CEUR-WS.org, mar 2009
    We present a finite representation of all substitutable services P' of a given service P. We show that our approach can be used for at least two applications: (1) given a finite set of services \mathcalP = P1, ..., Pn, we provide a representation of all services P' that can substitute every Pi \in \mathcalP, and (2) given a service P'' that cannot substitute a service P, we find the most similar service P* to P'' that can substitute P.
    close
    close
  • Wolf, Karsten, Stahl, Christian, Ott, Janine, Danitz, Robert
    Verifying Livelock Freedom in an SOA Scenario
    Stephen Edwards and Walter Vogler, editors
    In Proceedings of the Ninth International Conference on Application of Concurrency to System Design (ACSD'09), IEEE Computer Society, Augsburg, Germany, jul 2009
    In a service-oriented architecture (SOA), a service broker assigns a previously published service (stored in a service registry) to a service requester. It is desirable for the composition of the requesting and the assigned service to interact properly. While proper interaction is often reduced to deadlock freedom of the composed system, we additionally consider livelock freedom as a desirable property for the interaction of services. In principle, deadlock- and livelock freedom can be verified by inspecting the state space of the composition of (public views of) the involved services. The contribution of this paper is to propose a methodology to build that state space from pre-computed fragments which are computed upon publishing a service. That way, we shift computation time from the time critical request phase of service brokerage to the less critical publish phase. Interestingly, our setting enables state space reduction methods that are intrinsically different from traditional state space reductions.
    close
    close
  • Aalst, Wil M. P. van der, Mooij, Arjan J., Stahl, Christian, Wolf, Karsten
    Service Interaction: Patterns, Formalization, and Analysis
    Marco Bernardo and Luca Padovani and Gianluigi Zavattaro, editors
    In Formal Methods for Web Services (SFM 2009), volume 5569 of Springer-Verlag, apr 2009
    As systems become more service oriented and processes increasingly cross organizational boundaries, interaction becomes more important. New technologies support the development of such systems. However, the paradigm shift towards service orientation, requires a fundamentally different way of looking at processes. This survey aims to provide some foundational notions related to service interaction. A set of service interaction patterns is given to illustrate the challenges in this domain. Moreover, key results are given for three of these challenges: (1) How to expose a service?, (2) How to replace and refine services?, and (3) How to generate service adapters? These challenges will be addressed in a Petri net setting. However, the results extend to other languages used in this domain.
    close
    close
  • Liske, Nannette, Lohmann, Niels, Stahl, Christian, Wolf, Karsten
    Another Approach to Service Instance Migration
    Luciano Baresi and Chi-Hung Chi and Jun Suzuki, editors
    In Service-Oriented Computing - ICSOC 2009, 7th International Conference, Stockholm, Sweden, November 24-27, 2009. Proceedings, Lecture Notes in Computer Science, Springer-Verlag, nov 2009
    Services change over time, be it for internal improvements, be it for external requirements such as new legal regulations. For long running services, it may even be necessary to change a service while instances are actually running and interacting with other services. This problem is referred to as instance migration. We present a novel approach to the behavioral (service protocol) aspects of instance migration. We apply techniques for finitely characterizing the set of all correctly interacting partners to a given service. The approach assures that migration does not introduce behavioral problems with any running partner of the original service. Our technique scales up to services with thousands of states, including models of real WS-BPEL processes.
    close
    close
  • Lohmann, Niels, Verbeek, Eric, Ouyang, Chun, Stahl, Christian
    Comparing and Evaluating Petri Net Semantics for BPEL
    volume 4 of International Journal of Business Process Integration and Management (IJBPIM) 4 (1), 2009
    We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modelling decisions. These decisions together with their consequences are discussed. We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.
    close
    close
  • 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
  • Hee, Kees van, Verbeek, Eric, Stahl, Christian, Sidorova, Natalia
    A Framework for Linking and Pricing No-Cure-No-Pay Services
    Kurt Jensen and Wil M. P. van der Aalst, editors
    volume 2 of Lecture Notes in Computer Science, vol. 5460, Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems 2, Springer-Verlag, mar 2009
    In this paper, we present a framework that allows us to orchestrate web services such that the web services involved in this orchestration interact properly. To achieve this, we predefine service interfaces and certain routing constructs. Furthermore, we define a number of rules to incrementally compute the price of such a properly interacting orchestration (i.e. a web service) from the price of its web services. The fact that a web service gets only payed after its service is delivered (no-cure-no-pay) is reflected by considering a probability of success. To determine a safe price that includes the risk a web service takes, we consider the variance of costs.
    close
    close
  • Stahl, Christian, Wolf, Karsten
    Deciding Service Composition and Substitutability Using Extended Operating Guidelines
    volume 68 of Data Knowl. Eng. 68 (9), 2009
    We study the correct interaction between services using the following notion for correctness: there is no deadlock in the interaction of the services, and a given set of activities is not dead, that is, each activity in this set is executed in at least one run. The second condition has not been studied before. An operating guideline of a service P is an operational characterization of all deadlock-free interacting partners of P. In this paper, we present an extension of the concept of an operating guideline to characterize all correctly interacting partners of a service P. This extension can be used for answering at least the following two questions. First, given a service R, does R interact correctly with P? Second, given a service P', can P be substituted by P', that is, is every correctly interacting partner of P a correctly interacting partner of P', too?
    close
    close
  • Stahl, Christian
    Service Substitution - A Behavioral Approach Based on Petri Nets
    Dissertation, Dec 2009
    Service-Oriented Computing is an emerging computing paradigm that supports the modular design of (software) systems. Complex systems are designed by composing less complex systems, called services. Such a (complex) system is a distributed application often involving several cooperating enterprises. As a system usually changes over time, individual services will be substituted by other services. Substituting one service by another one should not affect the correctness of the overall system. Assuring correctness becomes particularly challenging, as the services rely on each other, and each of the involved enterprises only oversees a part of the overall system. In addition, services communicate asynchronously which makes the analysis even more difficult. For this reason, formal methods to support service substitution are indispensable. In this thesis, we study service substitution at the level of service models. Thereby we restrict ourselves to service behavior. As a formalism to model service behavior, we use Petri nets. The first contribution of this thesis is the definition of several substitutability criteria that are suitable in the context of Service-Oriented Computing. Substituting a service S by a service S' should preserve some behavioral properties of the overall system. For each set of behavioral properties and a given service S, there exists a set of behaviorally compatible services for S. A substitutability criterion defines which of these behaviorally compatible services of S have to be preserved by S'. We relate our substitutability criteria to preorders and equivalences known from process theory. The second contribution of this thesis is to present, for each substitutability criterion, a procedure to decide whether a service S' can substitute a service S. The decision requires the comparison of the in general infinite sets of behaviorally compatible services for the services S and S'. Hence, we extend existing work on an abstract representation of all behaviorally compatible services for a given service. For each notion of behavioral compatibility, we present an algorithmic solution to represent all behaviorally compatible services. Based on these representations, we can decide substitutability of a service S by a service S'. The third contribution of this thesis is a method to support the design of a service S' that can substitute a service $S$ according to a substitutability criterion. Our approach is to derive a service S' from the service S by stepwise transformation. To this end, we present several transformation rules. Finally, we formalize and we extend the equivalence notion for services specified in the language WS-BPEL. That way, we demonstrate the applicability of our work.
    close
    close
  • 2008

  • 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
  • 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
  • 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
  • Stahl, Christian, Wolf, Karsten
    Covering Places and Transitions in Open Nets
    Marlon Dumas and Manfred Reichert, editors
    In Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, Springer-Verlag, sep 2008
    We present a finite representation of all services M where the composition with a given service N is deadlock-free, and a given set of activities of N can be covered (i.e. is not dead). Our representation is an extension of the existing notion of an operating guideline which only cared about deadlock freedom. We further present an algorithm to decide whether a service M matches with the extended operating guideline of N.
    close
    close
  • Hee, Kees M. van, Verbeek, H.M.W., Stahl, Christian, Sidorova, Natalia
    A Framework for Linking and Pricing No-Cure-No-Pay Services
    Computer Science Report, Technische Universiteit Eindhoven, Eindhoven, The Netherlands, jun 2008
    In this paper, we present a framework that allows us to orchestrate web services such that the web services involved in this orchestration interact properly. To achieve this, we predefine service interfaces and certain routing constructs. Furthermore, we define a number of rules to incrementally compute the price of such a properly interacting orchestration (i.e. a web service) from the price of its web services. The fact that a web service gets only payed after its service is delivered (no-cure-no-pay) is reflected by considering a probability of success. To determine a safe price that includes the risk a web service takes, we consider the variance of costs.
    close
    close
  • Aalst, Wil M. P. van der, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Wolf, Karsten
    From Public Views to Private Views -- Correctness-by-Design for Services
    Marlon Dumas and Reiko Heckel, editors
    In Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, Springer-Verlag, 2008
    Service orientation is a means for integrating across diverse systems. Each resource, whether an application, system, or trading partner, can be accessed as a service. The resulting architecture, often referred to as SOA, has been an important enabler for interorganizational processes. Apart from technological issues that need to be addressed, it is important that all parties involved in such processes agree on the "rules of engagement". Therefore, we propose to use a contract that specifies the composition of the public views of all participating parties. Each party may then implement its part of the contract such that the implementation (i.e., the private view) accords with the contract. In this paper, we define a suitable notion of accordance inspired by the asynchronous nature of services. Moreover, we present several transformation rules for incrementally building a private view such that accordance with the contract is guaranteed by construction. These rules include adding internal tasks as well as the reordering of messages and are therefore much more powerful than existing correctness-preserving construction rules.
    close
    close