"433","Class and State Machine Refinement in UML-B ","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.","http://deploy-eprints.ecs.soton.ac.uk/433/","Said, Mar Yah and Butler, Michael and Snook, Colin","UNSPECIFIED","       <span class=\"person_name\">Said, Mar Yah</span> and <span class=\"person_name\">Butler, Michael</span> and <span class=\"person_name\">Snook, Colin</span>     (2009)  <a href=\"http://deploy-eprints.ecs.soton.ac.uk/433/\"><em>Class and State Machine Refinement in UML-B.</em></a>       In:  Integration of Model-based Formal Methods and Tools (workshop at iFM 2009).           ","","2009-02"