Incremental Database Design using UML-B and Event-B
This work addresses the need for rigorous database design in critical systems, but it appears incremental as it builds on existing formal methods like UML-B and Event-B.
The research tackled the problem of ensuring data consistency and integrity in critical systems by developing a verifiable database design process using UML-B and Event-B, resulting in a method that guides developers to model relational databases through layered refinement with constraints and operations.
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.