--- abstract: 'Modelling and refinement in Event-B provides a scalable sup- port for the development of complex service-oriented systems. Refinement in Event-B supports a systematic service development by a gradual trans- formation of an abstract specification into a detailed service architecture. In this paper we aim at integrating quantitative assessment of desired quality of essential service attributes into formal modelling process. We propose an approach to creating and verifying a dynamic service architecture in Event- B. Such an architecture can be augmented with stochastic information and transformed into the corresponding continuous-time Markov chain represen- tation. By relying on probabilistic model-checking techniques, we allow for quantitative evaluation of quality of service attributes at early development stages. The approach is illustrated by a simple case study.' accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - Anton.Tarasyuk@abo.fi - Elena.Troubitsyna@abo.fi - Linas.Laibinis@abo.fi creators_name: - family: Tarasyuk given: Anton honourific: '' lineage: '' - family: Troubitsyna given: Elena honourific: '' lineage: '' - family: Laibinis given: Linas honourific: '' lineage: '' data_type: ~ date: 2012 date_type: published datestamp: 2012-06-29 07:54:42 department: ~ dir: disk0/00/00/04/07 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 407 event_dates: ~ event_location: 'Pisa, Italy' event_title: 9th International Conference on Integrated Formal Methods – IFM 2012 event_type: conference exhibitors_id: [] exhibitors_name: [] fileinfo: ~ full_text_status: none funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: inpress issn: ~ item_issues_comment: [] item_issues_count: ~ 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: 2012-06-29 07:54:42 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: 10 series: ~ skill_areas: [] source: ~ status_changed: 2012-06-29 07:54:42 subjects: - Event-Bsemantics - Refinement - deploy_method - deploy_method_proof - examples succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B type: conference_item userid: 20 volume: ~