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)
TL;DR
This paper presents a formal, layered refinement approach for designing databases using UML-B and Event-B, enabling rigorous verification of data integrity and consistency properties.
Contribution
It introduces a practical methodology for modeling relational databases with formal methods through layered refinement and verification using UML-B and Rodin.
Findings
Successful case studies demonstrating layered refinement in UML-B
Verification of database properties using Rodin tool
Guidelines for modeling constraints and operations formally
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Database Systems and Queries · Distributed systems and fault tolerance · Data Management and Algorithms