--- abstract: 'Event-B is a refinement-based formal method that has been shown to be useful in developing concurrent and distributed programs. Large models can be decomposed into sub-models that can be refined semi-independently and executed in parallel. In this paper, we show how to introduce explicit control flow for the concurrent sub-models in the form of event schedules. We explore how schedules can be designed so that their application results in a correctness-preserving refinement step. For practical application, two patterns for schedule introduction are provided, together with their associated proof obligations. We demonstrate our method by applying it on the dining philosophers problem.' accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: [] creators_name: - family: Boström given: Pontus honourific: '' lineage: '' - family: Degerlund given: Fredrik honourific: '' lineage: '' - family: Sere given: Kaisa honourific: '' lineage: '' - family: Waldén given: Marina honourific: '' lineage: '' data_type: ~ date: 2011-06 date_type: published datestamp: 2011-11-16 09:32:55 department: ~ dir: disk0/00/00/03/56 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 356 event_dates: 20th June 2011 event_location: 'Limerick, Ireland' event_title: 15th International Refinement Workshop (associated with Formal Methods 2011) event_type: workshop exhibitors_id: [] exhibitors_name: [] fileinfo: '' full_text_status: none funders: - Supported by the EU DEPLOY project id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: pub 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: 2011-11-16 09:32:55 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: http://eptcs.org/paper.cgi?Refine2011.11 output_media: ~ pagerange: 166-182 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: 9 series: ~ skill_areas: [] source: ~ status_changed: 2011-11-16 09:32:55 subjects: - Event-Bsemantics - Refinement - deploy_method - theory succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Concurrent Scheduling of Event-B Models type: conference_item userid: 20 volume: ~