--- abstract: 'Event-B is a formal language for systems modeling, based on set theory and predicate logic. It has the advantage of mechanized proof, and it is possible to model a system in several levels of abstraction by using refinement. Discrete timing properties are important in many critical systems. However, modeling of timing properties is not directly supported in Event-B. In this paper we identify three main categories of discrete timing properties for trigger-response pattern, deadline, delay and expiry. We introduce language constructs for each of these timing properties that augment the Event-B language. We describe how these constructs can be mapped to standard Event-B constructs. To ease the process of using the timing constructs in a refinement-based development, we introduce patterns for refining the timing constructs that allow timing properties on abstract models to be replaced by timing properties on refined models. The language constructs and refinement patterns are illustrated through some generic examples. Event-B refinement allows atomic events at the abstract level to be broken down into sub-steps at the refined level. The goal of our refinement patterns is to provide an easy way to represent and correctly refine timing constraints on abstract atomic events with more elaborate timing constraints on the refined events. This paper presents an initial set of patterns.' accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: - University of Southampton creators_id: - mrs2g09@ecs.soton.acuk - mjb@ecs.soton.ac.uk creators_name: - family: Mohammad Reza given: Sarshogh honourific: '' lineage: '' - family: Michael given: Butler honourific: '' lineage: '' data_type: ~ date: 2011 date_type: published datestamp: 2012-05-16 08:21:27 department: ~ dir: disk0/00/00/04/00 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 400 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: /400/1.hassmallThumbnailVersion/AVoCS10.pdf;/400/1/AVoCS10.pdf full_text_status: public funders: [] id_number: 2011 importid: ~ institution: ~ isbn: ~ ispublished: pub issn: 1863-2122 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-05-18 14:16:52 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: http://journal.ub.tu-berlin.de/eceasst/article/view/701 output_media: ~ pagerange: ~ pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: ~ producers_id: [] producers_name: [] projects: [] publication: Automated Verification of Critical Systems 2011 publisher: ECEASST refereed: FALSE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 8 series: ~ skill_areas: [] source: ~ status_changed: 2012-05-16 08:21:27 subjects: - rt_modelling succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Specification and refinement of discrete timing properties in Event-B type: article userid: 266 volume: 46