More Web Proxy on the site http://driver.im/

research-article

Quantifying the parallelism in BPMN processes using model checking

Authors:

Lina YeAuthors Info & Claims

CBSE '14: Proceedings of the 17th international ACM Sigsoft symposium on Component-based software engineering

Pages 159 - 168

https://doi.org/10.1145/2602458.2602473

Published: 27 June 2014 Publication History

Abstract

A business process is a set of structured, related activities that aims at fulfilling a specific organizational goal for a customer or market. An important metric when developing a business process is its degree of parallelism, i.e., the maximum number of tasks that are executable in parallel in that process. The degree of parallelism determines the peak demand on tasks, providing a valuable guide for the problem of resource allocation in business processes. In this paper, we investigate how to automatically measure the degree of parallelism for business processes, described using the BPMN standard notation. We first present a formal model for BPMN processes in terms of Labelled Transition Systems, which are obtained through process algebra encodings. We then propose an approach for automatically computing the degree of parallelism by using model checking techniques and dichotomic search. We implemented a tool for automating this check and we applied it successfully to more than one hundred BPMN processes.

References

[1]

M. Autili, P. Inverardi, and M. Tivoli. CHOREOS: Large Scale Choreographies for the Future Internet. In Proc. of CSMR-WCRE'14, pages 391--394. IEEE, 2014.

[2]

D. Champelovier, X. Clerc, H. Garavel, Y. Guerte, C. McKinty, V. Powazny, F. Lang, W. Serwe, and G. Smeding. Reference Manual of the LOTOS NT to LOTOS Translator, Version 5.4. INRIA/VASY, 2011.

[3]

N. Coste, H. Garavel, H. Hermanns, F. Lang, R. Mateescu, and W. Serwe. Ten Years of Performance Evaluation for Concurrent Systems using CADP. In Proc. of ISoLA'10, volume 6416 of LNCS, pages 128--142. Springer, 2010.

Digital Library

[4]

M. Dam. Model Checking Mobile Processes. Information and Computation, 129(1):35--51, 1996.

Digital Library

[5]

T.H. Davenport. Process Innovation: Reengineering Work Through Information Technology. Harvard Business School Press, 1993.

Digital Library

[6]

G. Decker and M. Weske. Interaction-centric Modeling of Process Choreographies. Information Systems, 36(2):292--312, 2011.

Digital Library

[7]

Bonita designer (online). Available: http://www.bonitasoft.com/.

[8]

R.M. Dijkman, M. Dumas, and C. Ouyang. Semantics and Analysis of Business Process Models in BPMN. Inf. Softw. Technol., 50(12):1281--1294, 2008.

Digital Library

[9]

J. Esparza. Reachability in Live and Safe Free-choice Petri Nets is NP-complete. Theoretical Computer Science, 198:211--224, 1998.

Digital Library

[10]

H. Garavel, F. Lang, R. Mateescu, and W. Serwe. CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. STTT, 2(15):89--107, 2013.

[11]

M. Güdemann, P. Poizat, G. Salaün, and A. Dumont. VerChor: A Framework for Verifying Choreographies. In Proc. of FASE'13, volume 7793 of LNCS, pages 226--230. Springer, 2013.

Digital Library

[12]

M. Güdemann, G. Salaün, and M. Ouederni. Counterexample Guided Synthesis of Monitors for Realizability Enforcement. In Proc. of ATVA'12, volume 7561 of LNCS, pages 238--253. Springer, 2012.

Digital Library

[13]

ISO/IEC. International Standard 19510, Information technology - Business Process Model and Notation. 2013.

[14]

C. Larman. Applying UML And Patterns: An Introduction To Object-Oriented Analysis And Design And Iterative Development. Prentice Hall, 2005.

Digital Library

[15]

K. Bisgaard Lassen and W. Van der Aalst. Complexity Metrics for Workflow Nets. Inf. Softw. Technol., 51(3):610--626, 2009.

Digital Library

[16]

