---
abstract: 'In this short paper we describe early work on a case study concerning a power window control unit. We use UML-B state machines to simultaneously model both the cyclic processing schedule and the mode of control behaviour. We find this a useful way to visualise the model, particularly when the state machines are animated via the Pro-B animator. We verify the state machines using the Event-B proof tools. We envisage new developments to the UML-B tool set to improve support for this modelling technique. The motivation for this simple but powerful form of modelling is the immediate benefit and low cost of entry making industrial adoption of formal models more attractive to industry.'
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: ''
data_type: ~
date: 2011-06
date_type: published
datestamp: 2012-07-23 09:55:11
department: ~
dir: disk0/00/00/04/29
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 429
event_dates: ~
event_location: ~
event_title: B2011
event_type: workshop
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: ~
lastmod: 2012-07-23 09:55:11
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ' Event Dates: 21st June 2011'
num_pieces: ~
number: ~
official_url: http://eprints.soton.ac.uk/272287/
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: 8
series: ~
skill_areas: []
source: ~
status_changed: 2012-07-23 09:55:11
subjects:
  - Refinement
  - deploy_method_other
  - deploy_method_reqevo
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Modelling Control Process and Control Mode with Synchronising Orthogonal State Machines
type: conference_item
userid: 258
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>