--- abstract: "Distributed information systems are critical to the functioning of many businesses; designing them to be dependable is a challenging but important task. We report our experience in using formal methods to enhance processes and tools for development of business information software based on service-oriented architectures. In our work, which takes place in an industrial setting, we focus on the configuration of middleware, verifying application-level requirements in the presence of faults. In pilot studies provided by SAP, we used the Event-B formalism and the open Rodin tools platform to prove properties of models of business protocols and expose weaknesses of certain middleware configurations with respect to particular protocols. We then extended the approach to use models automatically generated from diagrammatic design tools, opening the possibility of seamless integration with current development environments.\r\nIncreased automation in the verification process, through\r\ndomain-specific models and theories, is a goal for future\r\nwork.\r\nKEYWORDS: Verification, Fault Modelling, Service-\r\nOriented Architectures, Event-B, Tool Support" accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: Jeremy.Bryans@ncl.ac.uk copyright_holders: [] corp_creators: [] creators_id: - Jeremy.Bryans@ncl.ac.uk - John.Fitzgerald@ncl.ac.uk - A.Romanovsky@ncl.ac.uk - Andreas/Roth@sap.com creators_name: - family: Bryans given: 'Jeremy W. ' honourific: '' lineage: '' - family: Fitzgerald given: 'John S. ' honourific: '' lineage: '' - family: Romanovsky given: Alexander honourific: '' lineage: '' - family: Roth given: Andreas honourific: '' lineage: '' data_type: ~ date: 2009 date_type: published datestamp: 2009-06-06 10:52:07 department: ~ dir: disk0/00/00/01/10 divisions: [] edit_lock_since: ~ edit_lock_until: ~ edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 110 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/110/1/PublishedVersionOfICECCSpaper.pdf full_text_status: public funders: [] id_number: 978-0-7695-3702-3/09 IEEE DOI 10.1109/ICECCS.2009.29 importid: ~ institution: ~ isbn: ~ ispublished: pub 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-04-19 15:05:54 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: ~ output_media: ~ pagerange: 68-77 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: ~ producers_id: [] producers_name: [] projects: [] publication: ' Proceedings 14th IEEE International Conference on Engineering of Complex Computer Systems ICECCS 2009.' publisher: IEEE refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 21 series: ~ skill_areas: [] source: ~ status_changed: 2009-06-06 10:52:07 subjects: - Event-Bsemantics - deploy_method - deploy_industrial succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Formal Modelling and Analysis of Business Information Applications with Fault Tolerant Middleware type: article userid: 43 volume: ~