--- abstract: " The use of business process models has gone far beyond documentation\r\n purposes. In the development of business applications, they can play\r\n the role of an artifact on which high level properties can be\r\n verified and design errors can be revealed in an effort to reduce\r\n overhead at later software development and diagnosis stages. This\r\n paper demonstrates how formal verification may add value to the\r\n specification, design and development of business process models in\r\n an industrial setting. The analysis of these models is achieved via\r\n an algorithmic translation from the de-facto standard business\r\n process modeling language BPMN to Event-B, a widely used formal\r\n language supported by the Rodin platform which offers a range of\r\n simulation and verification technologies." accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - Jeremy.Bryans@ncl.ac.uk - wei01.wei@sap.com creators_name: - family: Bryans given: Jeremy honourific: '' lineage: '' - family: 'Wei ' given: Wei honourific: '' lineage: '' data_type: ~ date: 2010 date_type: submitted datestamp: 2010-07-12 08:22:17 department: ~ dir: disk0/00/00/02/37 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 237 event_dates: ~ event_location: ~ event_title: Formal Methods for Industrial Critical Systems 2010 event_type: conference exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/237/1/root.pdf full_text_status: public funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: inpress issn: ~ item_issues_comment: [] item_issues_count: 0 item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2010-07-12 08:22:17 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: ~ output_media: ~ pagerange: ~ pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: paper producers_id: [] producers_name: [] projects: [] publication: ~ publisher: ~ refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 28 series: ~ skill_areas: [] source: ~ status_changed: 2010-07-12 08:22:17 subjects: - Event-Bsemantics - deploy_industrial - deploy_tooldev succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Formal Analysis of BPMN Models using Event-B type: conference_item userid: 43 volume: ~