creators_name: Said, Mar Yah
creators_name: Butler, Michael
creators_name: Snook, Colin
type: conference_item
datestamp: 2012-07-23 11:02:33
lastmod: 2012-07-23 11:02:33
metadata_visibility: show
title: Class and State Machine Refinement in UML-B 
ispublished: pub
subjects: Refinement
subjects: deploy_method_other
full_text_status: none
pres_type: paper
abstract: UML-B is a ’UML-like’ graphical front end for Event-B. It adds support for object oriented modeling concepts while visually retaining the Event-B
modeling concepts. In the continuity of the work on UML-B, we strengthen its
refinement concepts. Development in Event-B is done through refinements of an
abstract model. Since Event-B is reflected in UML-B, the abstraction-refinement
concepts must also be catered for in UML-B. UML-B introduced the new concept of refinement, where model complexity is managed by introducing more
detailed versions of a machine. We extend this refinement concept by introducing
the notion of refined classes and refined state machines. A refined class is one that
refines a more abstract class and a refined state machine is one that refines a more
abstract state machine. The UML-B drawing tool and Event-B translator are extended to support the refinement concepts. A case study of an auto teller machine
(ATM) is presented to demonstrate the notion of refined classes and refined state
machines.
date: 2009-02
date_type: published
event_title:  Integration of Model-based Formal Methods and Tools (workshop at iFM 2009)
event_type: workshop
refereed: TRUE
official_url: http://eprints.soton.ac.uk/267133/
citation:   Said, Mar Yah and Butler, Michael and Snook, Colin  (2009) Class and State Machine Refinement in UML-B.  In:  Integration of Model-based Formal Methods and Tools (workshop at iFM 2009).