Publications of Year 2009
Dissertations and Habilitations
Peter Massuthe. Operating Guidelines for Services. Dissertation, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II; Eindhoven University of Technology, April 2009. Note: ISBN 978-90-386-1702-2.
@PhDThesis{Massuthe2009_diss, author = {Peter Massuthe}, title = {{Operating Guidelines for Services}}, school = {Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II; Eindhoven University of Technology}, year = 2009, month = Apr, type = {Dissertation}, Pdf = {http://www2.informatik.hu-berlin.de/top/download/publications/Massuthe2009_OGfS_dissertation.pdf}, note = {ISBN 978-90-386-1702-2} }Christian Stahl. Service Substitution - A Behavioral Approach Based on Petri Nets. Dissertation, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II; Eindhoven University of Technology, December 2009. Note: ISBN 978-90-386-2065-7.
Abstract: 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. @PhDThesis{Stahl2009_diss, author = {Christian Stahl}, title = {{Service Substitution - A Behavioral Approach Based on Petri Nets}}, school = {Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II; Eindhoven University of Technology}, year = 2009, month = Dec, type = {Dissertation}, Pdf = {http://www2.informatik.hu-berlin.de/top/download/publications/Stahl2009-diss.pdf}, note = {ISBN 978-90-386-2065-7}, Keywords = {Bedienungsanleitung, Services, SOA, offene Workflownetze, Exchangeability}, abstract = {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.} }
Journal and Book Articles
Wilfried Brauer and Wolfgang Reisig. Carl Adam Petri and ''Petri Nets''. Fundamental Concepts in Computer Science, 3: 129--139, 2009.
@Article{BrauerR2009_fcics, Author = {Wilfried Brauer and Wolfgang Reisig}, Title = {Carl Adam Petri and ''Petri Nets''}, Journal = {Fundamental Concepts in Computer Science}, Publisher = {Imperial College Press}, Editor = {Erol Gelenbe and Jean-Pierre Kahane (Hrsg.)}, Series = {Advances in Computer Science and Engineering: Texts}, Volume = {3}, Year = {2009}, Isbn = {978-1-84816-290-7, 1-84816-290-1}, Pages = {129--139} }Niels Lohmann, Eric Verbeek, and Remco Dijkman. Petri Net Transformations for Business Processes -- A Survey. Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems, 2: 46-63, March 2009.
Abstract: 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. @article{LohmannVD_2008_topnoc, Author = {Niels Lohmann and Eric Verbeek and Remco Dijkman}, Journal = {Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems}, Title = {{Petri} Net Transformations for Business Processes -- A Survey}, Year = {2009}, Editor = {Kurt Jensen and Wil M. P. van der Aalst}, Volume = {2}, series = {Lecture Notes in Computer Science, vol. 5460}, Pages = {46-63}, Month = mar, Publisher = {Springer-Verlag}, url = {http://dx.doi.org/10.1007/978-3-642-00899-3_3}, Abstract = {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.} }Niels Lohmann, Eric Verbeek, Chun Ouyang, and Christian Stahl. Comparing and Evaluating Petri Net Semantics for BPEL. International Journal of Business Process Integration and Management (IJBPIM), 4(1): 60-73, 2009.
Abstract: 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. @article{LohmannVOS_2009_ijbpim, Author = {Niels Lohmann and Eric Verbeek and Chun Ouyang and Christian Stahl}, Journal = {International Journal of Business Process Integration and Management (IJBPIM)}, Title = {Comparing and Evaluating {Petri} Net Semantics for {BPEL}}, Year = {2009}, volume = {4}, number = {1}, pages = {60-73}, Keywords = {Tools4BPEL, BPEL, BPEL-Semantik}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/LohmannVOS2008_ijbpim.pdf}, url = {http://dx.doi.org/10.1504/IJBPIM.2009.026986}, Abstract = {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.} }Christian Stahl, Peter Massuthe, and Jan Bretschneider. Deciding Substitutability of Services with Operating Guidelines. Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems, 2(5460): 172-191, March 2009.
Abstract: 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. @article{StahlMB_2008_topnoc, Author = {Christian Stahl and Peter Massuthe and Jan Bretschneider}, Journal = {Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems}, Title = {{Deciding Substitutability of Services with Operating Guidelines}}, Year = {2009}, Editor = {Kurt Jensen and Wil M. P. van der Aalst}, Volume = {2}, Number = {5460}, Pages = {172-191}, Month = mar, Publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science, vol. 5460}, isbn = {978-3-642-00898-6}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/StahlMB2008_topnoc.pdf}, url = {http://dx.doi.org/10.1007/978-3-642-00899-3_10}, Keywords = {Exchangeability, Services, SOA, Bedienungsanleitung, Serviceautomat}, Abstract = {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.} }Christian Stahl and Karsten Wolf. Deciding Service Composition and Substitutability Using Extended Operating Guidelines. Data Knowl. Eng., 68(9): 819-833, 2009.
Abstract: 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? @Article{StahlW2009_dke, author = {Christian Stahl and Karsten Wolf}, title = {Deciding Service Composition and Substitutability Using Extended Operating Guidelines}, journal = {Data Knowl. Eng.}, year = 2009, volume = {68}, number = {9}, pages = {819-833}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/StahlW2008_dke.pdf}, url = {http://dx.doi.org/10.1016/j.datak.2009.02.012}, keywords = {offene Workflownetze, Services, Bedienungsanleitung, Exchangeability, Matching}, abstract = {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?} }Kees van Hee, Eric Verbeek, Christian Stahl, and Natalia Sidorova. A Framework for Linking and Pricing No-Cure-No-Pay Services. Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems, 2: 192-207, March 2009.
Abstract: 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. @article{HeeVSS_2008_topnoc, Author = {Kees van Hee and Eric Verbeek and Christian Stahl and Natalia Sidorova}, Journal = {Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems}, Title = {{A Framework for Linking and Pricing No-Cure-No-Pay Services}}, Year = {2009}, Editor = {Kurt Jensen and Wil M. P. van der Aalst}, Volume = {2}, series = {Lecture Notes in Computer Science, vol. 5460}, Pages = {192-207}, Month = mar, Publisher = {Springer-Verlag}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/HeeVSS2008_topnoc.pdf}, url = {http://dx.doi.org/10.1007/978-3-642-00899-3_11}, Keywords = {Architecture Framework, SOA}, Abstract = {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.} }
Workshop and Conference Papers
Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution. In SAT, pages 114-127, 2009.
@inproceedings{DBLP:conf/sat/AtseriasFT09, author = {Albert Atserias and Johannes Klaus Fichte and Marc Thurley}, title = {Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution}, booktitle = {SAT}, year = {2009}, pages = {114-127}, ee = {http://dx.doi.org/10.1007/978-3-642-02777-2_13} }Dirk Fahland. A scenario is a behavioral view - Orchestrating services by scenario integration. In Oliver Kopp and Niels Lohmann, editors, Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, pages 8-14, March 2009. CEUR-WS.org.
Abstract: 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 specified and combined. We suggest to specify a service orchestration in terms of behavioral scenarios that capture a specific 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. @inproceedings{Fahland_2009_zeus, Author = {Dirk Fahland}, Booktitle = {Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009}, Editor = {Oliver Kopp and Niels Lohmann}, Month = mar, Pages = {8-14}, Pdf = {http://ceur-ws.org/Vol-438/paper2.pdf}, Publisher = {CEUR-WS.org}, Series = {CEUR Workshop Proceedings}, Title = {A scenario is a behavioral view - Orchestrating services by scenario integration}, Volume = {438}, Year = {2009}, Abstract = {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 specified and combined. We suggest to specify a service orchestration in terms of behavioral scenarios that capture a specific 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.}, Keywords = {Services, Szenario-Basierte Modelle, Petrinetze} }Dirk Fahland. Oclets - scenario-based modeling with Petri nets. In Giuliana Franceschinis and Karsten Wolf, editors, 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, Paris, France, pages 223-242, June 2009. Springer-Verlag. Note: (revised version).
Abstract: 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. @InProceedings{Fahland2009_oclets, address = {Paris, France}, author = {Dirk Fahland}, booktitle = {Proceedings of the 30th International Conference on Petri Nets and Other Models Of Concurrency, 22-26 May 2009}, editor = {Giuliana Franceschinis and Karsten Wolf}, month = jun, pages = {223-242}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/fahland09_petrinets_rev.pdf}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, title = {Oclets - scenario-based modeling with {Petri} nets}, volume = {5606}, year = {2009}, keywords = {Adaptive/Flexible Workflows, Szenario-basierte Modelle, Petrinetze}, abstract = {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.}, note = {(revised version)} }Dirk Fahland, Cédric Favre, Barbara Jobstmann, Jana Koehler, Niels Lohmann, Hagen Völzer, and Karsten Wolf. Instantaneous Soundness Checking of Industrial Business Process Models. In Umeshwar Dayal, Johann Eder, Jana Koehler, and Hajo Reijers, editors, Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings, volume 5701 of Lecture Notes in Computer Science, September 2009. Springer-Verlag.
@InProceedings{FahlandWJKLVW_2009_bpm, Author = {Dirk Fahland and C{\'e}dric Favre and Barbara Jobstmann and Jana Koehler and Niels Lohmann and Hagen V{\"o}lzer and Karsten Wolf}, Booktitle = {Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings}, Editor = {Umeshwar Dayal and Johann Eder and Jana Koehler and Hajo Reijers}, Month = sep, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {Instantaneous Soundness Checking of Industrial Business Process Models}, Volume = {5701}, Year = {2009}, keywords = {Geschäftsprozesse, Petrinetze, Soundness} }Dirk Fahland, Daniel Lübke, Jan Mendling, Hajo Reijers, Barbara Weber, Matthias Weidlich, and Stefan Zugal. Declarative versus Imperative Process Modeling Languages: The Issue of Understandability. In John Krogstie, Terry Halpin, and Erik Proper, editors, 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, Amsterdam, The Netherlands, pages 353-366, June 2009. Springer-Verlag.
Abstract: 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. @InProceedings{FahlandLMRWWZ2009_emmsad, address = {Amsterdam, The Netherlands}, author = {Dirk Fahland and Daniel L\"{u}bke and Jan Mendling and Hajo Reijers and Barbara Weber and Matthias Weidlich and Stefan Zugal}, booktitle = {Proceedings of the 14th International Conference on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD'09)}, editor = {John Krogstie and Terry Halpin and Erik Proper}, month = jun, pages = {353-366}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/fahlandlmrwwz_2009_emmsad.pdf}, publisher = {Springer-Verlag}, series = {Lecture Notes in Business Information Processing}, volume = {29}, title = {{Declarative versus Imperative Process Modeling Languages: The Issue of Understandability}}, year = {2009}, keywords = {Geschäftsprozesse, Adaptive/Flexible Workflows, BPEL, Deklarative Modelle, Petrinetze, Szenario-basierte Modelle, Temporale Logik}, abstract = {Advantages and shortcomings of different process modeling languages are heavily debated, both in academia and industry, but little evidence is presented to support judgements. With this paper we aim to contribute to a more rigorous, theoretical discussion of the topic by drawing a link to well-established research on program comprehension. In particular, we focus on imperative and declarative techniques of modeling a process. Cognitive research has demonstrated that imperative programs deliver sequential information much better while declarative programs offer clear insight into circumstantial information. In this paper we show that in principle this argument can be transferred to respective features of process modeling languages. Our contribution is a pair of propositions that are routed in the cognitive dimensions framework. In future research, we aim to challenge these propositions by an experiment.} }Dirk Fahland, Jan Mendling, Hajo Reijers, Barbara Weber, Matthias Weidlich, and Stefan Zugal. Declarative vs. Imperative Process Modeling Languages: The Issue of Maintainability. In Stefanie Rinderle-Ma, Shazia Wasim Sadiq, and Frank Leymann, editors, Business Process Management Workshops, BPM 2009 International Workshops, Ulm, Germany, September 7, 2009. Revised Papers, volume 43 of Lecture Notes in Business Information Processing, Ulm, Germany, pages 477-488, September 2009. Springer.
Abstract: 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. @InProceedings{FahlandMRWWZ2009_erbpm, address = {Ulm, Germany}, author = {Dirk Fahland and Jan Mendling and Hajo Reijers and Barbara Weber and Matthias Weidlich and Stefan Zugal}, booktitle = {Business Process Management Workshops, BPM 2009 International Workshops, Ulm, Germany, September 7, 2009. Revised Papers}, editor = {Stefanie Rinderle-Ma and Shazia Wasim Sadiq and Frank Leymann}, month = sep, pages = {477-488}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/FahlandMRWWZ2009_erbpm_workshop.pdf}, publisher = {Springer}, series = {Lecture Notes in Business Information Processing}, title = {{Declarative vs. Imperative Process Modeling Languages: The Issue of Maintainability}}, volume = {43}, year = {2009}, keywords = {Geschäftsprozesse, Adaptive/Flexible Workflows, Deklarative Modelle, Petrinetze}, abstract = {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.} }Nannette Liske, Niels Lohmann, Christian Stahl, and Karsten Wolf. Another Approach to Service Instance Migration. In Luciano Baresi, Chi-Hung Chi, and Jun Suzuki, editors, Service-Oriented Computing - ICSOC 2009, 7th International Conference, Stockholm, Sweden, November 24-27, 2009. Proceedings, Lecture Notes in Computer Science, pages 607-621, November 2009. Springer-Verlag.
Abstract: 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. @inproceedings{LiskeLSW_2009_icsoc, Author = {Nannette Liske and Niels Lohmann and Christian Stahl and Karsten Wolf}, Booktitle = {Service-Oriented Computing - ICSOC 2009, 7th International Conference, Stockholm, Sweden, November 24-27, 2009. Proceedings}, Editor = {Luciano Baresi and Chi-Hung Chi and Jun Suzuki}, Month = nov, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {Another Approach to Service Instance Migration}, Year = {2009}, pages = {607-621}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/LiskeLSW2009_icsoc.pdf}, url = {http://dx.doi.org/10.1007/978-3-642-10383-4_44}, keywords = {Serviceautomat, Services, Bedienungsanleitung, Exchangeability}, Abstract = {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. } }Jarungjit Parnji, Christian Stahl, and Karsten Wolf. A finite representation of all substitutable services and its applications. In Oliver Kopp and Niels Lohmann, editors, Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, pages 8-14, March 2009. CEUR-WS.org.
Abstract: 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 \mathcal{P} = {P1, ..., Pn}, we provide a representation of all services P' that can substitute every Pi \in \mathcal{P}, 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. @inproceedings{ParnjaiSW_2009_zeus, Author = {Jarungjit Parnji and Christian Stahl and Karsten Wolf}, Booktitle = {Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009}, Editor = {Oliver Kopp and Niels Lohmann}, Month = mar, Pages = {8-14}, Pdf = {http://ceur-ws.org/Vol-438/paper5.pdf}, Publisher = {CEUR-WS.org}, Series = {CEUR Workshop Proceedings}, Title = {A finite representation of all substitutable services and its applications}, Volume = {438}, Year = {2009}, Abstract = {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 \mathcal{P} = {P1, ..., Pn}, we provide a representation of all services P' that can substitute every Pi \in \mathcal{P}, 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.}, Keywords = {Services, Exchangeability, Serviceautomat, Operating Guidelines} }Wolfgang Reisig. Simple Composition of Nets. In Giuliana Franceschinis and Karsten Wolf, editors, Proceedings of the 30th International Conference on Petri Nets and Other Models Of Concurrency, volume 5606 of Lecture Notes in Computer Science, Paris, France, pages 23-42, June 2009. Springer-Verlag.
@inproceedings{Reisig2009_SCoN, Author = {Wolfgang Reisig}, Booktitle = {Proceedings of the 30th International Conference on Petri Nets and Other Models Of Concurrency}, Editor = {Giuliana Franceschinis and Karsten Wolf}, Month = jun, Pages = {23-42}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {Simple Composition of Nets}, Volume = {5606}, Year = {2009}, Address = {Paris, France} }Jan Sürmeli. Profiling Services with Static Analysis. In AWPN, volume 501 of CEUR Workshop Proceedings, pages 35-40, 2009. CEUR-WS.org.
@inproceedings{Suermeli_2009_awpn, Author = {Jan S\"urmeli}, Booktitle = {AWPN}, Pages = {35-40}, Publisher = {CEUR-WS.org}, Series = {CEUR Workshop Proceedings}, Title = {Profiling Services with Static Analysis}, Volume = {501}, Year = {2009}, pdf = {http://ceur-ws.org/Vol-501/Paper5.pdf} }Jan Sürmeli and Daniela Weinberg. Creating Message Profiles of Open Nets. In Oliver Kopp and Niels Lohmann, editors, 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, pages 74-80, 2009. CEUR-WS.org.
@inproceedings{SuermeliW_2009_zeus, Author = {Jan S{\"u}rmeli and Daniela Weinberg}, Booktitle = {Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009}, Editor = {Oliver Kopp and Niels Lohmann}, Pages = {74-80}, Publisher = {CEUR-WS.org}, Series = {CEUR Workshop Proceedings}, Title = {Creating Message Profiles of Open Nets}, Url = {http://CEUR-WS.org/Vol-438/paper12.pdf}, Volume = {438}, Year = {2009} }Karsten Wolf, Christian Stahl, Janine Ott, and Robert Danitz. Verifying Livelock Freedom in an SOA Scenario. In Stephen Edwards and Walter Vogler, editors, Proceedings of the Ninth International Conference on Application of Concurrency to System Design (ACSD'09), Augsburg, Germany, pages 168-177, July 2009. IEEE Computer Society.
Abstract: 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. @inproceedings{WolfSDO_2009_acsd, author = {Karsten Wolf and Christian Stahl and Janine Ott and Robert Danitz}, title = {Verifying Livelock Freedom in an SOA Scenario}, editor = {Stephen Edwards and Walter Vogler}, booktitle = {Proceedings of the Ninth International Conference on Application of Concurrency to System Design (ACSD'09)}, year = 2009, pages = {168-177}, address = {Augsburg, Germany}, month = jul, publisher = {IEEE Computer Society}, Pdf = {http://www2.informatik.hu-berlin.de/top/download/publications/WolfSOD2009-fragments.pdf}, keywords = {Operating Guidelines, Matching, SOA, Services}, url = {http://dx.doi.org/10.1109/ACSD.2009.16}, abstract = {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.} }Wil M. P. van der Aalst, Arjan J. Mooij, Christian Stahl, and Karsten Wolf. Service Interaction: Patterns, Formalization, and Analysis. In Marco Bernardo, Luca Padovani, and Gianluigi Zavattaro, editors, Formal Methods for Web Services (SFM 2009), volume 5569, pages 42--88, April 2009. Springer-Verlag.
Abstract: 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. @inproceedings{AalstMSW_2009_lncs, author = {Wil M. P. van der Aalst and Arjan J. Mooij and Christian Stahl and Karsten Wolf}, title = {Service Interaction: Patterns, Formalization, and Analysis}, editor = {Marco Bernardo and Luca Padovani and Gianluigi Zavattaro}, booktitle = {Formal Methods for Web Services (SFM 2009)}, year = 2009, pages = "42--88", month = apr, publisher = {Springer-Verlag}, volume = "5569", pdf = {http://www.informatik.hu-berlin.de/top/download/publications/AalstMSW-sfm2009.pdf}, url = {http://dx.doi.org/10.1007/978-3-642-01918-0}, keywords = {Operating Guidelines, Matching, SOA, Exchangeability, Open Workflow Nets}, abstract = {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.} }
Technical Reports
Wolfgang Reisig. The Universal Net Composition Operator. Forschungsbericht, Humboldt-Universität zu Berlin, January 2009.
Abstract: 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. @techreport{Reisig_2009_tr_unco, Author = {Wolfgang Reisig}, Institution = {Humboldt-Universit\"{a}t zu Berlin}, Month = jan, Pdf = {http://www2.informatik.hu-berlin.de/top/download/publications/Reisig2009_unco.pdf}, Title = {The Universal Net Composition Operator}, Type = {Forschungsbericht}, Year = {2009}, Abstract = {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.} }
Research Paper and Master Thesis
Mike Herzog. Modellierung kommunizierender Systeme. Studienarbeit, Humboldt-Universität zu Berlin, March 2009.
@MastersThesis{Herzog2009_sa, author = {Mike Herzog}, title = {{Modellierung kommunizierender Systeme}}, school = {Humboldt-Universit\"{a}t zu Berlin}, year = 2009, type = {Studienarbeit}, month = mar, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Herzog2009_sa.pdf} }Richard Müller. Strukturelle Reduktion von Verhaltensadaptern. Studienarbeit, Humboldt-Universität zu Berlin, December 2009.
@MastersThesis{Mueller2009_sa, author = {Richard M\"uller}, title = {{Strukturelle Reduktion von Verhaltensadaptern}}, school = {Humboldt-Universit\"{a}t zu Berlin}, year = 2009, type = {Studienarbeit}, month = dec, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Mueller2009_sa.pdf} }Robert Prüfer. Optimierung der Sweeplinemethode. Studienarbeit, Humboldt-Universität zu Berlin, March 2009.
@MastersThesis{Pruefer2009_sa, author = {Robert Pr\"ufer}, title = {{Optimierung der Sweeplinemethode}}, school = {Humboldt-Universit\"{a}t zu Berlin}, year = 2009, type = {Studienarbeit}, month = mar, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Pruefer2009_sa.pdf} }Jan Sürmeli. Strukturelle Analyse von Servicenetzen. Diplomarbeit, Humboldt-Universität zu Berlin, February 2009.
@MastersThesis{Suermeli2009_da, author = {Jan S{\"u}rmeli}, title = {{Strukturelle Analyse von Servicenetzen}}, school = {Humboldt-Universit\"{a}t zu Berlin}, year = 2009, type = {Diplomarbeit}, month = feb }
Theory of Programming | | XHTML 1.0 | Thu Mar 31 15:30:03 2011

