TY - CONF ID - deploy433 UR - http://eprints.soton.ac.uk/267133/ A1 - Said, Mar Yah A1 - Butler, Michael A1 - Snook, Colin TI - Class and State Machine Refinement in UML-B Y1 - 2009/02// N2 - 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 re?nement concepts. Development in Event-B is done through re?nements of an abstract model. Since Event-B is re?ected in UML-B, the abstraction-re?nement concepts must also be catered for in UML-B. UML-B introduced the new concept of re?nement, where model complexity is managed by introducing more detailed versions of a machine. We extend this re?nement concept by introducing the notion of re?ned classes and re?ned state machines. A re?ned class is one that re?nes a more abstract class and a re?ned state machine is one that re?nes a more abstract state machine. The UML-B drawing tool and Event-B translator are extended to support the re?nement concepts. A case study of an auto teller machine (ATM) is presented to demonstrate the notion of re?ned classes and re?ned state machines. AV - none T2 - Integration of Model-based Formal Methods and Tools (workshop at iFM 2009) ER -