Publications 2007

  • [PDF] [DOI] W. M. P. van der Aalst, B. Benatallah, F. Casati, F. Curbera, and H. M. W. Verbeek, “Business process management: where business processes and web services meet,” Data and knowledge engineering (dke), vol. 61, iss. 1, pp. 1-5, 2007.
    [Bibtex]
    @Article{Aalst07,
    Title = {Business process management: Where business processes and web services meet},
    Author = {Aalst, W. M. P. van der and Benatallah, B. and Casati, F. and Curbera, F. and Verbeek, H. M. W.},
    Journal = {Data and Knowledge Engineering (DKE)},
    Year = {2007},
    Note = {Editorial},
    Number = {1},
    Pages = {1--5},
    Volume = {61},
    Doi = {10.1016/j.datak.2006.04.005},
    File = {Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Aalst07.pdf:URL;Data and Knowledge Engineering:http\://www.sciencedirect.com/science/journal/0169023X:URL;Volume 61, issue 1:http\://www.sciencedirect.com/science/issue/5630-2007-999389998-645006:URL},
    Owner = {hverbeek},
    Timestamp = {2008.11.04}
    }
  • [PDF] [DOI] W. M. P. van der Aalst, B. F. van Dongen, C. W. GĂĽnther, R. S. Mans, A. A. K. de Medeiros, A. Rozinat, V. Rubin, M. Song, H. M. W. Verbeek, and A. J. M. M. Weijters, “Prom 4.0: comprehensive support for real process analysis,” in Application and theory of petri nets and other models of concurrency 2007, Siedlce, Poland, 2007, pp. 484-494.
    [Bibtex]
    @InProceedings{Aalst07a,
    Title = {ProM 4.0: Comprehensive Support for Real Process Analysis},
    Author = {Aalst, W. M. P. van der and Dongen, B. F. van and G\"{u}nther, C. W. and Mans, R. S. and Medeiros, A. K. Alves de and Rozinat, A. and Rubin, V. and Song, M. and Verbeek, H. M. W. and Weijters, A. J. M. M.},
    Booktitle = {Application and Theory of Petri nets and Other Models of Concurrency 2007},
    Year = {2007},
    Address = {Siedlce, Poland},
    Editor = {Kleijn, J. and Yakovlev, A.},
    Month = {June},
    Pages = {484--494},
    Publisher = {Springer, Berlin, Germany},
    Series = {Lecture Notes in computer Science},
    Volume = {4546},
    Abstract = {This tool paper describes the functionality of ProM. Version 4.0 of ProM has been released at the end of 2006 and this version reflects recent achievements in process mining. Process mining techniques attempt to extract non-trivial and useful information from so-called “event logs”. One element of process mining is control-flow discovery, i.e., automatically constructing a process model (e.g., a Petri net) describing the causal dependencies between activities. Control-flow discovery is an interesting and practically relevant challenge for Petri-net researchers and ProM provides an excellent platform for this. For example, the theory of regions, genetic algorithms, free-choice-net properties, etc. can be exploited to derive Petri nets based on example behavior. However, as we will show in this paper, the functionality of ProM 4.0 is not limited to control-flow discovery. ProM 4.0 also allows for the discovery of other perspectives (e.g., data and resources) and supports related techniques such as conformance checking, model extension, model transformation, verification, etc. This makes ProM a versatile tool for process analysis which is not restricted to model analysis but also includes log-based analysis.},
    Doi = {10.1007/978-3-540-73094-1_28},
    File = {Lecture Notes in Computer Science:http\://link.springer.de/link/service/series/0558/index.htm:URL;Volume 4546:http\://link.springer.de/link/service/series/0558/tocs/t4546.htm:URL;# 28th International Conference on the Application and Theory of Petri nets and Other Models of Concurrency:http\://atpn2007.ap.siedlce.pl/:URL;Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Aalst07a.pdf:PDF},
    Owner = {hverbeek},
    Timestamp = {2008.11.04},
    Url = {http://www.springerlink.com/content/732433l336669301/fulltext.pdf}
    }
  • [PDF] [DOI] W. M. P. van der Aalst, H. A. Reijers, A. J. M. M. Weijters, B. F. van Dongen, A. A. K. de Medeiros, M. Song, and H. M. W. Verbeek, “Business process mining: an industrial application,” Information systems (is), vol. 32, iss. 1, pp. 713-732, 2007.
    [Bibtex]
    @Article{Aalst07b,
    Title = {Business Process Mining: An Industrial Application},
    Author = {Aalst, W. M. P. van der and Reijers, H. A. and Weijters, A. J. M. M. and Dongen, B. F. van and Medeiros, A. K. Alves de and Song, M. and Verbeek, H. M. W.},
    Journal = {Information Systems (IS)},
    Year = {2007},
    Number = {1},
    Pages = {713--732},
    Volume = {32},
    Abstract = {Contemporary information systems (e.g., WfM, ERP, CRM, SCM, and B2B systems) record business events in so-called event logs. Business process mining takes these logs to discover process, control, data, organizational, and social structures. Although many researchers are developing new and more powerful process mining techniques and software vendors are incorporating these in their software, few of the more advanced process mining techniques have been tested on real-life processes. This paper describes the application of process mining in one of the provincial offices of the Dutch National Public Works Department, responsible for the construction and maintenance of the road and water infrastructure. Using a variety of process mining techniques, we analyzed the processing of invoices sent by the various subcontractors and suppliers from three different perspectives: (1) the process perspective, (2) the organizational perspective, and (3) the case perspective. For this purpose, we used some of the tools developed in the context of the ProM framework. The goal of this paper is to demonstrate the applicability of process mining in general and our algorithms and tools in particular.},
    Doi = {10.1016/j.is.2006.05.003},
    File = {Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Aalst07b.pdf:URL;Information Systems:http\://www.sciencedirect.com/science/journal/03064379:URL},
    Keywords = {Process mining; Social network analysis; Workflow management; Business process management; Business process analysis; Data mining; Petri nets},
    Owner = {hverbeek},
    Timestamp = {2008.11.04}
    }
  • [PDF] [DOI] B. F. van Dongen, M. H. Jansen-Vullers, H. M. W. Verbeek, and W. M. P. van der Aalst, “Verification of the sap reference models using epc reduction, state space analysis, and invariants,” Computers in industry (cii), vol. 58, iss. 6, pp. 578-601, 2007.
    [Bibtex]
    @Article{Dongen07,
    Title = {Verification of the SAP Reference Models using EPC Reduction, State Space Analysis, and Invariants},
    Author = {Dongen, B. F. van and Jansen-Vullers, M. H. and Verbeek, H. M. W. and Aalst, W. M. P. van der},
    Journal = {Computers in Industry (CiI)},
    Year = {2007},
    Number = {6},
    Pages = {578--601},
    Volume = {58},
    Abstract = {A reference model is a generic conceptual model that formalizes recommended practices for a certain domain. Today, the SAP reference models are among the most comprehensive reference models, including over 4000 entity types and covering over 1000 business processes and inter-organizational scenarios. The SAP reference models use Event-driven Process Chains (EPCs) to model these processes and scenarios. Like other informal languages, EPCs are intended to support the transition from a business model to an executable model. For this reason, researchers have tried to formalize the semantics of EPCs. However, in their approaches, they fail to acknowledge the fact that in EPCs constructs exist that require human judgment to assess correctness. This paper aims to acknowledge this fact by introducing a two-step approach. First, the EPC is reduced using universally accepted reduction rules. Second, the reduced EPC is analyzed using a mixture of state-space analysis, invariants, and human judgment. This approach has been implemented in a tool, and applying this tool to the SAP reference models showed that these contain errors, which clearly shows the added value of this verification approach.},
    Doi = {10.1016/j.compind.2007.01.001},
    File = {Computers in Industry:http\://www.sciencedirect.com/science/journal/01663615:URL;Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Dongen07.pdf:PDF},
    Owner = {hverbeek},
    Timestamp = {2008.11.04}
    }
  • [PDF] K. M. van Hee, N. Sidorova, C. Stahl, and H. M. W. Verbeek, “A price of service in a compositional soa framework,” Eindhoven University of Technology, Computer Science Report 07/16, 2007.
    [Bibtex]
    @TechReport{Hee07,
    Title = {A Price of Service in a Compositional SOA Framework},
    Author = {Hee, K. M. van and Sidorova, N. and Stahl, C. and Verbeek, H. M. W.},
    Institution = {Eindhoven University of Technology},
    Year = {2007},
    Number = {07/16},
    Type = {Computer Science Report},
    Abstract = {In this paper we propose a framework for SOA covering such important features as proper termination (soundness) and correct correlation of tasks. Within this framework, we define a method for the calculation of the price of services. Our framework is compositional in the sense that composing a system from subsystems that meet our correctness requirements we obtain a system that still meets these requirements.},
    File = {Computer Science Reports:http\://library.tue.nl/catalog/TUEPublication.csp?Type=ComputerScienceReports&Sort=Year:URL;Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Hee07.pdf:PDF},
    Owner = {hverbeek},
    Timestamp = {2008.11.04},
    Url = {http://alexandria.tue.nl/repository/books/631702.pdf}
    }
  • [PDF] N. Lohmann, H. M. W. Verbeek, C. Ouyang, C. Stahl, and W. M. P. van der Aalst, “Comparing and evaluating petri net semantics for bpel,” Eindhoven University of Technology, Computer Science Report 07/23, 2007.
    [Bibtex]
    @TechReport{Lohmann07,
    Title = {Comparing and Evaluating Petri Net Semantics for BPEL},
    Author = {Lohmann, N. and Verbeek, H. M. W. and Ouyang, C. and Stahl, C. and Aalst, W. M. P. van der},
    Institution = {Eindhoven University of Technology},
    Year = {2007},
    Number = {07/23},
    Type = {Computer Science Report},
    Abstract = {We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modeling decisions. These decisions together with their consequences are discussed.We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.},
    File = {Computer Science Reports:http\://library.tue.nl/catalog/TUEPublication.csp?Type=ComputerScienceReports&Sort=Year:URL;Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Lohmann07.pdf:PDF},
    Owner = {hverbeek},
    Timestamp = {2008.11.04},
    Url = {http://alexandria.tue.nl/repository/books/630637.pdf}
    }
  • [PDF] [DOI] C. Ouyang, H. M. W. Verbeek, W. M. P. van der Aalst, S. Breutel, M. Dumas, and A. H. M. ter Hofstede, “Formal semantics and analysis of control flow in ws-bpel,” Science of computer programming (scp), vol. 67, pp. 162-198, 2007.
    [Bibtex]
    @Article{Ouyang07,
    Title = {Formal Semantics and Analysis of Control Flow in WS-BPEL},
    Author = {Ouyang, C. and Verbeek, H. M. W. and Aalst, W. M. P. van der and Breutel, S. and Dumas, M. and Hofstede, A. H. M. ter},
    Journal = {Science of Computer Programming (SCP)},
    Year = {2007},
    Pages = {162--198},
    Volume = {67},
    Abstract = {Web service composition refers to the creation of new (Web) services by combining functionalities provided by existing ones. A number of domain-specific languages for service composition have been proposed, with consensus being formed around a process-oriented language known as WS-BPEL (or BPEL). The kernel of BPEL consists of simple communication primitives that may be combined using control-flow constructs expressing sequence, branching, parallelism, synchronization, etc. We present a comprehensive and rigorously defined mapping of BPEL constructs onto Petri net structures, and use this for the analysis of various dynamic properties related to unreachable activities, conflicting messages, garbage collection, conformance checking, and deadlocks and lifelocks in interaction processes. We use a mapping onto Petri nets because this allows us to use existing theoretical results and analysis tools. Unlike approaches based on finite state machines, we do not need to construct the state space, and can use structural analysis (e.g., transition invariants) instead. We have implemented a tool that translates BPEL processes into Petri nets and then applies Petri-net-based analysis techniques. This tool has been tested on different examples, and has been used to answer a variety of questions.},
    Doi = {10.1016/j.scico.2007.03.002},
    File = {Science of Computer Programming:http\://www.sciencedirect.com/science/journal/01676423:URL;Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Ouyang07.pdf:PDF},
    Owner = {hverbeek},
    Timestamp = {2008.11.04}
    }
  • [PDF] [DOI] H. M. W. Verbeek, W. M. P. van der Aalst, and A. H. M. ter Hofstede, “Verifying workflows with cancellation regions and or-joins: an approach based on relaxed soundness and invariants,” The computer journal (cj), vol. 50, iss. 3, pp. 294-314, 2007.
    [Bibtex]
    @Article{Verbeek07,
    Title = {Verifying Workflows with Cancellation Regions and OR-joins: An Approach Based on Relaxed Soundness and Invariants},
    Author = {Verbeek, H. M. W. and Aalst, W. M. P. van der and Hofstede, A. H. M. ter},
    Journal = {The Computer Journal (CJ)},
    Year = {2007},
    Number = {3},
    Pages = {294--314},
    Volume = {50},
    Abstract = {YAWL (Yet Another Workflow Language) workflow language supports the most frequent control-flow patterns found in the current workflow practice. As a result, most workflow languages can be mapped onto YAWL without the loss of control-flow details, even languages allowing for advanced constructs such as cancellation regions and OR-joins. Hence, a verification approach for YAWL is desirable, because such an approach could be used for any workflow language that can be mapped onto YAWL. Unfortunately, cancellation regions and OR-joins are ‘non-local’ properties, and in general we cannot even decide whether the desired final state is reachable if both patterns are present. This paper proposes a verification approach based on (i) an abstraction of the OR-join semantics; (ii) the relaxed soundness property; and (iii) transition invariants. This approach is correct (errors reported are really errors), but not necessarily complete (not every error might get reported). This incompleteness can be explained because, on the one hand, the approach abstracts from the OR-join semantics and on the other hand, it may use only transition invariants, which are structural properties. Nevertheless, our approach can be used to successfully detect errors in YAWL models. Moreover, the approach can be easily transferred to other workflow languages allowing for advanced constructs such as cancellations and OR-joins.},
    Doi = {10.1093/comjnl/bxl074},
    File = {The Computer Journal:http\://www3.oup.co.uk/computer_journal/:URL;Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Verbeek07.pdf:PDF},
    Owner = {hverbeek},
    Timestamp = {2008.11.04},
    Url = {http://comjnl.oxfordjournals.org/cgi/reprint/50/3/294}
    }
  • [PDF] H. M. W. Verbeek and B. F. van Dongen, “Translating labelled p/t nets into epcs for sake of communication,” Eindhoven University of Technology, BETA Working Paper 194, 2007.
    [Bibtex]
    @TechReport{Verbeek07a,
    Title = {Translating labelled P/T nets into EPCs for sake of communication},
    Author = {Verbeek, H. M. W. and Dongen, B. F. van},
    Institution = {Eindhoven University of Technology},
    Year = {2007},
    Month = {January},
    Number = {194},
    Type = {BETA Working Paper},
    Abstract = {Petri nets can be used to capture the behavior of a process in a formal and precise way. However, Petri nets are less suitable to communicate the process to its owner, as simple routing constructs in the process might require a large number of transitions. This paper introduces a translation from labelled P/T nets to EPCs in such a way that many transitions can be translated into one EPC connector. The algorithm even allows for translating a set of transitions into an OR connector, even though the concept of OR connectors (especially the OR join connector) has no real equal in Petri nets. Using this translation presented here, labelled P/T nets may be communicated to the process owner by means of the created EPC.},
    File = {BETA Working Paper Series:http\://www.tm.tue.nl/beta/publications/window.htm:URL;Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Verbeek07a.pdf:PDF},
    Owner = {hverbeek},
    Timestamp = {2008.11.04},
    Url = {http://beta.ieis.tue.nl/node/1226}
    }
  • [PDF] H. M. W. Verbeek, A. J. Pretorius, W. M. P. van der Aalst, and J. J. van Wijk, “On petri-net synthesis and attribute-based visualization,” in Proceedings of workshop on petri nets and software engineering (pnse’07), Siedlce, Poland, 2007, pp. 127-141.
    [Bibtex]
    @InProceedings{Verbeek07b,
    Title = {On Petri-net synthesis and attribute-based visualization},
    Author = {Verbeek, H. M. W. and Pretorius, A. J. and Aalst, W. M. P. van der and Wijk, J. J. van},
    Booktitle = {Proceedings of Workshop on Petri Nets and Software Engineering (PNSE'07)},
    Year = {2007},
    Address = {Siedlce, Poland},
    Editor = {Moldt, D. and Kordon, F. and Hee, K. M. van and Colom, J.-M. and Bastide, R.},
    Month = {June},
    Pages = {127--141},
    Publisher = {Publishing House of University of Podlasie, Siedlce, Poland},
    Abstract = {State space visualization is important for a good understanding of the system's behavior. Unfortunately, today's visualization tools typically ignore the fact that states might have attributes. Based on these attributes, some states can be considered equivalent after abstraction, and can thus be clustered, which simplifies the state space. Attribute-based visualization tools are the exception to this rule. These tools can deal with attributes. In this paper, we investigate an approach based on Petri nets. Places in a Petri net correspond in a straightforward way to attributes. Furthermore, we can use existing techniques to automatically derive a Petri net from some state space, that is, to automatically add attributes to that state space. As a result, we can use attribute-based visualization tools for any state space. Unfortunately, the approach is hampered by the fact that not every state space results in a usable Petri net.},
    File = {PNSE 07:http\://www.informatik.uni-hamburg.de/TGI/events/pnse07/:URL;Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Verbeek07b.pdf:PDF},
    Owner = {hverbeek},
    Timestamp = {2008.11.04},
    Url = {http://www.win.tue.nl/~hverbeek/downloads/preprints/Verbeek07b.pdf}
    }
  • [PDF] H. M. W. Verbeek, A. J. Pretorius, W. M. P. van der Aalst, and J. J. van Wijk, “Visualizing state spaces with petri nets,” Eindhoven University of Technology, Computer Science Report 07/01, 2007.
    [Bibtex]
    @TechReport{Verbeek07c,
    Title = {Visualizing State Spaces with Petri nets},
    Author = {Verbeek, H. M. W. and Pretorius, A. J. and Aalst, W. M. P. van der and Wijk, J. J. van},
    Institution = {Eindhoven University of Technology},
    Year = {2007},
    Number = {07/01},
    Type = {Computer Science Report},
    Abstract = {Many analysis techniques are based on state spaces, e.g., based on some system model or system log, state spaces are generated that can be used to verify behavioral properties (e.g., absence of deadlocks). State spaces can be inspected automatically without any human interpretation. However, for a good understanding of the system's behavior the analyst needs to inspect and interpret the corresponding state space. Therefore, state space visualization is important. Unfortunately, this aspect has been neglected and today's analysis tools typically represent states spaces in such a way that they are difficult to interpret and inspection is only possible for toy examples. Attribute-based visualization methods address this issue by enabling users to study state spaces in terms of data they understand: the attributes associated with every state. These techniques can deal with many types of attributes. In this paper we propose an approach based on Petri nets. Using existing synthesis techniques based on regions, we automatically derive a Petri net from a given state space. We consider the places of this Petri net as new derived state attributes. Using these, we combine attribute-based visualizations of the state space with diagrams of the associated Petri net. This approach has been implemented and provides an innovative and versatile way to visualize state spaces.},
    File = {Computer Science Reports:http\://library.tue.nl/catalog/TUEPublication.csp?Type=ComputerScienceReports&Sort=Year:URL;Preprint of published paper:http\://www.win.tue.nl/~hverbeek/downloads/preprints/Verbeek07c.pdf:PDF},
    Owner = {hverbeek},
    Timestamp = {2008.11.04},
    Url = {http://alexandria.tue.nl/extra1/wskrap/publichtml/200701.pdf}
    }

Leave a Reply