Methodology of refinement and decomposition in UML-B

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 work introduces the notions of refined classes, refined state machines and extended classtypes to enable refinement of classes and state machines in UML-B. This work makes explicit the structures of class and state machine refinement in UML-B. This work also introduces seven refinement techniques which are, adding new attributes and associations, adding new classes, elaborating state, elaborating transition, moving a class event (or a state machine transition), adding new attributes and associations, and adding new class types.<br/><br/>In Event-B, decomposition is used to decompose a system into components. The same decomposition concepts can be applied in UML-B. This work introduces the techniques of flattening state machines and state grouping to facilitate a decomposition of a UML-B machine. This work also introduces the notion of composed machine which composes the component machines. The composed machine refines a machine which is being decomposed. The composed machine is used to ensure the composition of the component machines is a valid refinement. Together with the composed UML-B machine, the notions of included machine, composed event and constituent event are introduced.<br/><br/>The UML-B drawing tool and Event-B translator are extended to support the new refinement and decomposition concepts. A case study of an auto teller machine (ATM) is presented to validate the extensions of UML-B with regards to the above notions. The ATM case study also demonstrates the above techniques introduced in refinement and decomposition. In addition, this work provides guidelines for performing refinement and decomposition in UML-B and presents a number of generic invariants that may be used when refining a middleware. The middleware is a component via which a requesting component such as an ATM and a responding component such as bank interact in a distributed system.

Name dc:type.qualificationname

Ph.D.

Level dc:type.qualificationlevel

doctoral

Grantor dc:publisher.institution

University of Southampton

Year dc:date.issued

2010

Author dc:creator

• Said, Mar Yah

Advisors dc:contributor.advisor

• Butler, Michael
• Snook, Colin