This site has been permanently archived. This is a static copy provided by the University of Southampton.

Industrial deployment of system engineering methods providing high dependability and productivity

 

Language and tool support for class and state machine refinement in UML-B

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.

Full text not available from this repository.

Official URL: http://eprints.soton.ac.uk/268268/

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.

Item Type:Conference or Workshop Item (Paper)
Additional Information:This work has been presented at the IM FMT 2009 workshop of the IFM2009 conference, Dusseldorf, Germany on 16 February 2009
Uncontrolled Keywords:visual modelling languages, formal specification, uml-b, event-b, rodin, refinement
Subjects:Methodology > Refinement
Methodology > Other
ID Code:434
Deposited By: Colin Snook
Deposited On:23 Jul 2012 11:05
Last Modified:23 Jul 2012 11:05

Repository Staff Only: item control page

Deploy-Project - All right reserved