SpringerLink
Log in

Formal Analysis of BPMN Models Using Event-B

  • Conference paper
Formal Methods for Industrial Critical Systems (FMICS 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6371))

Abstract

The use of business process models has gone far beyond documentation purposes. In the development of business applications, they can play the role of an artifact on which high level properties can be verified and design errors can be revealed in an effort to reduce overhead at later software development and diagnosis stages. This paper demonstrates how formal verification may add value to the specification, design and development of business process models in an industrial setting. The analysis of these models is achieved via an algorithmic translation from the de-facto standard business process modeling language BPMN to Event-B, a widely used formal language supported by the Rodin platform which offers a range of simulation and verification technologies.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 42.79
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 53.49
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  MATH  Google Scholar 

  2. Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Ball, E., Butler, M.: Event-b patterns for specifying fault-tolerance in multi-agent interaction. LNCS, vol. 5454, pp. 104–129. Springer, Heidelberg (2009)

    Google Scholar 

  4. Börger, E., Sörensen, O.: BPMN Core Modeling Concepts. Inheritance-Based Execution Semantics. In: Handbook of database technology. Springer, Heidelberg (to appear, 2010)

    Google Scholar 

  5. Bryans, J.W., Fitzgerald, J.S., Romanovsky, A., Roth, A.: Formal modelling and analysis of business information applications with fault tolerant middleware. In: Proc. of ICECCS 2009, pp. 68–77. IEEE Computer Society, Los Alamitos (June 2009)

    Google Scholar 

  6. Bryans, J.W., Fitzgerald, J.S., Romanovsky, A., Roth, A.: Patterns for modelling time and consistency in business information systems. In: Proc. of IECCS 2010, pp. 105–114. IEEE Computer Society, Los Alamitos (2010)

    Google Scholar 

  7. Bryans, J.W., Wei, W.: Formal Analysis of BPMN models using Event-B. Technical Report CS-TR 1201, School of Computing Science, Newcastle University (May 2010)

    Google Scholar 

  8. Cansell, D., Méry, D., Rehm, J.: Time constraint patterns for event B development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 140–154. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. Dijkman, R.M., Dumas, M., Ouyang, C.: Formal semantics and analysis of BPMN process models using Petri nets, http://eprints.qut.edu.au/7115/01/7115.pdf

  10. Fürst, A.: Design patterns in Event-B and their tool support. Master’s thesis, ETH Zürich (2009)

    Google Scholar 

  11. Hoang, T.S., Fürst, A., Abrial, J.-R.: Event-B Patterns and Their Tool Support. In: Proc. of SEFM 2009, pp. 210–219. IEEE Computer Society, Los Alamitos (2009)

    Google Scholar 

  12. Iliasov, A.: Design Components. PhD thesis, Newcastle University (2008)

    Google Scholar 

  13. Kätker, S., Patig, S.: Model-driven development of service-oriented business application systems. In: Wirtschaftsinformatik (1), vol. 246, pp. 171–180. Österreichische Computer Gesellschaft (2009), books@ocg.at

    Google Scholar 

  14. Masalagiu, C., Chin, W.-N., Andrei, Ş., Alaiba, V.: A rigorous methodology for specification and verification of business processes. Formal Aspects of Computing 21(5), 495–510 (2009)

    Article  MATH  Google Scholar 

  15. OMG. Business process model and notation (BPMN), FTF beta 1 for version 2.0, http://www.omg.org/spec/BPMN/2.0/Beta1/PDF/

  16. Prandi, D., Quaglia, P., Zannone, N.: Formal analysis of BPMN via a translation into COWS. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 249–263. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Takemura, T.: Formal semantics and verification of BPMN transaction and compensation. In: Proc. of APSCC 2008, pp. 284–290. IEEE, Los Alamitos (2008)

    Google Scholar 

  18. Wong, P.Y.H., Gibbons, J.: A process semantics for BPMN. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 355–374. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  19. Wong, P.Y.H., Gibbons, J.: A Relative Timed Semantics for BPMN. Electronic Notes in Theoretical Computer Science 229(2), 59–75 (2009)

    Article  MATH  Google Scholar 

  20. Ye, J.-H., Sun, S.-X., Wen, L., Song, W.: Transformation of BPMN to YAWL. In: CSSE (2), pp. 354–359. IEEE Computer Society, Los Alamitos (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing Science, Newcastle University, United Kingdom

    Jeremy W. Bryans

  2. SAP Research CEC Darmstadt, SAP AG, Bleichstr. 8, 64283, Darmstadt, Germany

    Wei Wei

Authors
  1. Jeremy W. Bryans
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wei Wei
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Embedded Software Laboratory, RWTH Aachen, Ahornstr. 55, 52074, Aachen, Germany

    Stefan Kowalewski

  2. Fondazione Bruno Kessler — IRST, Via Sommarive 18, 38123, Povo (Trento), Italy

    Marco Roveri

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bryans, J.W., Wei, W. (2010). Formal Analysis of BPMN Models Using Event-B. In: Kowalewski, S., Roveri, M. (eds) Formal Methods for Industrial Critical Systems. FMICS 2010. Lecture Notes in Computer Science, vol 6371. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15898-8_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15898-8_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15897-1

  • Online ISBN: 978-3-642-15898-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation