---
abstract: 'Event-B is a formal language for systems modelling, 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, modelling 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 patterns, 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 have been given a semantic in terms of the standard Event-B constructs. To ease the process of using timing properties 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.'
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.ac.uk
  - mjb@ecs.soton.ac.uk
creators_name:
  - family: Mohammad Reza
    given: Sarshogh
    honourific: ''
    lineage: ''
  - family: Michael
    given: Butler
    honourific: ''
    lineage: ''
data_type: ~
date: 2012-05-05
date_type: submitted
datestamp: 2012-05-16 08:21:38
department: ~
dir: disk0/00/00/04/01
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 401
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: /401/1.hassmallThumbnailVersion/Journal.pdf;/401/1/Journal.pdf
full_text_status: public
funders: []
id_number: 2012
importid: ~
institution: ~
isbn: ~
ispublished: submitted
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-09-11 18:34:26
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: ~
producers_id: []
producers_name: []
projects: []
publication: Special Issue on Automated Verification of Critical Systems
publisher: Science of Computer Programming
refereed: FALSE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 10
series: ~
skill_areas: []
source: ~
status_changed: 2012-05-16 08:21:38
subjects:
  - ADVANCE
  - rt_modelling
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Extending Event-B with Discrete Timing Properties
type: article
userid: 266
volume: ~
