A Tool for Business Process Architecture Analysis
Business Process Architectures (BPA) are used for structuring and managing process collections. For optimising business processes a high level view on their interdependencies is necessary. BPAs allow to capture message and trigger flow relations between processes and their multiple process instances within a process collection. However, tools that allow analysis of BPAs besides visualization do not exist. This contribution presents a novel tool to model and to analyse the correctness of a BPA by transforming it into open nets, translate the correctness criteria into CTL formula and model check those using LoLA.
KeywordsModel Checker Correctness Criterion High Level View Modeling Guideline Renew Module
- 1.Mendling, J.: Metrics for Process Models: Empirical Foundations of Verification, Error Prediction, and Guidelines for Correctness. LNBIP, vol. 6. Springer, Heidelberg (2008)Google Scholar
- 2.Mendling, J., Reijers, H., van der Aalst, W.: Seven Process Modeling Guidelines (7PMG). Qut eprint. Queensland University of Technology (2008)Google Scholar
- 5.Hewelt, M., Wagner, T., Cabac, L.: Integrating verification into the PAOSE approach. In: Duvigneau, M., Moldt, D., Hiraishi, K. (eds.) Petri Nets and Software Engineering, PNSE 2011. CEUR Workshop Proceedings, vol. 723, pp. 124–135. CEUR-WS.org (2011)Google Scholar