Publikationen des Jahres 2008
Bücher und Konferenzbände
Dirk Fahland, Daniel Sadilek, Markus Scheidgen, and Stephan Weissleder, editors. Proceedings of the Workshop on Domain-Specific Modeling Languages (DSML'08), Berlin, Germany, March 14, volume 324 of CEUR Workshop Proceedings, 2008. CEUR-WS.org.
@proceedings{FahlandSSW_2008_dsml, editor = {Dirk Fahland and Daniel Sadilek and Markus Scheidgen and Stephan Wei{\ss}leder}, title = {Proceedings of the Workshop on Domain-Specific Modeling Languages ({DSML}'08), Berlin, Germany, March 14}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, volume = {324}, year = {2008} }Thomas Kühne, Wolfgang Reisig, and Friedrich Steimann, editors. Modellierung 2008, 12.-14. März 2008, Berlin, Proceedings, volume P-127 of Lecture Notes in Informatics (LNI), March 2008. GI.
@proceedings{KuehneRS_2008_mod, Month = mar, Title = {Modellierung 2008, 12.-14. M{\"a}rz 2008, Berlin, Proceedings}, Editor = {Thomas K{\"u}hne and Wolfgang Reisig and Friedrich Steimann}, Publisher = {GI}, Series = {Lecture Notes in Informatics (LNI)}, Volume = {P-127}, Year = {2008}, Month = mar }
Publikationen in Zeitschriften und Büchern
Niels Lohmann, Peter Massuthe, Christian Stahl, and Daniela Weinberg. Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation. Data Knowl. Eng., 64(1):38-54, January 2008.
Abstract: 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 \emph{flexible model generation} which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain. @Article{LohmannMSW2008_dke, author = {Niels Lohmann and Peter Massuthe and Christian Stahl and Daniela Weinberg}, title = {Analyzing Interacting {WS-BPEL} Processes Using Flexible Model Generation}, journal = {Data Knowl. Eng.}, year = 2008, Month = jan, Number = {1}, Pages = {38-54}, Volume = {64}, keywords = {BPEL-Semantik, BPEL, Services, Operating Guidelines, Matching, Tools4BPEL}, url = {http://dx.doi.org/10.1016/j.datak.2007.06.006}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/LohmannMSW2008_dke.pdf}, abstract = {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 \emph{flexible model generation} which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.} }Niels Lohmann, Eric Verbeek, and Remco Dijkman. Petri Net Transformations for Business Processes -- A Survey. Transactions on Petri Nets and Other Models of Concurrency, 2008. Note: (Accepted for publication).
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}, Note = {(Accepted for publication)}, Title = {{Petri} Net Transformations for Business Processes -- A Survey}, Year = {2008}, 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. IJBPIM, 2008. Note: (Accepted for publication).
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{LohmannVOSA_2008_ijbpim, Author = {Niels Lohmann and Eric Verbeek and Chun Ouyang and Christian Stahl}, Journal = {IJBPIM}, Note = {(Accepted for publication)}, Title = {Comparing and Evaluating {Petri} Net Semantics for {BPEL}}, Year = {2008}, 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.} }Peter Massuthe, Alexander Serebrenik, Natalia Sidorova, and Karsten Wolf. Can I find a Partner? Undecidablity of Partner Existence for Open Nets. Information Processing Letters, 108(6):374--378, November 2008.
@article{MassutheSSW_2008_ipl, author = {Peter Massuthe and Alexander Serebrenik and Natalia Sidorova and Karsten Wolf}, title = {Can {I} find a Partner? {U}ndecidablity of Partner Existence for Open Nets}, journal = {Information Processing Letters}, volume = {108}, number = {6}, month = {Nov}, year = {2008}, pages = {374--378}, url = {http://dx.doi.org/10.1016/j.ipl.2008.07.006}, keywords = {oWFNs, Services, Bedienbarkeit} }Wolfgang Reisig. Abstract State Machines for the Classroom - The Basics. Logics of Specification Languages, pp 15-46, 2008.
Abstract: Abstract State Machines (henceforth referred to as just ASM) were introduced as \"a 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. @Article{Reisig2008_asmc, author = {Wolfgang Reisig}, title = {{Abstract State Machines for the Classroom - The Basics}}, year = {2008}, journal = {{Logics of Specification Languages}}, Pages = {15-46}, keywords = {ASM}, abstract = { Abstract State Machines (henceforth referred to as just ASM) were introduced as \"a 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. } }Wolfgang Reisig. The Scholten/Dijkstra Pebble Game Played Straightly, Distributely, Online and Reversed. Pillars of Computer Science, 2008.
Abstract: 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. @Article{Reisig2008_dpgpsdor, Author = {Wolfgang Reisig}, journal = {Pillars of Computer Science}, Publisher = {Springer-Verlag}, Title = {{The Scholten/Dijkstra Pebble Game Played Straightly, Distributely, Online and Reversed}}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Reisig2008_dpgpsdor.pdf}, Year = {2008}, Abstract = {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.} }Wolfgang Reisig. The computable kernel of Abstract State Machines. To appear in Theoretical Computer Science, 2008.
@Article{Reisig2008_tcs, author = {Wolfgang Reisig}, title = {{The computable kernel of Abstract State Machines}}, year = {2008}, journal = {{To appear in Theoretical Computer Science}}, keywords = {ASM} }Christian Stahl, Peter Massuthe, and Jan Bretschneider. Deciding Substitutability of Services with Operating Guidelines. Transactions on Petri Nets and Other Models of Concurrency, 2008. Note: (Accepted for publication).
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}, Note = {(Accepted for publication)}, Title = {{Deciding Substitutability of Services with Operating Guidelines}}, Year = {2008}, 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.} }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, 2008. Note: (Accepted for publication).
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}, Note = {(Accepted for publication)}, Title = {{A Framework for Linking and Pricing No-Cure-No-Pay Services}}, Year = {2008}, 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.} }Wil M. P. van der Aalst, Niels Lohmann, Peter Massuthe, Christian Stahl, and Karsten Wolf. Multiparty Contracts: Agreeing and Implementing Interorganizational Processes. The Computer Journal, 2008. Note: (Accepted for publication).
Abstract: 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. @article{AalstLMSW_2008_compj, Author = {Wil M. P. van der Aalst and Niels Lohmann and Peter Massuthe and Christian Stahl and Karsten Wolf}, Journal = {The Computer Journal}, Note = {(Accepted for publication)}, Title = {{Multiparty Contracts: Agreeing and Implementing Interorganizational Processes}}, Year = {2008}, Abstract = {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.} }
Konferenzbeiträge und Beiträge auf Workshops
Wil M. P. van der Aalst, Niels Lohmann, Peter Massuthe, Christian Stahl, and Karsten Wolf. From Public Views to Private Views -- Correctness-by-Design for Services. In Marlon Dumas and Reiko Heckel, editors, 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, pages 139-153, 2008. Springer-Verlag.
Abstract: 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. @inproceedings{AalstLMSW2007_wsfm, Author = {{Wil} {M.} {P.} {van} {der} Aalst and Niels Lohmann and Peter Massuthe and Christian Stahl and Karsten Wolf}, Booktitle = {Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings}, Editor = {Marlon Dumas and Reiko Heckel}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {From Public Views to Private Views -- Correctness-by-Design for Services}, Year = {2008}, Pages = {139-153}, Volume = {4937}, keywords = {oWFNs, Services, Operating Guidelines, Exchangeability, SOA}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/AalstLMSW2007_wsfm.pdf}, Abstract = {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.} }Dirk Fahland. Adaptive und Selbststabilisierende Workflows. In Malte Diehl, Henrik Lipskoch, Roland Meyer, and Christian Storm, editors, Proceedings des gemeinsamen Workshops der Graduiertenkollegs, Trustworthy Software Systems, Berlin, pages 55--56, 2008. Gito-Verlag.
@INPROCEEDINGS{Fahland_2008_adaptive, author = {Fahland, Dirk}, title = {{Adaptive und Selbststabilisierende Workflows}}, booktitle = {Proceedings des gemeinsamen Workshops der Graduiertenkollegs}, year = {2008}, editor = {Diehl, Malte and Lipskoch, Henrik and Meyer, Roland and Storm, Christian}, series = {Trustworthy Software Systems}, pages = {55--56}, address = {Berlin}, publisher = {Gito-Verlag}, keywords = {Adaptive/Flexible Workflows, Szenario-basierte Modelle, Petrinetze} }Dirk Fahland. Oclets -- Scenario-Based Modeling with Petri Nets. In Niels Lohmann and Karsten Wolf, editors, 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, pages 1-6, September 2008. CEUR-WS.org.
Abstract: 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. @inproceedings{Fahland_2008_awpn, Author = {Dirk Fahland}, Booktitle = {Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008}, Editor = {Niels Lohmann and Karsten Wolf}, Month = sep, Pages = {1-6}, Pdf = {http://CEUR-WS.org/Vol-380/paper01.pdf}, Publisher = {CEUR-WS.org}, Series = {CEUR Workshop Proceedings}, Title = {Oclets -- Scenario-Based Modeling with {Petri} Nets}, Volume = {380}, Year = {2008}, Keywords = {Adaptive/Flexible Workflows, Szenario-basierte Modelle, Petrinetze}, Abstract = {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.} }Dirk Fahland and Heiko Woith. Towards Process Models for Disaster Response. In A.t. Hofstede M. de Leoni, S. Dustdar, editor, Proceedings of the First International Workshop on Process Management for Highly Dynamic and Pervasive Scenarios (PM4HDPS), co-located with 6th International Conference on Business Process Management (BPM'08), Milan, Italy, September 2008. Note: Accepted, Springer publication to appear.
Abstract: 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. @INPROCEEDINGS{FahlandW_2008_Response, author = {Dirk Fahland and Heiko Woith}, title = {Towards Process Models for Disaster Response}, booktitle = {Proceedings of the First International Workshop on Process Management for Highly Dynamic and Pervasive Scenarios (PM4HDPS), co-located with 6th International Conference on Business Process Management (BPM'08)}, year = {2008}, editor = {M. de Leoni, S. Dustdar, A.t. Hofstede}, address = {Milan, Italy}, month = {September}, note = {Accepted, Springer publication to appear}, abstract = {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.}, pdf = {http://www.informatik.hu-berlin.de/~fahland/docs/fahlandW08_response.pdf}, keywords = {Adaptive/Flexible Workflows, Szenario-basierte Modelle, Petrinetze} }Christian Gierds. Finding Cost-Efficient Adapters. In Niels Lohmann and Karsten Wolf, editors, 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, pages 37-42, September 2008. CEUR-WS.org.
@inproceedings{Gierds_2008_awpn, Author = {Christian Gierds}, Booktitle = {Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008}, Editor = {Niels Lohmann and Karsten Wolf}, Month = sep, Pages = {37-42}, Pdf = {http://CEUR-WS.org/Vol-380/paper06.pdf}, Publisher = {CEUR-WS.org}, Series = {CEUR Workshop Proceedings}, Title = {Finding Cost-Efficient Adapters}, Volume = {380}, Year = {2008} }Dieter König, Niels Lohmann, Simon Moser, Christian Stahl, and Karsten Wolf. Extending the Compatibility Notion for Abstract WS-BPEL Processes. In Wei-Ying Ma, Andrew Tomkins, and Xiaodong Zhang, editors, Proceedings of the 17th International Conference on World Wide Web, WWW 2008, Beijing, China, April 21--25, 2008, pages 785-794, April 2008. ACM.
Abstract: 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. @inproceedings{KoenigLMSW_2008_www, Author = {Dieter K{\"o}nig and Niels Lohmann and Simon Moser and Christian Stahl and Karsten Wolf}, Booktitle = {Proceedings of the 17th International Conference on World Wide Web, WWW 2008, Beijing, China, April 21--25, 2008}, Editor = {Wei-Ying Ma and Andrew Tomkins and Xiaodong Zhang}, Month = apr, Organization = {ACM}, Pages = {785-794}, Title = {Extending the Compatibility Notion for Abstract {WS-BPEL} Processes}, Year = {2008}, keywords = {BPEL-Semantik, BPEL, Operating Guidelines, Exchangeability, Tools4BPEL}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/KoenigLMSW2008_www.pdf}, Abstract = {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.} }Niels Lohmann. A Feature-Complete Petri Net Semantics for WS-BPEL 2.0. In Marlon Dumas and Reiko Heckel, editors, 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, pages 77-91, 2008. Springer-Verlag.
Abstract: 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. @inproceedings{Lohmann2007_wsfm, Author = {Niels Lohmann}, Booktitle = {Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings}, Editor = {Marlon Dumas and Reiko Heckel}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {A Feature-Complete {P}etri Net Semantics for {WS-BPEL} 2.0}, Year = {2008}, Pages = {77-91}, Volume = {4937}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Lohmann2007_wsfm.pdf}, Abstract = {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.} }Niels Lohmann. Correcting Deadlocking Service Choreographies Using a Simulation-Based Graph Edit Distance. In Marlon Dumas and Manfred Reichert, editors, Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1--4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, pages 132-147, September 2008. Springer-Verlag.
Abstract: 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. @inproceedings{Lohmann_2008_bpm, Author = {Niels Lohmann}, Booktitle = {Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1--4, 2008, Proceedings}, Editor = {Marlon Dumas and Manfred Reichert}, Month = sep, Pages = {132-147}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {Correcting Deadlocking Service Choreographies Using a Simulation-Based Graph Edit Distance}, Volume = {5240}, Year = {2008}, Abstract = {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.} }Niels Lohmann. Decompositional Calculation of Operating Guidelines Using Free Choice Conflicts. In Niels Lohmann and Karsten Wolf, editors, 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, pages 63-68, September 2008. CEUR-WS.org.
@inproceedings{Lohmann_2008_awpn, Author = {Niels Lohmann}, Booktitle = {Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008}, Editor = {Niels Lohmann and Karsten Wolf}, Month = sep, Pages = {63-68}, Pdf = {http://CEUR-WS.org/Vol-380/paper10.pdf}, Publisher = {CEUR-WS.org}, Series = {CEUR Workshop Proceedings}, Title = {Decompositional Calculation of Operating Guidelines Using Free Choice Conflicts}, Volume = {380}, Year = {2008} }Niels Lohmann. Why does my service have no partners?. In Roberto Bruni and Karsten Wolf, editors, Web Services and Formal Methods, Fifth International Workshop, WS-FM 2008, Milan, Italy, September 4-5, 2008, Proceedings, Lecture Notes in Computer Science, September 2008. Springer-Verlag.
Abstract: 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. @inproceedings{Lohmann_2008_wsfm, Author = {Niels Lohmann}, Booktitle = {Web Services and Formal Methods, Fifth International Workshop, WS-FM 2008, Milan, Italy, September 4-5, 2008, Proceedings}, Editor = {Roberto Bruni and Karsten Wolf}, Month = sep, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {Why does my service have no partners?}, Year = {2008}, Abstract = {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.} }Niels Lohmann and Jens Kleine. Fully-automatic Translation of Open Workflow Net Models into Human-readable Abstract BPEL Processes. In Thomas Kühne, Wolfgang Reisig, and Friedrich Steimann, editors, Modellierung 2008, 12.-14. März 2008, Berlin, Proceedings, volume P-127 of Lecture Notes in Informatics (LNI), pages 57-72, March 2008. GI.
Abstract: 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. @inproceedings{LohmannK_2008_mod, Month = mar, Author = {Niels Lohmann and Jens Kleine}, Booktitle = {Modellierung 2008, 12.-14. M{\"a}rz 2008, Berlin, Proceedings}, Editor = {Thomas K{\"u}hne and Wolfgang Reisig and Friedrich Steimann}, Pages = {57-72}, Publisher = {GI}, Series = {Lecture Notes in Informatics (LNI)}, Volume = {P-127}, Title = {{Fully-automatic Translation of Open Workflow Net Models into Human-readable Abstract {BPEL} Processes}}, Year = {2008}, Abstract = {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.} }Niels Lohmann, Oliver Kopp, Frank Leymann, and Wolfgang Reisig. Analyzing BPEL4Chor: Verification and Participant Synthesis. In Marlon Dumas and Reiko Heckel, editors, 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, pages 46-60, 2008. Springer-Verlag.
Abstract: 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. @inproceedings{LohmannKLR2007_wsfm, Author = {Niels Lohmann and Oliver Kopp and Frank Leymann and Wolfgang Reisig}, Booktitle = {Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings}, Editor = {Marlon Dumas and Reiko Heckel}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {Analyzing {BPEL4Chor}: Verification and Participant Synthesis}, Year = {2008}, Pages = {46-60}, Volume = {4937}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/LohmannKLR2007_wsfm.pdf}, Abstract = {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.} }Peter Massuthe and Daniela Weinberg. Fiona: A Tool to Analyze Interacting Open Nets. In Niels Lohmann and Karsten Wolf, editors, 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, pages 99-104, September 2008. CEUR-WS.org.
@inproceedings{MassutheW_2008_awpn, Author = {Peter Massuthe and Daniela Weinberg}, Booktitle = {Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008}, Editor = {Niels Lohmann and Karsten Wolf}, Month = sep, Pages = {99-104}, Pdf = {http://CEUR-WS.org/Vol-380/paper16.pdf}, Publisher = {CEUR-WS.org}, Series = {CEUR Workshop Proceedings}, Title = {Fiona: A Tool to Analyze Interacting Open Nets}, Volume = {380}, Year = {2008} }Wolfgang Reisig. Towards a Theory of Services. In Invited paper for UNISCON 2008 in Klagenfurt, 2008. Springer-Verlag.
Abstract: 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. @inproceedings{Reisig2008_tts, Author = {Wolfgang Reisig}, Booktitle = {Invited paper for UNISCON 2008 in Klagenfurt}, Publisher = {Springer-Verlag}, Title = {{Towards a Theory of Services}}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Reisig2008_tts.pdf}, Year = {2008}, Abstract = {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.} }Chistian Stahl and Karsten Wolf. An Approach to Tackle Livelock-Freedom in SOA. In Niels Lohmann and Karsten Wolf, editors, 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, pages 69-74, September 2008. CEUR-WS.org.
@inproceedings{StahlW_2008_awpn, Author = {Chistian Stahl and Karsten Wolf}, Booktitle = {Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008}, Editor = {Niels Lohmann and Karsten Wolf}, Month = sep, Pages = {69-74}, Pdf = {http://CEUR-WS.org/Vol-380/paper11.pdf}, Publisher = {CEUR-WS.org}, Series = {CEUR Workshop Proceedings}, Title = {An Approach to Tackle Livelock-Freedom in {SOA}}, Volume = {380}, Year = {2008} }Christian Stahl and Karsten Wolf. Covering Places and Transitions in Open Nets. In Marlon Dumas and Manfred Reichert, editors, Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, pages 116-131, September 2008. Springer-Verlag.
Abstract: 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. @inproceedings{StahlW2008_bpm, Author = {Christian Stahl and Karsten Wolf}, Booktitle = {Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings}, Editor = {Marlon Dumas and Manfred Reichert}, Month = sep, Pages = {116-131}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {Covering Places and Transitions in Open Nets}, Year = {2008}, Volume = {5240}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/StahlW2008_bpm.pdf}, Abstract = {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.} }Daniela Weinberg. Efficient Controllability Analysis of Open Nets. In Roberto Bruni and Karsten Wolf, editors, Web Services and Formal Methods, Fifth International Workshop, WS-FM 2008, Milan, Italy, September 4--5, 2008, Proceedings, Lecture Notes in Computer Science, September 2008. Springer-Verlag.
Abstract: A service is designed to interact with other services. If the service interaction is stateful and asynchronous, the interaction protocol can become quite complex. A service may be able to interact with a lot of possible partner services, one partner or no partner at all. Having no partner surely is not intended by the designer. But the stateful interaction between services can be formalized and thus analyzed at design time. We present a formalization which is centered around a graph data structure that we call interaction graph, which represents feasible runs of a partner service according to the interaction protocol. As interaction graphs suffer from state explosion, we introduce a set of suitable reduction rules to alleviate the complexity of our approach. As our case studies show we are able to analyze the interaction behavior of a service efficiently. @inproceedings{Weinberg_2008_wsfm, Author = {Daniela Weinberg}, Booktitle = {Web Services and Formal Methods, Fifth International Workshop, WS-FM 2008, Milan, Italy, September 4--5, 2008, Proceedings}, Editor = {Roberto Bruni and Karsten Wolf}, Month = sep, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {Efficient Controllability Analysis of Open Nets}, Year = {2008}, Abstract = {A service is designed to interact with other services. If the service interaction is stateful and asynchronous, the interaction protocol can become quite complex. A service may be able to interact with a lot of possible partner services, one partner or no partner at all. Having no partner surely is not intended by the designer. But the stateful interaction between services can be formalized and thus analyzed at design time. We present a formalization which is centered around a graph data structure that we call interaction graph, which represents feasible runs of a partner service according to the interaction protocol. As interaction graphs suffer from state explosion, we introduce a set of suitable reduction rules to alleviate the complexity of our approach. As our case studies show we are able to analyze the interaction behavior of a service efficiently. } }
Technische Berichte
Dirk Fahland. Oclets - a formal approach to adaptive systems using scenario-based concepts. Informatik-Berichte 223, Humboldt-Universität zu Berlin, 2008.
Abstract: 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. @TECHREPORT{Fahland_2008_oclets, author = {Fahland, Dirk}, title = {Oclets - a formal approach to adaptive systems using scenario-based concepts}, institution = {Humboldt-Universit\"{a}t zu Berlin}, year = {2008}, type = {Informatik-Berichte}, number = {223}, pdf = {http://www.informatik.hu-berlin.de/~fahland/docs/fahland08_oclets_tr_223.pdf}, abstract = {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.}, keywords = {Adaptive/Flexible Workflows, Szenario-basierte Modelle, Petrinetze} }Dirk Fahland. Translating UML2 Activity Diagrams Petri Nets for analyzing IBM WebSphere Business Modeler process models. Informatik-Berichte 226, Humboldt-Universität zu Berlin, 2008.
Abstract: 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/. @TECHREPORT{Fahland_2008_uml, author = {Fahland, Dirk}, title = {Translating {UML2 Activity Diagrams} {Petri} Nets for analyzing {IBM WebSphere Business Modeler} process models}, institution = {Humboldt-Universit\"{a}t zu Berlin}, year = {2008}, type = {Informatik-Berichte}, number = {226}, pdf = {http://www.informatik.hu-berlin.de/~fahland/docs/fahland08_umlpn_tr_226.pdf}, abstract = {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/.}, keywords = {Geschäftsprozesse, Petrinetze, LoLA} }Christian Gierds, Arjan J. Mooij, and Karsten Wolf. Specifying and generating behavioral service adapter based on transformation rules. Preprint CS-02-08, Universität Rostock, Rostock, Germany, August 2008.
Abstract: 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. @techreport{GierdsMW_2008_tr_cs0208, Address = {Rostock, Germany}, Author = {Christian Gierds and Arjan J. Mooij and Karsten Wolf}, Institution = {Universit{\"a}t Rostock}, Month = aug, Number = {CS-02-08}, Pdf = {http://wwwteo.informatik.uni-rostock.de/ls_tpp/publications/GierdsMW_2008_tr_cs0208.pdf}, Title = {Specifying and generating behavioral service adapter based on transformation rules}, Type = {Preprint}, Year = {2008}, Abstract = {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.} }Peter Massuthe, Alexander Serebrenik, Natalia Sidorova, and Karsten Wolf. Can I find a Partner?. Preprint CS-01-08, Universität Rostock, Rostock, Germany, March 2008.
Abstract: 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. @techreport{MassutheSSW_2008_tr_cs0108, Address = {Rostock, Germany}, Author = {Peter Massuthe and Alexander Serebrenik and Natalia Sidorova and Karsten Wolf}, Institution = {Universität Rostock}, Month = mar, Number = {CS-01-08}, Title = {Can {I} find a Partner?}, Type = {Preprint}, Year = {2008}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/MassutheSSW_2008_tr_cs0108.pdf}, Abstract = {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.} }Christian Stahl, Peter Massuthe, and Jan Bretschneider. Deciding Substitutability of Services with Operating Guidelines. Informatik-Berichte 222, Humboldt-Universität zu Berlin, April 2008.
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 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. @TECHREPORT{StahlMB2008_hub_tr222, Author = {Christian Stahl and Peter Massuthe and Jan Bretschneider}, Institution = {Humboldt-Universit{\"a}t zu Berlin}, Number = {222}, Title = {{Deciding Substitutability of Services with Operating Guidelines}}, Type = {Informatik-Berichte}, Year = {2008}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/StahlMB2008-hub_tr222.pdf}, Month = apr, 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 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.}, keywords = {Exchangeability, Operating Guidelines, Open Workflow Nets, Services} }Kees M. van Hee, H.M.W. Verbeek, Christian Stahl, and Natalia Sidorova. A Framework for Linking and Pricing No-Cure-No-Pay Services. Computer Science Report 08/19, Technische Universiteit Eindhoven, Eindhoven, The Netherlands, June 2008.
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. @techreport{HeeVSS_2008_tr_cs-08-19, Address = {Eindhoven, The Netherlands}, Author = {Kees M. van Hee and H.M.W. Verbeek and Christian Stahl and Natalia Sidorova}, Institution = {Technische Universiteit Eindhoven}, Month = jun, Number = {08/19}, Title = {A Framework for Linking and Pricing No-Cure-No-Pay Services}, Type = {Computer Science Report}, Year = {2008}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/HeeVSS2008-csr_08_19.pdf}, 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.} }
Studien- und Diplomarbeiten
Christian Gierds. Strukturelle Reduktion von Bedienungsanleitungen. Diplomarbeit, Humboldt-Universität zu Berlin, January 2008.
Abstract: In dieser Arbeit werden wir uns mit Diamantenstrukturen in Bedienungsanleitungen beschäftigen. Im Rahmen der Service-Oriented Architecture beschreiben Bedienungsanleitungen Kommunikationspartner (Strategien) von Diensten. Ein großer Vorteil der Bedienungsanleitungen ist die endliche Repräsentation der gewöhnlich unendlich großen Menge aller Strategien eines Dienstes. Bedienungsanleitungen können nichtsdestotrotz sehr groß werden. Diamantenstrukturen sind eine der Hauptursachen dafür. Wir wollen eine Kurzschreibweise einführen, die das Eintreten von Ereignissen in jeder beliebigen Reihenfolge in einem Zustandsübergang beschreibt. Anschließend werden wir verschiedene Muster für Diamantenstrukturen vorstellen, also Muster mit Ereignissen, die in jeder beliebigen Reihenfolge stattfinden können. Für diese Muster werden wir Ersetzungen mit der eingeführten Kurzschreibweise angeben. Wir werden ferner Algorithmen angeben, welche die von uns definierten Diamantenmuster in Bedienungsanleitungen erkennen. @MastersThesis{Gierds2008_da, author = {Christian Gierds}, title = {{Strukturelle Reduktion von Bedienungsanleitungen}}, school = {Humboldt-Universität zu Berlin}, year = 2008, type = {Diplomarbeit}, month = jan, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Gierds2008_da.pdf}, keywords = {Serviceautomat, Bedienungsanleitung}, abstract={In dieser Arbeit werden wir uns mit Diamantenstrukturen in Bedienungsanleitungen beschäftigen. Im Rahmen der Service-Oriented Architecture beschreiben Bedienungsanleitungen Kommunikationspartner (Strategien) von Diensten. Ein großer Vorteil der Bedienungsanleitungen ist die endliche Repräsentation der gewöhnlich unendlich großen Menge aller Strategien eines Dienstes. Bedienungsanleitungen können nichtsdestotrotz sehr groß werden. Diamantenstrukturen sind eine der Hauptursachen dafür. Wir wollen eine Kurzschreibweise einführen, die das Eintreten von Ereignissen in jeder beliebigen Reihenfolge in einem Zustandsübergang beschreibt. Anschließend werden wir verschiedene Muster für Diamantenstrukturen vorstellen, also Muster mit Ereignissen, die in jeder beliebigen Reihenfolge stattfinden können. Für diese Muster werden wir Ersetzungen mit der eingeführten Kurzschreibweise angeben. Wir werden ferner Algorithmen angeben, welche die von uns definierten Diamantenmuster in Bedienungsanleitungen erkennen.} }Katharina Görlach. Ein Verfahren zur abstrakten Interpretation von XPath-Ausdrücken in WS-BPEL-Prozessen. Diplomarbeit, Humboldt-Universität zu Berlin, March 2008.
Abstract: Die Web Services Business Process Execution Language ist eine Sprache zur Modellierung von Geschäftsprozessen als Web Services. Für eine umfassende Analyse von WS-BPEL-Prozessen müssen auch die Daten der Prozesse analysiert werden. Daten werden in WS-BPEL-Prozessen mit Hilfe von XML-Schema typisiert und standardmäßig mit Hilfe von XPath manipuliert. Eine Datenanalyse für WS-BPEL muss deshalb XML-Schema berücksichtigen die im Prozess enthaltenen XPath-Ausdrücke auswerten. Eine solche Datenanalyse ermöglicht Rückschlüsse auf den Kontrollfluss und dient so beispielsweise zur Optimierung eines WS-BPEL-Prozesses. In der vorliegenden Arbeit wird ein Verfahren zur abstrakten Interpetation von XPath-Ausdrücken in WS-BPEL-Prozessen vorgestellt. Dafür wird ein umfassendes Datenmodell für WS-BPEL-Prozesse sowie die enthaltenen XPath-Ausdrücke entwickelt. Auf Grundlage des entwickelten Datenmodells stellen wir eine statische Analyse vor, die die XPath-Ausdrücke in einem WS-BPEL-Prozess abstrakt interpretiert. Die Analyse berechnet dabei die Wertebereiche für Variablen und Bedingungen in WS-BPEL-Prozessen. @MastersThesis{Goerlach2008_da, author = {Katharina Görlach}, title = {{Ein Verfahren zur abstrakten Interpretation von XPath-Ausdrücken in WS-BPEL-Prozessen}}, school = {Humboldt-Universität zu Berlin}, year = 2008, type = {Diplomarbeit}, month = mar, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Goerlach2008_da.pdf}, keywords = {BPEL}, abstract={Die Web Services Business Process Execution Language ist eine Sprache zur Modellierung von Geschäftsprozessen als Web Services. Für eine umfassende Analyse von WS-BPEL-Prozessen müssen auch die Daten der Prozesse analysiert werden. Daten werden in WS-BPEL-Prozessen mit Hilfe von XML-Schema typisiert und standardmäßig mit Hilfe von XPath manipuliert. Eine Datenanalyse für WS-BPEL muss deshalb XML-Schema berücksichtigen die im Prozess enthaltenen XPath-Ausdrücke auswerten. Eine solche Datenanalyse ermöglicht Rückschlüsse auf den Kontrollfluss und dient so beispielsweise zur Optimierung eines WS-BPEL-Prozesses. In der vorliegenden Arbeit wird ein Verfahren zur abstrakten Interpetation von XPath-Ausdrücken in WS-BPEL-Prozessen vorgestellt. Dafür wird ein umfassendes Datenmodell für WS-BPEL-Prozesse sowie die enthaltenen XPath-Ausdrücke entwickelt. Auf Grundlage des entwickelten Datenmodells stellen wir eine statische Analyse vor, die die XPath-Ausdrücke in einem WS-BPEL-Prozess abstrakt interpretiert. Die Analyse berechnet dabei die Wertebereiche für Variablen und Bedingungen in WS-BPEL-Prozessen.} }Daniel Janusz. Implementierung zweier Algorithmen zur Abstraktion von Petrinetzen. Studienarbeit, Humboldt-Universität zu Berlin, April 2008.
@MastersThesis{Janusz2008_sa, author = {Daniel Janusz}, title = {{Implementierung zweier Algorithmen zur Abstraktion von Petrinetzen}}, school = {Humboldt-Universität zu Berlin}, year = 2008, type = {Studienarbeit}, month = apr, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Janusz2008_sa.pdf} }Patrick Köhnen. Synthese offener Workflownetze aus Serviceautomaten. Diplomarbeit, Humboldt-Universität zu Berlin, January 2008.
Abstract: Das Paradigma der service-orientierten Architektur beschreibt eine Kapselung einzelner Funktionalitäten von Softwaresystemen in Services. Ein Service besitzt somit eine bestimmte Funktionalität und zudem eine definierte Schnittstelle. Über diese Schnittstelle kann die Funktionalität des Services genutzt werden. Durch diese Trennung von Funktionalität und Schnittstelle ist ein Service unabhängig von der Plattform und der verwendeten Programmiersprache. Änderungen und Erweiterungen service-basierter Softwaresysteme können durch Anpassungen oder das Austauschen des betreffenden Services erreicht werden und sind daher im Vergleich zu anderen Systemen einfacher, schneller und mit einem geringeren Risiko umsetzbar. Web Services sind eine spezielle und weit verbreitete Form von Services. Ein Web Service ist ein eigenständiges Softwaremodul, dessen Funktionalität über das Internet angeboten wird. Mit der Web Service Business Process Execution Language (WS-BPEL) kann ein Web Service definiert werden, der den Geschäftsprozess eines Unternehmens abbildet. WS-BPEL besitzt hierfür Konstrollstrukturen und Funktionalität zur Behandlung von Fehlern und Ausnahmen. WS-BPEL besitzt keine formale Semantik und kann daher nicht formal analysiert werden. Für eine formale Analyse kann ein WS-BPEL Prozess in ein offenes Workflownetz (oWFN) übersetzt werden. Existiert für ein oWFN ein Partner, der verklemmungsfrei mit diesem oWFN interagiert, kann ein Serviceautomat (SVA) berechnet werden, der das Verhalten dieses Partners beschreibt. Bisher war es möglich, ein oWFN nach WS-BPEL zu übersetzen, aber nicht, ein oWFN aus einem SVA zu synthetisieren. Ein berechneter Partner für einen WS-BPEL Prozess in Form eines SVAs konnte somit bisher nicht zurück in WS-BPEL übersetzt werden. Das Ziel dieser Arbeit ist es, die Synthese eines oWFNS aus einem SVA zu definieren und somit den Vorgang der Berechnung eines Partners für einen WS-BPEL Prozesss zu vervollständigen. @MastersThesis{Koehnen2008_da, author = {Patrick Köhnen}, title = {{Synthese offener Workflownetze aus Serviceautomaten}}, school = {Humboldt-Universität zu Berlin}, year = 2008, type = {Diplomarbeit}, month = jan, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Koehnen2008_da.pdf}, keywords = {oWFNs}, abstract={Das Paradigma der service-orientierten Architektur beschreibt eine Kapselung einzelner Funktionalitäten von Softwaresystemen in Services. Ein Service besitzt somit eine bestimmte Funktionalität und zudem eine definierte Schnittstelle. Über diese Schnittstelle kann die Funktionalität des Services genutzt werden. Durch diese Trennung von Funktionalität und Schnittstelle ist ein Service unabhängig von der Plattform und der verwendeten Programmiersprache. Änderungen und Erweiterungen service-basierter Softwaresysteme können durch Anpassungen oder das Austauschen des betreffenden Services erreicht werden und sind daher im Vergleich zu anderen Systemen einfacher, schneller und mit einem geringeren Risiko umsetzbar. Web Services sind eine spezielle und weit verbreitete Form von Services. Ein Web Service ist ein eigenständiges Softwaremodul, dessen Funktionalität über das Internet angeboten wird. Mit der Web Service Business Process Execution Language (WS-BPEL) kann ein Web Service definiert werden, der den Geschäftsprozess eines Unternehmens abbildet. WS-BPEL besitzt hierfür Konstrollstrukturen und Funktionalität zur Behandlung von Fehlern und Ausnahmen. WS-BPEL besitzt keine formale Semantik und kann daher nicht formal analysiert werden. Für eine formale Analyse kann ein WS-BPEL Prozess in ein offenes Workflownetz (oWFN) übersetzt werden. Existiert für ein oWFN ein Partner, der verklemmungsfrei mit diesem oWFN interagiert, kann ein Serviceautomat (SVA) berechnet werden, der das Verhalten dieses Partners beschreibt. Bisher war es möglich, ein oWFN nach WS-BPEL zu übersetzen, aber nicht, ein oWFN aus einem SVA zu synthetisieren. Ein berechneter Partner für einen WS-BPEL Prozess in Form eines SVAs konnte somit bisher nicht zurück in WS-BPEL übersetzt werden. Das Ziel dieser Arbeit ist es, die Synthese eines oWFNS aus einem SVA zu definieren und somit den Vorgang der Berechnung eines Partners für einen WS-BPEL Prozesss zu vervollständigen.} }Thomas Pillat. Gegenüberstellung struktureller Reduktionstechniken für Petrinetze. Diplomarbeit, Humboldt-Universität zu Berlin, March 2008.
Abstract: Petrinetze sind eine formale Methode zur Modellierung und Analyse von Systemen. Ein großes Problem bei der Analyse von Petrinetzen ist die Größe des Zustandsraums. Um dieses Problem abzuschwächen, können Reduktionstechniken eingesetzt werden. Petrinetze sind einer der wenigen Formalismen, die die Möglichkeit bieten, bereits die Struktur des Modells zu reduzieren. Diese strukturellen Reduktionstechniken verändern die Struktur des Netzes und bewahren dabei bestimmte Eigenschaften des ursprünglichen Modells. Es existieren eine Vielzahl wissenschaftlicher Arbeiten, die strukturelle Reduktionstechniken untersuchen. In der vorliegenden Arbeit werden strukturelle Reduktionstechniken einander gegenübergestellt und katalogisiert. Es wird ermittelt, welche Eigenschaften eines ursprünglichen Natzes durch die Anwendung der Reduktionstechnik bewahrt und für welche Netzklasse diese Reduktionstechnik gilt. Die Reduktionstechniken werden miteinander verglichen und die Beziehungen der Regeln zueinander ermittelt. Basierend auf diesen Ergebnissen wird ein Katalog erstellt, der beschreibt, für welche Netzklasse das Anwenden einer Regel welche Eigenschaften bewahrt. @MastersThesis{Pillat2008_da, author = {Thomas Pillat}, title = {{Gegen{\"u}berstellung struktureller Reduktionstechniken für Petrinetze}}, school = {Humboldt-Universität zu Berlin}, year = 2008, type = {Diplomarbeit}, month = mar, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Pillat2008_da.pdf}, keywords = {Petrinetze}, abstract={Petrinetze sind eine formale Methode zur Modellierung und Analyse von Systemen. Ein großes Problem bei der Analyse von Petrinetzen ist die Größe des Zustandsraums. Um dieses Problem abzuschwächen, können Reduktionstechniken eingesetzt werden. Petrinetze sind einer der wenigen Formalismen, die die Möglichkeit bieten, bereits die Struktur des Modells zu reduzieren. Diese strukturellen Reduktionstechniken verändern die Struktur des Netzes und bewahren dabei bestimmte Eigenschaften des ursprünglichen Modells. Es existieren eine Vielzahl wissenschaftlicher Arbeiten, die strukturelle Reduktionstechniken untersuchen. In der vorliegenden Arbeit werden strukturelle Reduktionstechniken einander gegenübergestellt und katalogisiert. Es wird ermittelt, welche Eigenschaften eines ursprünglichen Natzes durch die Anwendung der Reduktionstechnik bewahrt und für welche Netzklasse diese Reduktionstechnik gilt. Die Reduktionstechniken werden miteinander verglichen und die Beziehungen der Regeln zueinander ermittelt. Basierend auf diesen Ergebnissen wird ein Katalog erstellt, der beschreibt, für welche Netzklasse das Anwenden einer Regel welche Eigenschaften bewahrt.} }
Theorie der Programmierung | | XHTML 1.0 | Wed Nov 5 08:30:01 2008

