Skip to main content
SpringerLink
Log in

Short: Graphical Specification and Automatic Verification of Business Process

  • Conference paper
  • First Online:
Book cover Networked Systems (NETYS 2014)

Part of the book series: Lecture Notes in Computer Science ((LNCCN,volume 8593))

Included in the following conference series:

Abstract

This paper deals with the integration of the formal verification techniques of business process (BP) in the design phase. In order to achieve this purpose, we use the graphical notation of Business Process Modeling Notation (BPMN) for modeling BP and specifying constraint properties to be verified. A formal semantics for some response properties are given.

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

Notes

  1. 1.

    http://www.promtools.org/prom6/

References

  1. Lodhi, A., Koppen, V., Saake, G.: Business process modeling: active research areas and challenges. Technical report 1, Faculty of Computer Science, University of Magdeburg, p. 38 (2011)

    Google Scholar 

  2. OMG. Business Process Modeling Notation (BPMN) Version 2.0. OMG Final Adopted Specification. Object Management Group (2011)

    Google Scholar 

  3. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)

    Book  Google Scholar 

  4. Heljanko, K.: Model checking the branching time temporal logic CTL. Research report A45, Digital Systems Laboratory, Helsinki University of Technology, Espoo, Finland (1997)

    Google Scholar 

  5. Takemura, T.: Formal semantics and verification of BPMN transaction and compensation. In: Proceedings of APSCC 2008, pp. 284–290. IEEE (2008)

    Google Scholar 

  6. EI Hichami, O., AI Achhab, M., Berrada, I., Oucheikh, R., El Mohajir, B.E.: An approach of optimisation and formal verification of workflow Petri nets. J. Theor. Appl. Inf. Technol. 61(3), 486–495 (2014)

    Google Scholar 

  7. van der Aalst, W.M.P., van Dongen, B.F.: Discovering Petri nets from event logs. In: Jensen, K., van der Aalst, W.M.P., Balbo, G., Koutny, M., Wolf, K. (eds.) Transactions on Petri Nets and Other Models of Concurrency VII. LNCS, vol. 7480, pp. 372–422. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  8. Fahland, D., Favre, C., Koehler, J., Lohmann, N., Volzer, H., Wolf, K.: Analysis on demand: instantaneous soundness checking of industrial business process models. Data Knowl. Eng. 70(5), 448–466 (2011)

    Article  Google Scholar 

  9. Dijkman, R.M., Dumas, M., Ouyang, C.: Formal semantics and analysis of BPMN process models using Petri nets. Technical report 7115, Queensland University of Technology, Brisbane (2007)

    Google Scholar 

  10. Murata, T., Koh, J.Y.: Petri nets: properties, analysis and applications. an invited survey paper. Proc. IEEE 77(4), 541–580 (1989)

    Article  Google Scholar 

  11. van der Aalst, W.M.P., van Dongen, B.F., Günther, C.W., Mans, R.S., de Medeiros, A.K.A., Rozinat, A., Rubin, V., Song, M., Verbeek, H.M.W.E., Weijters, A.J.M.M.T.: ProM 4.0: comprehensive support for real process analysis. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 484–494. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Sciences, UAE, Tetouan, Morocco

    Outman El Hichami & Badr Eddine El Mohajir

  2. National School of Applied Sciences, UAE, Tetouan, Morocco

    Mohammed Al Achhab

  3. Faculty of Sciences and Technology, USMBA, Fez, Morocco

    Ismail Berrada

Authors
  1. Outman El Hichami
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mohammed Al Achhab
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ismail Berrada
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Badr Eddine El Mohajir
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Outman El Hichami .

Editor information

Editors and Affiliations

  1. Northeastern University, Boston, Massachusetts, USA

    Guevara Noubir

  2. Université de Rennes 1, Rennes Cedex, France

    Michel Raynal

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

El Hichami, O., Al Achhab, M., Berrada, I., El Mohajir, B.E. (2014). Short: Graphical Specification and Automatic Verification of Business Process. In: Noubir, G., Raynal, M. (eds) Networked Systems. NETYS 2014. Lecture Notes in Computer Science(), vol 8593. Springer, Cham. https://doi.org/10.1007/978-3-319-09581-3_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-09581-3_27

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-09580-6

  • Online ISBN: 978-3-319-09581-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation