TY - CONF N1 - This work has been presented at the IM FMT 2009 workshop of the IFM2009 conference, Dusseldorf, Germany on 16 February 2009 ID - deploy434 UR - http://eprints.soton.ac.uk/268268/ A1 - Said, Mar Yah A1 - Butler, Michael A1 - Snook, Colin Y1 - 2009/11// N2 - UML-B is a ?UML-like? graphical front end for Event-B that provides support for object-oriented modelling concepts. In particular, UML-B supports class diagrams and state machines, concepts that are not explicitly supported in plain Event-B. In Event-B, refinement is used to relate system models at different abstraction levels. The same abstraction-refinement concepts can also be applied in UML-B. This paper introduces the notions of refined classes and refined state machines to enable refinement of classes and state machines in UML-B. Together with these notions, a technique for moving an event between classes to facilitate abstraction is also introduced. Our work makes explicit the structures of class and state machine refinement in UML-B. The UML-B drawing tool and Event-B translator are extended to support the new refinement concepts. A case study of an auto teller machine (ATM) is presented to demonstrate application and effectiveness of refined classes and refined state machines. PB - Springer T3 - LNCS 5850 KW - visual modelling languages KW - formal specification KW - uml-b KW - event-b KW - rodin KW - refinement TI - Language and tool support for class and state machine refinement in UML-B SP - 579 M2 - Eindhoven AV - none EP - 595 T2 - Formal Methods 2009 ER -