Work2010

Detecting deadlock and multiple termination in BPMN model using process automata

Nasi Tantitharanukul · Prompong Sugunnasil · Watcharee Jumpamule

10 citations0/0 files storedInternational Conference on Electrical Engineering/Electronics, Computer, Telecommunications and Information Technology (ECTI-CON)

No readable copy stored yet — this record is metadata only.

No open-access location is known for this record yet.

Literature note Cite in a project Citation map

Business Process Modeling and Analysis Formal Methods in Verification Model-Driven Software Engineering Techniques

Abstract

The Business Process Modeling Notation (BPMN) has been widely used as a tool for business process modeling. Despite of its popular, the BPMN does not contain a precise semantics. The incompatible constructs can cause the behavioral error such as deadlock. This paper proposed an automata-based formalism for verification of the single source BPMN model. We first introduce the transformation of the BPMN model to the process automata. Then, we verify the compatibility of the transition function. The BPMN model is considered to be correct if there exists at least one process sequence that is accepted by the process automata. Deadlock and multiple termination problems are chosen to illustrate our approach. The experimental results show that we can detect both problems (if any).

Paper brief

Loading…

Cite this work

Citation unavailable for this work.

BibTeX RIS CSL-JSON

No public copy is stored for this record, so only the metadata is cited.

Citations in this library

Citation map →

Stored only when both papers are in the corpus — 10 citations exist upstream.

References

2004Business Process Modeling Notation (BPMN), Version 1.0 2004Advances in business process management 2008The importance of business process modeling in software systems design 2007Verification of the SAP reference models using EPC reduction, state-space analysis, and invariants 2007Formal semantics and automated analysis of BPMN process models 2008Formal Semantics and Verification of BPMN Transaction and Compensation 2009A Simple Algorithm for Automatic Layout of BPMN Processes 2008Structural Detection of Deadlocks in Business Process Models

Cited by

2012Detecting structural errors in BPMN process models

Explore the map →

Papers that cite the same references — the relational fallback while embeddings are still backfilling.

Imported from OpenAlex (CC0) — nothing here is generated.