R. Mateescu and M. Sighireanu. Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. Sci. Comput. Program., 46(3):255--281, 2003.

Digital Library

[17]

R. Mateescu and D. Thivolle. A Model Checking Language for Concurrent Value-Passing Systems. In Proc. of FM'08, volume 5014 of LNCS, pages 148--164. Springer, 2008.

Digital Library

[18]

E.W. Mayr. An Algorithm for the General Petri Net Reachability Problem. SIAM J. Comput., 13(3):441--460, 1984.

[19]

T. McCabe. A Complexity Measure. In IEEE Transactions on Software Engineering, volume 2, pages 308--320. IEEE, 1976.

Digital Library

[20]

OMG. Business Process Model and Notation (BPMN) - Version 2.0. January 2011.

[21]

OMG. BPMN 2.0 by Example. 2010.

[22]

P. Poizat and G. Salaün. Checking the Realizability of BPMN 2.0 Choreographies. In Proc. of SAC'12, pages 1927--1934. ACM Press, 2012.

Digital Library

[23]

I. Raedts, M. Petkovic, Y. S. Usenko, J. M. van der Werf, J. F. Groote, and L. Somers. Transformation of BPMN Models for Behaviour Analysis. In Proc. of MSVVEIS'07, pages 126--137, 2007.

[24]

T. J. Rolfe. Analytic Derivation of Comparisons in Binary Search. SIGNUM Newsletter, 32(4):15--19, 1997.

Digital Library

[25]

Y. Sun and J. Su. Computing Degree of Parallelism for BPMN Processes. In Proc. of ICSOC'11, volume 7084 of LNCS, pages 1--15. Springer, 2011.

Digital Library

[26]

W. M. P. van der Aalst and A. H. M. Ter Hofstede. YAWL: Yet Another Workflow Language. Information Systems, 30:245--275, 2003.

Digital Library

[27]

P.Y.H. Wong and J. Gibbons. A Process Semantics for BPMN. In Proc. of ICFEM'08, volume 5256 of LNCS, pages 355--374. Springer, 2008.

Digital Library

[28]

P.Y.H. Wong and J. Gibbons. Verifying Business Process Compatibility. In Proc. of QSIC'08, pages 126--131. IEEE, 2008.

Digital Library

Cited By

Falcone YSalaün GZuo A(2024)Probabilistic Runtime Enforcement of Executable BPMN ProcessesFundamental Approaches to Software Engineering10.1007/978-3-031-57259-3_3(56-76)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57259-3_3
Falcone YSalaün GZuo A(2022)Probabilistic Model Checking of BPMN Processes at RuntimeIntegrated Formal Methods10.1007/978-3-031-07727-2_11(191-208)Online publication date: 1-Jun-2022
https://doi.org/10.1007/978-3-031-07727-2_11
Durán FRocha CSalaün G(2019)A rewriting logic approach to resource allocation analysis in business process modelsScience of Computer Programming10.1016/j.scico.2019.102303(102303)Online publication date: Sep-2019
https://doi.org/10.1016/j.scico.2019.102303
Show More Cited By

Index Terms

Quantifying the parallelism in BPMN processes using model checking
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Model Checking UML Activity Diagrams in FDR
ICIS '09: Proceedings of the 2009 Eigth IEEE/ACIS International Conference on Computer and Information Science

The Unified Modeling Language (UML) is the de-facto industrial standard for modeling object-oriented software systems. UML Activity diagrams (ADs) can be used for software modeling and they have under gone significant changes with UML 2.0 specification, ...
Model Checking UML Statechart Diagrams Using JACK
HASE '99: The 4th IEEE International Symposium on High-Assurance Systems Engineering

Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modeling Language (UML). In this paper we present a branching time model-checking approach to the automatic verification of formal ...
Modelling and model checking suspendible business processes via statechart diagrams and CSP

