Formal analysis of BPMN models using event-B

    Research output: Chapter in Book/Report/Conference proceedingConference proceeding

    16 Citations (Scopus)

    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.
    Original languageEnglish
    Title of host publicationFormal Methods for Industrial Critical Systems
    EditorsStefan Kowalewski, Marco Roveri
    Place of PublicationBerlin
    PublisherSpringer Verlag
    Pages33-49
    Number of pages17
    Volume6371 LNCS
    ISBN (Electronic)978-3-642-15898-8
    ISBN (Print)978-3-642-15897-1
    DOIs
    Publication statusPublished - 2010
    EventInternational Workshop on Formal Methods for Industrial Critical Systems - Antwerp, Belgium
    Duration: 20 Sep 201021 Sep 2010
    Conference number: 15
    https://es-static.fbk.eu/events/fmics2010/index.php

    Publication series

    NameFMICS: International Workshop on Formal Methods for Industrial Critical Systems
    PublisherSpringer
    Volume6371

    Conference

    ConferenceInternational Workshop on Formal Methods for Industrial Critical Systems
    CountryBelgium
    CityAntwerp
    Period20/09/1021/09/10
    Internet address

    Keywords

    • business process modelling
    • verification
    • BPMN
    • Event-B

    Fingerprint Dive into the research topics of 'Formal analysis of BPMN models using event-B'. Together they form a unique fingerprint.

  • Cite this

    Bryans, J. W., & Wei, W. (2010). Formal analysis of BPMN models using event-B. In S. Kowalewski, & M. Roveri (Eds.), Formal Methods for Industrial Critical Systems (Vol. 6371 LNCS, pp. 33-49). (FMICS: International Workshop on Formal Methods for Industrial Critical Systems; Vol. 6371). Berlin: Springer Verlag. https://doi.org/10.1007/978-3-642-15898-8_3