Abstract
This paper addresses the question how to verify that the local workflow of an organisation participating in a cross-organisational collaboration is in compliance with the globally specified rules of that collaboration. We assume that the collaborative workflow is specified as a BPMN Collaboration Diagram and the local workflows as BPMN Process Diagrams. We then employ existing LTL semantics of the former and token semantics of the latter to verify conformance. We use the graph transformation tool GROOVE to automate the verification, and exemplify our approach with a case study from the financial markets domain.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
van der Aalst, W.M.P., Weske, M.: The P2P approach to interorganizational workflows. In: Dittrich, K.R., Geppert, A., Norrie, M. (eds.) CAiSE 2001. LNCS, vol. 2068, pp. 140–156. Springer, Heidelberg (2001). doi:10.1007/3-540-45341-5_10
van der Aalst, W.M.P., Weske, M.: Reflections on a decade of interorganizational workflow research. In: Bubenko, J., Krogstie, J., Pastor, O., Pernici, B., Rolland, C., Sølvberg, A. (eds.) Seminal Contributions to Information Systems Engineering: 25 Years of CAiSE, pp. 307–313. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36926-1_24
Bandener, N., Soltenborn, C., Engels, G.: Extending DMM behavior specifications for visual execution and debugging. In: Malloy, B., Staab, S., van den Brand, M. (eds.) SLE 2010. LNCS, vol. 6563, pp. 357–376. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19440-5_24
Brambilla, M., Deutsch, A., Sui, L., Vianu, V.: The role of visual tools in a web application design and verification framework: a visual notation for LTL formulae. In: Lowe, D.G., Gaedke, M. (eds.) ICWE 2005. LNCS, vol. 3579, pp. 557–568. Springer, Heidelberg (2005). doi:10.1007/11531371_70
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001). http://books.google.de/books?id=Nmc4wEaLXFEC
Decker, G., Barros, A.: Interaction modeling using BPMN. In: ter Hofstede, A.H.M., Benatallah, B., Paik, H.-Y. (eds.) BPM Workshops 2007. LNCS, vol. 4928, pp. 208–219. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78238-4_22
Decker, G., Weske, M.: Local enforceability in interaction petri nets. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 305–319. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75183-0_22
ECB: Target2securities. https://www.ecb.europa.eu/paym/t2s, Mar 2015
Elgammal, A., Turetken, O., van den Heuvel, W.J., Papazoglou, M.: Formalizing and appling compliance patterns for business process compliance. Softw. Syst. Model., 1–28 (2014). http://dx.doi.org/10.1007/s10270-014-0395-3
Eshuis, R., Norta, A., Kopp, O., Pitkanen, E.: Service outsourcing with process views. IEEE Trans. Serv. Comput. 8(1), 136–154 (2015). http://doi.ieeecomputersociety.org/10.1109/TSC.2013.51
Fellmann, M., Zasada, A.: State-of-the-art of business process compliance approaches. In: 22st European Conference on Information Systems, ECIS 2014, Tel Aviv, Israel, 9–11 June 2014 (2014). http://aisel.aisnet.org/ecis2014/proceedings/track06/8
Gabbay, D.M.: The declarative past and imperative future: executable temporal logic for interactive systems. In: Temporal Logic in Specification, Altrincham, UK, 8–10 April 1987, Proceedings, pp. 409–448 (1987)
Ghamarian, A.H., de Mol, M., Rensink, A., Zambon, E., Zimakova, M.: Modelling and analysis using GROOVE. STTT 14(1), 15–40 (2012). http://dx.doi.org/10.1007/s10009-011-0186-x
Gorp, P.V., Dijkman, R.M.: A visual token-based formalization of BPMN 2.0 based on in-place transformations. Inf. Softw. Technol. 55(2), 365–394 (2013). http://dx.doi.org/10.1016/j.infsof.2012.08.014
Hausmann, J.H.: Dynamic META modeling: a semantics description technique for visual modeling languages. Ph.D. thesis, University of Paderborn (2005). http://ubdata.uni-paderborn.de/ediss/17/2005/hausmann/disserta.pdf
Knuplesch, D., Reichert, M., Fdhila, W., Rinderle-Ma, S.: On enabling compliance of cross-organizational business processes. In: Daniel, F., Wang, J., Weber, B. (eds.) BPM 2013. LNCS, vol. 8094, pp. 146–154. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40176-3_12
Kwantes, P.M.: Design of clearing and settlement operations: a case study in business process modelling and evaluation with petri nets. In: 7th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools (CPN 2006) (2006)
Martens, A.: On compatibility of web services. Petri Net Newsletter 65, 12–20 (2003)
Muram, F.U., Tran, H., Zdun, U.: Automated mapping of UML activity diagrams to formal specifications for supporting containment checking. In: Proceedings 11th International Workshop on Formal Engineering Approaches to Software Components and Architectures, FESCA 2014, Grenoble, France, 12th April 2014, pp. 93–107 (2014), http://dx.doi.org/10.4204/EPTCS.147.7
OMG: Business process model and notation (BPMN) version 2.0. Technical report, Jan 2011. http://taval.de/publications/BPMN20
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pp. 46–57 (1977). http://dx.doi.org/10.1109/SFCS.1977.32
Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comput. Sci. 13, 45–60 (1981). doi:10.1016/0304-3975(81)90110-9
Rensink, A.: The GROOVE simulator: a tool for state space generation. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004). doi:10.1007/978-3-540-25959-6_40
SMPG: Securities markets practices group/market practices and documents/settlement and reconciliation. http://www.smpg.info, Mar 2015
S.W.I.F.T.: ISO15022 financial industry message scheme. http://www.iso15022.org, Mar 2015
S.W.I.F.T.: ISO20022 universal financial industry message scheme. http://www.iso20022.org, Mar 2015
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Kwantes, P.M., Van Gorp, P., Kleijn, J., Rensink, A. (2015). Towards Compliance Verification Between Global and Local Process Models. In: Parisi-Presicce, F., Westfechtel, B. (eds) Graph Transformation. ICGT 2015. Lecture Notes in Computer Science(), vol 9151. Springer, Cham. https://doi.org/10.1007/978-3-319-21145-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-21145-9_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-21144-2
Online ISBN: 978-3-319-21145-9
eBook Packages: Computer ScienceComputer Science (R0)