Efficiency of Formal Verification of ArchiMate Business Processes with NuSMV Model Checker

• Autorzy: Piotr Szwed
• Języki publikacji: EN

Abstrakty

EN

We investigate an application of model checking techniques to automated verification of business processes expressed in ArchiMate language. As a verification tool the state of the art symbolic model checker NuSMV is used. The proposed approach consists in fully automated translation of behavioral elements embedded in ArchiMate models into a corresponding representation in NuSMV language and then verifying its properties specified in CTL. Since our goal is to build an interactive verification tool, we focus on time efficiency of the verification process. We report results of tests performed on artificial process models of various complexity, as well as on a real business process example. The results show, that the described approach can be applied successfully, however, verification of complex business process specifications may face the problem of state space explosion. In such a case, to make the verification feasible, various reductions and simplifications can be applied. Index Terms-ArchiMate, business process verification, model checking, NuSMV(original abstract)

Słowa kluczowe

EN

Business models

PL

Modele biznesowe

• Czasopismo: Annals of Computer Science and Information Systems
• Rocznik: 2015
• Tom: 5
• Strony: 1427--1436

Twórcy

autor

Piotr Szwed

• AGH University of Science and Technology Kraków, Poland

Bibliografia

• S. Morimoto, "A survey of formal verification for business process modeling," in Proceedings of the 8th international conference on Computational Science, Part II, ser. ICCS '08. Berlin, Heidelberg: Springer- Verlag, 2008. doi: 10.1007/978-3-540-69387-1_58. ISBN 978-3-540- 69386-4 pp. 514-522.
• OMG, "Business Process Model and Notation (BPMN) version 2.0," OMG, Tech. Rep., January 2011. [Online]. Available: http: //www.omg.org/spec/BPMN/2.0
• A. Scheer, Aris - Business Process Modeling, ser. ARIS - Business Process Modeling. Springer, 1999, no. v. 2. ISBN 9783540644385
• A.-W. Scheer and M. Nüttgens, "ARIS architecture and reference models for business process management," in Business Process Management. Springer, 2000, pp. 376-389.
• The Open Group, Open Group Standard. Archimate 2.1 Specificattion. Van Haren Publishing, Zaltbommel, 2013. ISBN 978 94 018 0003 7
• E. M. Clarke and J. M. Wing, "Formal methods: State of the art and future directions," ACM Computing Surveys (CSUR), vol. 28, no. 4, pp. 626-643, 1996.
• E. M. Clarke, W. Klieber, M. Nováˇcek, and P. Zuliani, "Model checking and the state explosion problem," in Tools for Practical Software Verification. Springer, 2012, pp. 1-30.
• R. E. Bryant, "Symbolic boolean manipulation with ordered binarydecision diagrams," ACM Computing Surveys (CSUR), vol. 24, no. 3, pp. 293-318, 1992.
• R. Huuck, "Formal verification, engineering and business value," in Proceedings First International Workshop on Formal Techniques for Safety-Critical Systems, Kyoto, Japan, November 12, 2012, ser. Electronic Proceedings in Theoretical Computer Science, P. C. Olveczky and C. Artho, Eds., vol. 105. Open Publishing Association, 2012. doi: 10.4204/EPTCS.105.1 pp. 1-4.
• [10] P. Beauvoir, "Archi, archimate modelling tool," 2015, [Online; accessed March 2015]. [Online]. Available: http://www.archimatetool.com/
• [11] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella, "NuSMV 2: An opensource tool for symbolic model checking," in Computer Aided Verification. Springer, 2002, pp. 359-364.
• [12] P. Szwed, "Verification of ArchiMate behavioral elements by model checking," in Computer Information Systems and Industrial Management, ser. Lecture Notes in Computer Science, K. Saeed and W. Homenda, Eds. Springer International Publishing, 2015, vol. 9339, pp. 132-144. ISBN 978-3-319-24368-9. [Online]. Available: http://dx.doi.org/10.1007/978-3-319-24369-6_11
• G. J. Holzmann, "The model checker SPIN," IEEE Transactions on software engineering, vol. 23, no. 5, pp. 279-295, 1997.
• G. Behrmann, A. Cougnard, A. David, E. Fleury, K. G. Larsen, and D. Lime, "Uppaal-tiga: Time for playing games!" in Computer Aided Verification. Springer, 2007, pp. 121-125.
• K. Watahiki, F. Ishikawa, and K. Hiraishi, "Formal verification of business processes with temporal and resource constraints," in Systems, Man, and Cybernetics (SMC), 2011 IEEE International Conference on. IEEE, 2011, pp. 1173-1180.
• B. Anderson, J. V. Hansen, P. Lowry, and S. Summers, "Model checking for e-business control and assurance," Systems, Man, and Cybernetics, Part C: Applications and Reviews, IEEE Transactions on, vol. 35, no. 3, pp. 445-450, 2005. doi: 10.1109/TSMCC.2004.843181
• M. Mongiello and D. Castelluccia, "Modelling and verification of BPEL business processes," in Model-Based Development of Computer-Based Systems and Model-Based Methodologies for Pervasive and Embedded Software, 2006. MBD/MOMPES 2006. Fourth and Third International Workshop on. IEEE, 2006, pp. 5-pp.
• X. Fu, T. Bultan, and J. Su, "Formal verification of e-services and workflows," in Web Services, E-Business, and the Semantic Web. Springer, 2002, pp. 188-202.
• A. Deutsch, R. Hull, F. Patrizi, and V. Vianu, "Automatic verification of data-centric business processes," in Proceedings of the 12th International Conference on Database Theory. ACM, 2009, pp. 252-267.
• M. T. Wynn, H. Verbeek, W. M. van der Aalst, A. H. ter Hofstede, and D. Edmond, "Business process verification-finally a reality!" Business Process Management Journal, vol. 15, no. 1, pp. 74-92, 2009.
• W. M. Van der Aalst and A. H. Ter Hofstede, "YAWL: yet another workflow language," Information systems, vol. 30, no. 4, pp. 245-275, 2005.
• R. Klimek and P. Szwed, "Verification of ArchiMate process specifications based on deductive temporal reasoning," in Proceedings of the 2013 Federated Conference on Computer Science and Information Systems, Kraków, Poland, September 8-11, 2013., M. Ganzha, L. A. Maciaszek, and M. Paprzycki, Eds., 2013, pp. 1103-1110. [Online].
• Available: http://fedcsis.org/2013/ R. Klimek, P. Szwed, and S. Jedrusik, "Application of deductive reasoning to the verification of ArchiMate behavioral elements," Informatyka Ekonomiczna, vol. 29, pp. 76-97, 2013.
• E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness, "Verification of the futurebus+ cache coherence protocol," Formal Methods in System Design, vol. 6, no. 2, pp. 217-232, 1995.
• A. Fuxman, M. Pistore, J. Mylopoulos, and P. Traverso, "Model checking early requirements specifications in tropos," in Requirements Engineering, 2001. Proceedings. Fifth IEEE International Symposium on. IEEE, 2001, pp. 174-181.
• P. Bertoli, A. Cimatti, M. Pistore, M. Roveri, and P. Traverso, "Mbp: a model based planner," in Proc. of the IJCAIŠ01 Workshop on Planning under Uncertainty and Incomplete Information, 2001.
• E. Clarke and W. Heinle, "Modular translation of statecharts to smv," Citeseer, Tech. Rep., 2000.
• M. Szpyrka, A. Biernacka, and J. Biernacki, "Methods of translation of Petri nets to NuSMV language," in Proceedings of the 23th International Workshop on Concurrency, Specification and Programming, Chemnitz, Germany, September 29 - October 1, 2014., ser. CEUR Workshop Proceedings, L. Popova-Zeugmann, Ed., vol. 1269. CEUR-WS.org, 2014, pp. 245-256. [Online]. Available: http://ceur-ws.org/Vol-1269/ paper245.pdf
• P. Szwed, W. Chmiel, S. Jedrusik, and P. Kadluczka, "Business processes in a distributed surveillance system integrated through workflow," Automatyka/ Automatics, vol. 17, no. 1, pp. 127-139, 2013.
• R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta, "The nuxmv symbolic model checker," in CAV, ser. Lecture Notes in Computer Science, A. Biere and R. Bloem, Eds., vol. 8559. Springer, 2014. ISBN 978-3-319-08866-2 pp. 334-342.
• T. McCabe, "A complexity measure," Software Engineering, IEEE Transactions on, vol. SE-2, no. 4, pp. 308-320, Dec 1976. doi: 10.1109/TSE.1976.233837
• H. R. Andersen, "An introduction to binary decision diagrams," Lecture notes, available online, IT University of Copenhagen, 1997.
• P. Szwed and A. Ligeza, "Application of OBDD diagrams in verification of tabular rule systems," Schedae Informaticae, vol. 14, 2005.
• R. Rudell, "Dynamic variable ordering for ordered binary decision diagrams," in Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design. IEEE Computer Society Press, 1993, pp. 42-47.
• B. Weiß, "Business process modelingand analysis in banks," 2011, [Online; accessed April 2015]. [Online]. Available: http://www.bpm. scitech.qut.edu.au/seminars/2011/BurkhardWeissBPMSeriesTalk.pdf

Identyfikatory

DOI

10.15439/2015F44