creators_name: Said, Mar Yah creators_name: Butler, Michael creators_name: Snook, Colin type: conference_item datestamp: 2012-07-23 11:05:24 lastmod: 2012-07-23 11:05:24 metadata_visibility: show title: Language and tool support for class and state machine refinement in UML-B ispublished: pub subjects: Refinement subjects: deploy_method_other full_text_status: none pres_type: paper keywords: visual modelling languages, formal specification, uml-b, event-b, rodin, refinement note: This work has been presented at the IM FMT 2009 workshop of the IFM2009 conference, Dusseldorf, Germany on 16 February 2009 abstract: 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. date: 2009-11 date_type: published series: LNCS 5850 publisher: Springer pagerange: 579-595 event_title: Formal Methods 2009 event_location: Eindhoven event_dates: November 2009 event_type: conference refereed: TRUE book_title: FM 2009: Formal Methods official_url: http://eprints.soton.ac.uk/268268/ citation: Said, Mar Yah and Butler, Michael and Snook, Colin (2009) Language and tool support for class and state machine refinement in UML-B. In: Formal Methods 2009, November 2009, Eindhoven.