---
abstract: 'Timing diagrams provide an intuitive graphical specification for time constraints and causal dependencies between a system?s objects. Such a view can provide useful insight during Requirements Engineering (RE). Formal Modeling techniques allow abstract system level models to be explored in revealing detail and provide feedback via verification and validation methods such as proofs of consistency, model checking and animation. Here, we bring these two modelling approaches together. In particular we present techniques to extend a graphical modeling capability for formal modeling into the real-time domain by developing a Timing diagram view for the Event-B formal method and its graphical front-end, UML-B. Translation schemes to Event-B and UML-B are proposed and presented. A case study of a lift system is used to demonstrate the translation in practice.'
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id: []
creators_name:
  - family: Joochim
    given: Tossaporn
    honourific: ''
    lineage: ''
  - family: Snook
    given: Colin
    honourific: ''
    lineage: ''
  - family: Poppleton
    given: Mike
    honourific: ''
    lineage: ''
  - family: Gravell
    given: Andrew
    honourific: ''
    lineage: ''
data_type: ~
date: 2010-02
date_type: published
datestamp: 2012-07-23 10:20:34
department: ~
dir: disk0/00/00/04/31
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 431
event_dates: ~
event_location: ~
event_title: IASTED International Conference on Software Engineering (SE2010)
event_type: conference
exhibitors_id: []
exhibitors_name: []
fileinfo: ~
full_text_status: none
funders: []
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: 'Visual and Formal modeling, Timing diagram, Event-B, UML-B'
lastmod: 2012-07-23 10:20:34
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ' Event Dates: February 16 ? 18, 2010'
num_pieces: ~
number: ~
official_url: http://eprints.soton.ac.uk/268489/
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: paper
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: ACTA Press
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 7
series: ~
skill_areas: []
source: ~
status_changed: 2012-07-23 10:20:34
subjects:
  - deploy_method_other
  - deploy_method_reqevo
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: 'TIMING DIAGRAMS REQUIREMENTS MODELING USING EVENT-B FORMAL METHODS '
type: conference_item
userid: 258
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>