Semantics and analysis of business process models in BPMN
Information and Software TechnologyPublished 3 March 2008
Remco Dijkman, Marlon Dumas, Chun Ouyang
Citations584
SJR quartileQ1
SJR score1.04
SNIP2.15
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
This paper proposes a mapping from BPMN to a formal language, namely Petri nets, for which efficient analysis techniques are available and has been implemented as a tool that, in conjunction with existing Petri net-based tools, enables the static analysis of BPMn models.
Abstract
The Business Process Modelling Notation (BPMN) is a standard for capturing business processes in the early phases of systems development. The mix of constructs found in BPMN makes it possible to create models with semantic errors. Such errors are especially serious, because errors in the early phases of systems development are among the most costly and hardest to correct. The ability to statically check the semantic correctness of models is thus a desirable feature for modelling tools based on BPMN. Accordingly, this paper proposes a mapping from BPMN to a formal language, namely Petri nets, for which efficient analysis techniques are available. The proposed mapping has been implemented as a tool that, in conjunction with existing Petri net-based tools, enables the static analysis of BPMN models. The formalisation also led to the identification of deficiencies in the BPMN standard specification
Keywords
Computer ScienceBusiness, Management and Accounting
Distributed and Parallel DatabasesWorkflow Patterns
2,600 Citations2003Wil M. P. van der Aalst, Arthur H. M. ter Hofstede +2 more
A number of workflow patterns addressing what the authors believe identify comprehensive workflow functionality are described, providing the basis for an in-depth comparison of a number of commercially availablework flow management systems.
Information SystemsYAWL: yet another workflow language
1,340 Citations2004Wil M. P. van der Aalst, Arthur H. M. ter Hofstede
This paper motivates the need for a new workflow language, specifies the semantics of the language, and shows that soundness can be verified in a compositional way.
Lecture notes in computer scienceThe ProM Framework: A New Era in Process Mining Tool Support
919 Citations2005Boudewijn F. van Dongen, Ana Karla Alves de Medeiros +3 more
The ProM framework is introduced and an overview of the plug-ins that have been developed and is flexible with respect to the input and output format, and is also open enough to allow for the easy reuse of code during the implementation of new process mining ideas.
Information and Software TechnologyFormalization and verification of event-driven process chains
564 Citations1999Wil M. P. van der Aalst
This paper maps EPCs (without connectors of type ∨) onto Petri nets and shows that the correctness of an EPC can be checked in polynomial time by using Petri-net-based analysis techniques.
Lecture notes in computer scienceThe Petri Net Markup Language: Concepts, Technology, and Tools
341 Citations2003Jonathan Billington, Søren Christensen +7 more
The design principles, the basic concepts, and the underlying XML technology of PNML are discussed to stimulate discussion on and contributions to a standard Petri net interchange format.
Science of Computer ProgrammingFormal semantics and analysis of control flow in WS-BPEL
341 Citations2007Chun Ouyang, Eric Verbeek +4 more
A tool is described that performs two useful types of static checks and extracts meta-data to optimise dynamic resource management by translating BPEL processes into Petri nets and exploiting existing Petri net analysis techniques.
Lecture notes in computer scienceTransforming BPEL to Petri Nets
286 Citations2005Sebastian Hinz, Karsten Schmidt +1 more
A Petri net semantics for the Business Process Execution Language for Web Services (BPEL) that covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation).
Information SystemsVerification Of Workflow Task Structures: A Petri-net-baset Approach
267 Citations2000Wil M. P. van der Aalst, Arthur H. M. ter Hofstede
It is shown how verification of a typical process control specification, which is at the heart of most workflow specifications, can benefit from state-of-the-art Petri-net based analysis techniques.
Acta InformaticaFundamentals of control flow in workflows
210 Citations2003Bartek Kiepuszewski, Arthur H. M. ter Hofstede +1 more
The goal of this paper is to establish a formal foundation for control-flow aspects of workflow specification languages, that assists in understanding fundamental properties of such languages, in particular their expressive power.
Lecture notes in computer scienceApplications and Theory of Petri Nets 2005
198 Citations2005Gianfranco Ciardo, Philippe Darondeau +1 more
Particle Petri Nets for Aircraft Procedure Monitoring Under Uncertainty, and the Expressive Power of Petri Net Schemata.
Lecture notes in computer scienceA Process Semantics for BPMN
173 Citations2008Peter Y. H. Wong, Jeremy Gibbons
This paper shows how a subset of the BPMN can be given a process semantics in Communicating Sequential Processes, which allows developers to formally analyse and compare BPMn diagrams.
International Journal of Web Services ResearchPattern-Based Translation of BPMN Process Models to BPEL Web Services
154 Citations2008Chun Ouyang, Marlon Dumas +2 more
Methods for identifying not only perfectly block-structured fragments in BPMN models, but quasi-structuring fragments that can be turned into perfectly structured ones and flow-based acyclic fragments that are mapped onto a combination of structured constructs and control links are defined.
Lecture notes in computer scienceApplication and Theory of Petri Nets 1992
101 Citations1992Kathleen Jensen
Lecture notes in computer scienceInvestigations on Soundness Regarding Lazy Activities
72 Citations2006Frank Puhlmann, Mathias Weske
The π-calculus is utilized to discuss and implement reasoning on lazy soundness, a solution for proving the correctness of business processes containing discriminator, n-out-of-m-join or multiple instances without synchronization patterns that can leave running (lazy) activities behind.
Lecture notes in computer scienceAchieving a General, Formal and Decidable Approach to the OR-Join in Workflow Using Reset Nets
64 Citations2005Moe Thandar Wynn, David Edmond +2 more
The concept of OR-join is examined in detail in the context of the workflow language YAWL, a powerful workflow language designed to support a collection of workflow patterns and inspired by Petri nets.
Theoretical Computer ScienceAutomatic workflow verification and generation
39 Citations2005Shiyong Lu, Arthur Bernstein +1 more
A new workflow model based on Hoare semantics is proposed that allows to automatically check if the desired outcome of a workflow can be produced by its actual implementation, and automatically synthesize a workflow implementation from the workflow specification and a given task library.
TU/e Research Portal (Eindhoven University of Technology)Choreography-based design of business collaborations
8 Citations2006Remco Dijkman
Techniques to construct the choreography in a gradual manner, based on step-wise refinement, allowing a designer to focus on the most important problems of the choreographic first and then gradually introduce more detail are presented.