Incremental Database Design using UML-B and Event-B
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.
Keywords
Cite
@article{arxiv.1805.05514,
title = {Incremental Database Design using UML-B and Event-B},
author = {Ahmed Al-Brashdi and Michael Butler and Abdolbaghi Rezazadeh},
journal= {arXiv preprint arXiv:1805.05514},
year = {2018}
}
Comments
In Proceedings IMPEX 2017 and FM&MDD 2017, arXiv:1805.04636