Paper Info
Title
Language and Tool Support for Class and State Machine Refinement in UML-B
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.
Year
DOI
Venue
2009
10.1007/978-3-642-05089-3_37
FM
Keywords
Field
DocType
plain event-b,state machine,auto teller machine,new refinement concept,uml-b drawing tool,event-b translator,state machine refinement,refined class,refined state machine,class diagram,tool support,refinement,formal specification,front end,uml,system modeling
Front and back ends,Programming language,Abstraction,Refinement calculus,Unified Modeling Language,Computer science,Formal specification,Theoretical computer science,Finite-state machine,Atmosphere (unit),Class diagram
Conference
Volume
ISSN
Citations 
5850
0302-9743
21
PageRank 
References 
Authors
1.09
14
3
Name
Order
Citations
PageRank
Mar Yah Said1302.36
Michael Butler21768104.74
Colin Snook320315.41