Incremental Database Design using UML-B and Event-B

Ahmed Al-Brashdi
(University of Southampton)
Michael Butler
(University of Southampton)
Abdolbaghi Rezazadeh
(University of Southampton)

Correct operation of many critical systems is dependent on the data consistency and integrity properties of underlying databases. Therefore, a verifiable and rigorous database design process is highly desirable. This research aims to investigate and deliver a comprehensive and practical approach for modelling databases in formal methods through layered refinements. The methodology is being guided by a number of case studies, using abstraction and refinement in UML-B and verification with the Rodin tool. UML-B is a graphical representation of the Event-B formalism and the Rodin tool supports verification for Event-B and UML-B. Our method guides developers to model relational databases in UML-B through layered refinement and to specify the necessary constraints and operations on the database.

In Régine Laleau, Dominique Méry, Shin Nakajima and Elena Troubitsyna: Proceedings Joint Workshop on Handling IMPlicit and EXplicit knowledge in formal system development (IMPEX) and Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD) (IMPEX 2017 and FM&MDD 2017), Xi'An, China, 16th November 2017, Electronic Proceedings in Theoretical Computer Science 271, pp. 34–47.
Published: 12th May 2018.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: