Said, Mar Yah and Butler, Michael and Snook, Colin (2009) Class and State Machine Refinement in UML-B. In: Integration of Model-based Formal Methods and Tools (workshop at iFM 2009).
Full text not available from this repository.
Official URL: http://eprints.soton.ac.uk/267133/
Abstract
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.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Subjects: | Methodology > Refinement Methodology > Other |
| ID Code: | 433 |
| Deposited By: | Colin Snook |
| Deposited On: | 23 Jul 2012 11:02 |
| Last Modified: | 23 Jul 2012 11:02 |
Repository Staff Only: item control page
