---
abstract: 'State machines are hierarchical automata that are widely used to structure complex behavioural specifications. We develop two notions of refinement of state machines, node refinement and edge refinement. We compare the two notions by means of examples and argue that, by adopting simple conventions, they can be combined into one method of refinement. In the combined method, node refinement can be used to develop architectural aspects of a model and edge refinement to develop algorithmic aspects. The two notions of refinement are grounded in previous work. Event-B is used as the foundation for our refinement theory and UML-B state machine refinement influences the style of node refinement. Hence we propose a method with direct proof of state machine refinement avoiding the detour via Event-B that is needed by UML-B.'
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id: []
creators_name:
  - family: Hallerstede
    given: Stefan
    honourific: ''
    lineage: ''
  - family: Snook
    given: Colin
    honourific: ''
    lineage: ''
data_type: ~
date: 2011-10
date_type: published
datestamp: 2012-07-23 09:55:40
department: ~
dir: disk0/00/00/04/28
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 428
event_dates: ~
event_location: ~
event_title: 'ICFEM 2011: 13th International Conference on Formal Engineering Methods'
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: Refinement State Machines
lastmod: 2012-07-23 09:55:40
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ' Event Dates: 26th--28th October 2011'
num_pieces: ~
number: ~
official_url: http://eprints.soton.ac.uk/272940/
output_media: ~
pagerange: ~
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: 2012-07-23 09:55:40
subjects:
  - Refinement
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Refining Nodes and Edges of State Machines
type: conference_item
userid: 258
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>