creators_name: Bryans, Jeremy creators_name: Wei , Wei creators_id: Jeremy.Bryans@ncl.ac.uk creators_id: wei01.wei@sap.com type: conference_item datestamp: 2010-07-12 08:22:17 lastmod: 2010-07-12 08:22:17 metadata_visibility: show title: Formal Analysis of BPMN Models using Event-B ispublished: inpress subjects: Event-Bsemantics subjects: deploy_industrial subjects: deploy_tooldev full_text_status: public pres_type: paper 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. date: 2010 date_type: submitted event_title: Formal Methods for Industrial Critical Systems 2010 event_type: conference refereed: TRUE citation: Bryans, Jeremy and Wei , Wei (2010) Formal Analysis of BPMN Models using Event-B. In: Formal Methods for Industrial Critical Systems 2010. (In Press) document_url: http://deploy-eprints.ecs.soton.ac.uk/237/1/root.pdf