When modelling object behaviour with UML statechart diagrams, the history mechanism can be useful for modelling the suspension of a ''normal'' business process upon certain ''abnormal'' events together with the subsequent resumption, as illustrated by ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CBSE '14: Proceedings of the 17th international ACM Sigsoft symposium on Component-based software engineering

June 2014

200 pages

ISBN:9781450325776

DOI:10.1145/2602458

General Chair:
Lionel Seinturier
Université Lille 1, France
,
Program Chairs:
Eduardo Almeida
Federal University of Bahia, Brazil
,
Jan Carlson
Mälardalen University, Sweden

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 June 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CompArch'14

Sponsor:

SIGSOFT

CompArch'14: Federated Events on Component-Based Software Engineering and Software Architecture

June 30 - July 4, 2014

Marcq-en-Bareul, France

Acceptance Rates

CBSE '14 Paper Acceptance Rate 21 of 62 submissions, 34%;

Overall Acceptance Rate 55 of 147 submissions, 37%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
169
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)0

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Falcone YSalaün GZuo A(2024)Probabilistic Runtime Enforcement of Executable BPMN ProcessesFundamental Approaches to Software Engineering10.1007/978-3-031-57259-3_3(56-76)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57259-3_3
Falcone YSalaün GZuo A(2022)Probabilistic Model Checking of BPMN Processes at RuntimeIntegrated Formal Methods10.1007/978-3-031-07727-2_11(191-208)Online publication date: 1-Jun-2022
https://doi.org/10.1007/978-3-031-07727-2_11
Durán FRocha CSalaün G(2019)A rewriting logic approach to resource allocation analysis in business process modelsScience of Computer Programming10.1016/j.scico.2019.102303(102303)Online publication date: Sep-2019
https://doi.org/10.1016/j.scico.2019.102303
Cortes-Cornax MKrishna AMos ASalaün GHaddad HWainwright RChbeir R(2018)Automated analysis of industrial workflow-based modelsProceedings of the 33rd Annual ACM Symposium on Applied Computing10.1145/3167132.3167142(120-127)Online publication date: 9-Apr-2018
https://dl.acm.org/doi/10.1145/3167132.3167142
Durán FRocha CSalaün G(2018)Symbolic Specification and Verification of Data-Aware BPMN Processes Using Rewriting Modulo SMTRewriting Logic and Its Applications10.1007/978-3-319-99840-4_5(76-97)Online publication date: 8-Sep-2018
https://doi.org/10.1007/978-3-319-99840-4_5
Durán FRocha CSalaün G(2018)Computing the Parallelism Degree of Timed BPMN ProcessesSoftware Technologies: Applications and Foundations10.1007/978-3-030-04771-9_24(320-335)Online publication date: 6-Dec-2018
https://doi.org/10.1007/978-3-030-04771-9_24
Afanasyev AVoit NKirillov S(2018)Timed Automaton RVT-Grammar for Workflow TranslatingAdvances in Computational Intelligence10.1007/978-3-030-04497-8_12(146-155)Online publication date: 22-Oct-2018
https://dl.acm.org/doi/10.1007/978-3-030-04497-8_12
Du YWang LLi X(2017)Analyzing Degree of Parallelism for Concurrent Timed Workflow Processes With Shared ResourcesIEEE Transactions on Engineering Management10.1109/TEM.2016.262172664:1(42-56)Online publication date: Feb-2017
https://doi.org/10.1109/TEM.2016.2621726
Afanasyev AVoit NTimofeeva OEpifanov V(2017)Analysis and Control of Hybrid Diagrammatical WorkflowsProceedings of the Second International Scientific Conference “Intelligent Information Technologies for Industry” (IITI’17)10.1007/978-3-319-68321-8_13(124-133)Online publication date: 30-Sep-2017
https://doi.org/10.1007/978-3-319-68321-8_13
Durán FSalaün G(2017)Verifying Timed BPMN Processes Using MaudeCoordination Models and Languages10.1007/978-3-319-59746-1_12(219-236)Online publication date: 27-May-2017
https://doi.org/10.1007/978-3-319-59746-1_12
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents