Language and Tool Support for Class and State Machine Refinement in UML-B Export

@incollection{citeulike:6082906, 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.}, author = {Said, Mar and Butler, Michael and Snook, Colin}, citeulike-article-id = {6082906}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-05089-3_37}, citeulike-linkout-1 = {http://www.springerlink.com/content/5042p61825437085}, doi = {10.1007/978-3-642-05089-3_37}, journal = {FM 2009: Formal Methods}, keywords = {2009, refinement, uml, umlb}, pages = {579--595}, posted-at = {2009-11-07 13:28:10}, priority = {4}, title = {Language and Tool Support for Class and State Machine Refinement in UML-B}, url = {http://dx.doi.org/10.1007/978-3-642-05089-3_37}, year = {2009} }

TY - CHAP ID - citeulike:6082906 L3 - citeulike-article-id:6082906 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. JF - FM 2009: Formal Methods EP - 595 TI - Language and Tool Support for Class and State Machine Refinement in UML-B SP - 579 KW - 2009 KW - refinement KW - uml KW - umlb AU - Said, Mar AU - Butler, Michael AU - Snook, Colin PY - 2009/// UR - http://dx.doi.org/10.1007/978-3-642-05089-3_37 ER -