---
abstract: "UML-B is a `UML like' notation based on the Event-B formalism which allows models to be progressively detailed through refinements that are proven to be consistent and to satisfy safety invariants using the Rodin platform and its automatic proof tools. UML, on the other hand, encourages large models to be expressed in a single, detailed level and relies on simulation and model testing techniques for verification. The advantage of proof over model-testing is that the proof is valid for all instantiations of the model whereas a simulation must choose a typical instantiation. In the INESS project we take an extant UML model of a railway interlocking system and explore methodical ways to translate it into UML-B in such a way as to facilitate proof that the model satisfies certain safety properties which are expressed as invariants. We describe the translation attempted so far and insights that we have gained from attempting to prove a safety property. We propose some possible improvements to the translation which we believe will make the proof easier. "
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id: []
creators_name:
  - family: Snook
    given: Colin
    honourific: ''
    lineage: ''
  - family: Savicks
    given: Vitaly
    honourific: ''
    lineage: ''
  - family: Butler
    given: Michael
    honourific: ''
    lineage: ''
data_type: ~
date: 2011
date_type: published
datestamp: 2012-07-23 12:29:58
department: ~
dir: disk0/00/00/04/44
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 444
event_dates: 29 Nov 2010
event_location: Graz
event_title: Formal Methods for Components and Objects
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: UML-B UML
lastmod: 2012-07-23 12:29:58
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: http://eprints.soton.ac.uk/272921/
output_media: ~
pagerange: 251
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: paper
producers_id: []
producers_name: []
projects: []
publication: Lecture Notes in Computer Science
publisher: Springer
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 10
series: ~
skill_areas: []
source: ~
status_changed: 2012-07-23 12:29:58
subjects:
  - Refinement
  - deploy_industrial_trans
  - deploy_method_proof
  - examples
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Verification of UML models by translation to UML-B
type: conference_item
userid: 258
volume: 6957
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>