Skip to main content
SpringerLink
Log in

Evaluating Efficiency of ArchiMate Business Processes Verification with NuSMV

  • Conference paper
Information Technology for Management

Part of the book series: Lecture Notes in Business Information Processing ((LNBIP,volume 243))

  • 504 Accesses

Abstract

The motivation for our work was an idea of integrating formal verification with business processes modeling. In the presented approach ArchiMate was selected as a language used for definition of processes. We describe a procedure, which extracts behavioral elements from ArchiMate specification and transforms them into a corresponding representation used by NuSMV model checker. Then, we focus on time efficiency of the verification task. We give results of tests performed on a set of artificial process specifications, as well as on a complex business process, whose development was supported by the implemented solution. We compare three semantics of ArchiMate process definitions and discuss their influence on model complexity and verification time.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Morimoto, S.: A survey of formal verification for business process modeling. In: Bubak, M., van Albada, G.D., Dongarra, J., Sloot, P.M.A. (eds.) ICCS 2008, Part II. LNCS, vol. 5102, pp. 514–522. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. OMG: Business Process Model and Notation (BPMN) version 2.0. Technical report, OMG, January 2011

    Google Scholar 

  3. Scheer, A.-W., Nüttgens, M.: ARIS architecture and reference models for business process management. In: van der Aalst, W.M.P., Desel, J., Oberweis, A. (eds.) Business Process Management. LNCS, vol. 1806, pp. 376–389. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  4. The Open Group: Open Group Standard. Archimate 2.1 Specificattion. Van Haren Publishing, Zaltbommel (2013)

    Google Scholar 

  5. Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. (CSUR) 28(4), 626–643 (1996)

    Article  Google Scholar 

  6. Clarke, E.M., Klieber, W., Nováček, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1–30. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  7. Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. (CSUR) 24(3), 293–318 (1992)

    Article  Google Scholar 

  8. Huuck, R.: Formal verification, engineering and business value. In: Olveczky, P.C., Artho, C. (eds.) Proceedings First International Workshop on Formal Techniques for Safety-Critical Systems, Kyoto, Japan, November 12, 2012, Electronic Proceedings in Theoretical Computer Science, vol. 105, pp. 1–4. Open Publishing Association (2012)

    Google Scholar 

  9. Beauvoir, P.: Archi, archimate modelling tool (2015). Accessed March 2015

    Google Scholar 

  10. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  11. Szwed, P.: Verification of archimate behavioral elements by model checking. In: Saeed, K., Homenda, W. (eds.) Computer Information Systems and Industrial Management. Lecture Notes in Computer Science, vol. 9339, pp. 132–144. Springer International Publishing, Warsaw (2015)

    Chapter  Google Scholar 

  12. Szwed, P.: Efficiency of formal verification of archimate business processes with nusmv model checker. In: Federated Conference on Computer Science and Information Systems (FedCSIS), pp. 1427–1436 (2015)

    Google Scholar 

  13. Watahiki, K., Ishikawa, F., Hiraishi, K.: Formal verification of business processes with temporal and resource constraints. In: 2011 IEEE International Conference on Systems, Man, and Cybernetics (SMC), pp. 1173–1180. IEEE (2011)

    Google Scholar 

  14. Anderson, B., Hansen, J.V., Lowry, P., Summers, S.: Model checking for e-business control and assurance. IEEE Trans. Syst. Man, Cybern. C Appl. Rev. 35(3), 445–450 (2005)

    Article  Google Scholar 

  15. Mongiello, M., Castelluccia, D.: Modelling and verification of BPEL business processes. In: Fourth and Third International Workshop on Model-Based Development of Computer-Based Systems and Model-Based Methodologies for Pervasive and Embedded Software, MBD/MOMPES 2006, p. 5. IEEE (2006)

    Google Scholar 

  16. Fu, X., Bultan, T., Su, J.: Formal verification of e-services and workflows. In: Bussler, C.J., McIlraith, S.A., Orlowska, M.E., Pernici, B., Yang, J. (eds.) CAiSE 2002 and WES 2002. LNCS, vol. 2512, pp. 188–202. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: Proceedings of the 12th International Conference on Database Theory, pp. 252–267. ACM (2009)

    Google Scholar 

  18. Wynn, M.T., Verbeek, H., van der Aalst, W.M., ter Hofstede, A.H., Edmond, D.: Business process verification-finally a reality!. Bus. Process Manag. J. 15(1), 74–92 (2009)

    Article  Google Scholar 

  19. Van der Aalst, W.M., Ter Hofstede, A.H.: YAWL: Yet Another Workflow Language. Inf. Syst. 30(4), 245–275 (2005)

    Article  Google Scholar 

  20. Klimek, R., Szwed, P.: Verification of ArchiMate process specifications based on deductive temporal reasoning. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2013 Federated Conference on Computer Science and Information Systems, Kraków, Poland, 8–11 September 2013, pp. 1103–1110 (2013)

    Google Scholar 

  21. Klimek, R., Szwed, P., Jedrusik, S.: Application of deductive reasoning to the verification of ArchiMate behavioral elements. Informatyka Ekonomiczna 29, 76–97 (2013)

    Google Scholar 

  22. Klimek, R.: A system for deduction-based formal verification of workflow-oriented software models. Appl. Math. Comput. Sci. 24(4), 941–956 (2014)

    MATH  Google Scholar 

  23. Clarke, E.M., Grumberg, O., Hiraishi, H., Jha, S., Long, D.E., McMillan, K.L., Ness, L.A.: Verification of the futurebus+ cache coherence protocol. Formal Methods Syst. Des. 6(2), 217–232 (1995)

    Article  Google Scholar 

  24. Fuxman, A., Pistore, M., Mylopoulos, J., Traverso, P.: Model checking early requirements specifications in tropos. In: Proceedings of the Fifth IEEE International Symposium on Requirements Engineering, pp. 174–181. IEEE (2001)

    Google Scholar 

  25. Bertoli, P., Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: MBP: a Model Based Planner. In: Proceedings of the IJCAI01 Workshop on Planning under Uncertainty and Incomplete Information (2001)

    Google Scholar 

  26. Clarke, E., Heinle, W.: Modular translation of statecharts to SMV. Technical report, Citeseer (2000)

    Google Scholar 

  27. Szpyrka, M., Biernacka, A., Biernacki, J.: Methods of translation of petri nets to NuSMV language. In: Popova-Zeugmann, L. (ed.) Proceedings of the 23th International Workshop on Concurrency, Specification and Programming. CEUR Workshop Proceedings, vol. 1269, pp. 245–256. CEUR-WS.org, Berlin (2014)

    Google Scholar 

  28. Andersen, H.R.: An introduction to binary decision diagrams. Lecture notes, IT University of Copenhagen (1997)

    Google Scholar 

  29. Szwed, P., Ligeza, A.: Application of OBDD diagrams in verification of tabular rule systems. Schedae Informaticae 14 (2005)

    Google Scholar 

  30. Szwed, P., Chmiel, W., Jedrusik, S., Kadluczka, P.: Business processes in a distributed surveillance system integrated through workflow. Automatyka/Automatics 17(1), 127–139 (2013)

    Article  Google Scholar 

  31. McCabe, T.: A complexity measure. IEEE Trans. SE Softw. Eng. 2(4), 308–320 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  32. Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, pp. 42–47. IEEE Computer Society Press (1993)

    Google Scholar 

  33. Szwed, P.: Application of fuzzy ontological reasoning in an implementation of medical guidelines. In: 2013 The 6th International Conference on Human System Interaction (HSI), pp. 342–349, June 2013

    Google Scholar 

  34. Szwed, P., Skrzynski, P., Grodniewicz, P.: Risk assessment for SWOP telemonitoring system based on fuzzy cognitive maps. In: Dziech, A., Czyżewski, A. (eds.) MCSS 2013. CCIS, vol. 368, pp. 233–247. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. AGH University of Science and Technology, Mickiewicza Av. 30, 30-059, Kraków, Poland

    Piotr Szwed

Authors
  1. Piotr Szwed
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Piotr Szwed .

Editor information

Editors and Affiliations

  1. Faculty of Finance and Insurance, University of Economics in Katowice, Katowice, Poland

    Ewa Ziemba

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Szwed, P. (2016). Evaluating Efficiency of ArchiMate Business Processes Verification with NuSMV. In: Ziemba, E. (eds) Information Technology for Management. Lecture Notes in Business Information Processing, vol 243. Springer, Cham. https://doi.org/10.1007/978-3-319-30528-8_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-30528-8_11

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-30527-1

  • Online ISBN: 978-3-319-30528-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation