Conceptual framework for business processes compositional verification

OMG, Business Process Model and Notation (BPMN) – version 2.0, Object Management Group, Massachusetts, USA, 2011. P.Y. Wong, J. Gibbons, Formalisations and applications of BPMN, Science of Computer Programming In Press, Corrected Proof. doi:10.1016/j.scico.2009.09.010. W. Aalst, Business process management demystified: A tutorial on models, systems and standards for workflow management, in: Lectures on Concurrency and Petri Nets, Lecture Notes in Computer Science, Springer, Berlin/ Heidelberg. Combi, 2009, Controllability in temporal conceptual workflow schemata, Vol. 5701, 64 A. Rozinat, W. Aalst, Conformance testing: Measuring the fit and appropriateness of event logs and process models, in: Business Process Management Workshops, Lecture Notes in Computer Science, Springer Berlin/ Heidelberg. S. Ma, L. Zhang, J. He, Towards formalization and verification of unified business process model based on pi calculus, Proc. ACIS International Conference on Software Engineering Research, Management and Applications 1. Morimoto, 2008, A survey of formal verification for business process modeling, International Journal of Operations and Quantitative Management, 14, 237 Mendoza, 2009, Compositional Model-Checking Verification of Critical Systems, 213 Aalst, 2002, Workflow Management: Models, Methods, and Systems Dongen, 2004, Multi-phase process mining: Building instance graphs, Vol. 3288, 362 W. Aalst, H. Reijers, A. Weijters, B. Dongen, A.A. de Medeiros, M. Song, H. Verbeek, Business process mining: An industrial application, Information Systems 32 (5). Formal Systems (Europe) Ltd, Failures–Divergence Refinement – FDR2 User Manual, Formal Systems (Europe) Ltd, Oxford, 2005. Aalst, 2009, Challenges in business process analysis, Vol. 12, 27 OASIS, Web Services Business Process Execution Language Version 2.0, OASIS Open, Billerica, USA, 2007. URL http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.pdf. R. Dijkman, M. Dumas, C. Ouyang, Semantics and analysis of business process models in BPMN, Inf. Softw. Technol. 50 (12). Díaz, 2005 Žic, 1994, Time-constrained buffer specifications in CSP+T and Timed CSP, ACM Transaction on Programming Languages and Systems, 16, 1661, 10.1145/197320.197322 C. Duursma, U. Olle, Task model definition and task analysis process, Tech. rep., Vrije University, Brussels KADSII/M5/VUB/RR/004/2.0. (1994). H. Eshuis, Semantics and verification of UML activity diagrams for workflow modelling, Phd thesis, University of Twente, Enschede, The Netherlands (2002). Schneider, 2000 Roscoe, 1997 W. Yeung, S. Schneider, Design and verification of distributed recovery blocks with CSP, Form. Methods Syst. Des. 22 (3). J. Rüf, T. Kropf, Symbolic model checking for a discrete clocked temporal logic with intervals, in: Proceedings of the IFIP WG 10.5 International Conference on Correct Hardware Design and Verification Methods, 1997. Clarke, 2000, Model Checking González, 2011, BTransformer – a tool for BPMN to CSP+T transformation, Vol. 3, 363 L. Mendoza, M. Capel, Algorithm proposal to automata generation from CCTL formulas, Technical report, University of Granada (2008). L. Mendoza, A. Marius, M. Pérez, A. Grimán, Critical success factors for a customer relationship management strategy, Inf. Softw. Technol. 49 (8). L. Mendoza, M. Capel, Procedure proposal to automata generation from CSP+T process terms, Technical report, University of Granada (2009).