Automated analysis of industrial workflow-based models

ABSTRACT

Modelling and governance of business processes are important concerns in companies all over the world. By better understanding business processes, different optimizations are made possible, concretely resulting into potential efficiency gains, cost reductions and improvements in agility. The use of formal specification languages for the modelling of business processes paves the way for different kinds of automated analysis. Such analysis can be used to infer properties from the modelled processes that can be used to improve their design. In this paper, we particularly explore two important classes of verification, namely verification of behavioural properties using model checking techniques and data-based analysis using SAT solving. Those verifications are fully automated by using different tools such as the CADP verification toolbox and the Z3 solver. We illustrate our approach on a real-world case study.

References

1. D. Calvanese, M. Dumas, U. Laurson, F. Maria Maggi, M. Montali, and I. Teinemaa. 2016. Semantics and Analysis of DMN Decision Tables. In Proc. of BPM'16 (LNCS), Vol. 9850. Springer, 217--233.
2. L. De Moura and N. Bjørner. 2008. Z3: An Efficient SMT Solver. In Proc. of TACAS'08 (LNCS), Vol. 4963. Springer, 337--340.
3. L. De Moura and N. Bjørner. 2011. Satisfiability Modulo Theories: Introduction and Applications. Commun. ACM 54, 9 (2011), 69--77.
4. L. de Moura, B. Dutertre, and N. Shankar. 2007. A Tutorial on Satisfiability Modulo Theories. In Proc. of CAV'07 (LNCS), Vol. 4590. Springer, 20--36.
5. G. Decker and M. Weske. 2011. Interaction-centric Modeling of Process Choreographies. Information Systems 36, 2 (2011), 292--312.
6. R.M. Dijkman, M. Dumas, and C. Ouyang. 2008. Semantics and Analysis of Business Process Models in BPMN. Inf. Softw. Technol. 50, 12 (2008), 1281--1294.
7. F. Durán and G. Salaün. 2017. Verifying Timed BPMN Processes Using Maude. In Proc. of COORDINATION'17 (LNCS), Vol. 10319. Springer, 219--236.
8. M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. 1999. Patterns in Property Specifications for Finite-State Verification. In Proc. of ICSE'99. ACM, 411--420.
9. N. El-Saber and A. Boronat. 2014. BPMN Formalization and Verification using Maude. In Proc. of BM-FA'14. ACM, 1--8.
10. H. Garavel, F. Lang, R. Mateescu, and W. Serwe. 2013. CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. STTT 2, 15 (2013), 89--107.
11. M. Güdemann, P. Poizat, G. Salaün, and A. Dumont. 2013. VerChor: A Framework for Verifying Choreographies. In Proc. of FASE'13 (LNCS), Vol. 7793. Springer, 226--230.
12. M. Güdemann, P. Poizat, G. Salaün, and L Ye. 2016. VerChor: A Framework for the Design and Verification of Choreographies. IEEE Trans. Services Computing 9, 4 (2016), 647--660.
13. F. Kossak, C. Illibauer, V. Geist, J. Kubovy, C. Natschläger, T. Ziebermayr, T. Kopetzky, B. Freudenthaler, and K.-D. Schewe. 2014. A Rigorous Semantics for BPMN 2.0 Process Diagrams. Springer.
14. A. Krishna, P. Poizat, and G. Salaün. 2017. VBPMN: Automated Verification of BPMN Processes. In Proc. of IFM'17 (LNCS), Vol. 10510. Springer, 323--331.
15. S. Maoz, J. O. Ringert, and B. Rumpe. 2011. ADDiff: Semantic Differencing for Activity Diagrams. In Proc. of SIGSOFT/FSE'11. ACM, 179--189.
16. A. Martens. 2005. Analyzing Web Service Based Business Processes. In Proc. of FASE'05 (LNCS), Vol. 3442. Springer, 19--33.
17. R. Mateescu, G. Salaün, and L. Ye. 2014. Quantifying the Parallelism in BPMN Processes using Model Checking. In Proc. of CBSE'14. ACM, 159--168.
18. A. Mos and M. Cortes-Cornax. 2016. Business Matter Experts do Matter: A Model-Driven Approach for Domain Specific Process Design and Monitoring. In Proc. of BPM Forum'16 (LNBIP), Vol. 260. Springer, 210--226.
19. H. N. Nguyen, P. Poizat, and F. Zaïdi. 2012. A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies. In Proc. of ICSOC'12 (LNCS), Vol. 7636. Springer, 525--532.
20. P. Poizat and G. Salaün. 2012. Checking the Realizability of BPMN 2.0 Choreographies. In Proc. of SAC'12. ACM, 1927--1934.
21. P. Poizat, G. Salaün, and A. Krishna. 2016. Checking Business Process Evolution. In Proc. of FACS'16 (LNCS), Vol. 10231. Springer, 36--53.
22. I. Raedts, M. Petkovic, Y. S. Usenko, J. M. van der Werf, J. F. Groote, and L. Somers. 2007. Transformation of BPMN Models for Behaviour Analysis. In Proc. of MSVVEIS'07. 126--137.
23. M. Reichert and B. Weber. 2012. Enabling Flexibility in Process-Aware Information Systems - Challenges, Methods, Technologies. Springer.
24. M. Weidlich, R. M. Dijkman, and M. Weske. 2012. Behaviour Equivalence and Compatibility of Business Process Models with Complex Correspondences. Comput. J. 55, 11 (2012), 1398--1418.
25. P.Y.H. Wong and J. Gibbons. 2008. A Process Semantics for BPMN. In Proc. of ICFEM'08 (LNCS), Vol. 5256. Springer, 355--374.
26. P.Y.H. Wong and J. Gibbons. 2008. Verifying Business Process Compatibility. In Proc. of QSIC'08. IEEE, 126--131.

Index Terms

• Applied computing

  • Enterprise computing

    • Business process management

      • Business process modeling

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

• Theory of computation

  • Logic

    • Logic and verification