A method of refinement in UML-B
UML-B is a ‘UML-like’ graphical front end for Event-B that provides support for object-oriented and state-machine modelling concepts, which are not available in Event-B. In particular, UML-B includes class diagram and state-machine diagram editors with automatic generation of corresponding Event-B....
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Springer-Verlag Berlin Heidelberg
2015
|
| Online Access: | http://psasir.upm.edu.my/id/eprint/43510/ http://psasir.upm.edu.my/id/eprint/43510/1/A%20method%20of%20refinement%20in%20UML.pdf |
| _version_ | 1848850247706476544 |
|---|---|
| author | Said, Mar Yah @ Mek Yah Butler, Micheal Snook, Colin |
| author_facet | Said, Mar Yah @ Mek Yah Butler, Micheal Snook, Colin |
| author_sort | Said, Mar Yah @ Mek Yah |
| building | UPM Institutional Repository |
| collection | Online Access |
| description | UML-B is a ‘UML-like’ graphical front end for Event-B that provides support for object-oriented and state-machine modelling concepts, which are not available in Event-B. In particular, UML-B includes class diagram and state-machine diagram editors with automatic generation of corresponding Event-B. In Event- B, refinement is used to relate system models at different abstraction levels. The same refinement concepts are also applicable in UML-B but require special consideration due to the higher-level modelling concepts. In previous work we described a case study to introduce support for refinement in UML-B. We now provide a more complete presentation of the technique of refinement in UML-B including a formalisation of the refinement rules and a definition of the extensions to the abstract syntax of UML-B notation. The provision of gluing invariants to discharge the proof obligations associated with a refinement is a significant step in providing verifiable models. We discuss and compare two approaches for constructing gluing invariants in the context of UML-B refinement. |
| first_indexed | 2025-11-15T10:03:16Z |
| format | Article |
| id | upm-43510 |
| institution | Universiti Putra Malaysia |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-15T10:03:16Z |
| publishDate | 2015 |
| publisher | Springer-Verlag Berlin Heidelberg |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | upm-435102017-05-25T08:04:41Z http://psasir.upm.edu.my/id/eprint/43510/ A method of refinement in UML-B Said, Mar Yah @ Mek Yah Butler, Micheal Snook, Colin UML-B is a ‘UML-like’ graphical front end for Event-B that provides support for object-oriented and state-machine modelling concepts, which are not available in Event-B. In particular, UML-B includes class diagram and state-machine diagram editors with automatic generation of corresponding Event-B. In Event- B, refinement is used to relate system models at different abstraction levels. The same refinement concepts are also applicable in UML-B but require special consideration due to the higher-level modelling concepts. In previous work we described a case study to introduce support for refinement in UML-B. We now provide a more complete presentation of the technique of refinement in UML-B including a formalisation of the refinement rules and a definition of the extensions to the abstract syntax of UML-B notation. The provision of gluing invariants to discharge the proof obligations associated with a refinement is a significant step in providing verifiable models. We discuss and compare two approaches for constructing gluing invariants in the context of UML-B refinement. Springer-Verlag Berlin Heidelberg 2015 Article PeerReviewed application/pdf en http://psasir.upm.edu.my/id/eprint/43510/1/A%20method%20of%20refinement%20in%20UML.pdf Said, Mar Yah @ Mek Yah and Butler, Micheal and Snook, Colin (2015) A method of refinement in UML-B. Software and Systems Modeling, 14 (4). pp. 1557-1580. ISSN 1619-1366; ESSN: 1619-1374 http://link.springer.com/article/10.1007/s10270-013-0391-z 10.1007/s10270-013-0391-z |
| spellingShingle | Said, Mar Yah @ Mek Yah Butler, Micheal Snook, Colin A method of refinement in UML-B |
| title | A method of refinement in UML-B |
| title_full | A method of refinement in UML-B |
| title_fullStr | A method of refinement in UML-B |
| title_full_unstemmed | A method of refinement in UML-B |
| title_short | A method of refinement in UML-B |
| title_sort | method of refinement in uml-b |
| url | http://psasir.upm.edu.my/id/eprint/43510/ http://psasir.upm.edu.my/id/eprint/43510/ http://psasir.upm.edu.my/id/eprint/43510/ http://psasir.upm.edu.my/id/eprint/43510/1/A%20method%20of%20refinement%20in%20UML.pdf |