Formal analysis of BPMN via a translation into COWS

Davide Prandi1, Paola Quaglia2, and Nicola Zannone3

1 Dip. di Medicina Sperimentale e Clinica, Univ. Magna Graecia di Catanzaro, Italy
2 Dip. di Ing. e Scienza dell'Informazione, Univ. di Trento, Italy
3 Dep. of Computer Science, Univ. of Toronto, Canada

A translation of the Business Process Modeling Notation into the process calculus COWS is presented. The stochastic extension of COWS is then exploited to address quantitative reasoning about the behaviour of business processes. An example of such reasoning is shown by running the PRISM probabilistic model checker on a case study.