--- abstract: "Distributed information systems are critical to the functioning of\r\nmany businesses; designing them to be dependable is a challenging but\r\nimportant task. We report our experience in using formal methods to\r\nenhance processes and tools for development of business information\r\nsoftware based on service-oriented architectures. In our work, which\r\ntakes place in an industrial setting, we focus on the configuration of\r\nmiddleware, verifying application-level requirements in the presence\r\nof faults. In pilot studies provided by SAP, we used the Event-B\r\nformalism and the open RODIN tools platform to prove properties of\r\nmodels of business protocols and expose weaknesses of certain\r\nmiddleware configurations with respect to particular protocols. We\r\nthen extended the approach to use models automatically generated from\r\ndiagrammatic design tools, opening the possibility of seamless\r\nintegration with current development environments. Increased\r\nautomation in the verification process, through domain-specific models\r\nand theories, is a goal for future work. " 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 - john.fitzgerald@ncl.ac.uk - alexander.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: Alexander given: Romanovsky honourific: '' lineage: '' - family: Andreas given: Roth honourific: '' lineage: '' data_type: ~ date: 2008-12-15 date_type: submitted datestamp: 2008-12-18 14:43:04 department: ~ dir: disk0/00/00/00/52 divisions: [] edit_lock_since: ~ edit_lock_until: ~ edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 52 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/52/1/Bryans%2Det%2Dal.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: 'Verification, Fault Assumptions, Service-Oriented Architectures, Event-B, Tool Support ' lastmod: 2010-04-19 15:05:51 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: http://www.cs.ncl.ac.uk/publications/techreports/trs/papers/1131.pdf output_media: ~ pagerange: ~ pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: 'Newcastle University TR, accepted to appear in Proceedings of ICECCS 2009' pres_type: ~ producers_id: [] producers_name: [] projects: - DEPLOY publication: ~ publisher: Newcastle University refereed: ~ referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 29 series: ~ skill_areas: [] source: ~ status_changed: 2008-12-18 14:43:04 subjects: - deploy_method_comp - deploy_industrial_bus - deploy_method_resil - examples succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: "Formal Modelling and Analysis of Business Information\r\nApplications with Fault Tolerant Middleware \r\n\r\n" type: other userid: 43 volume: ~