Model-based database design

Many databases contain critical resources and data upon which important decisions rely and therefore their design requires a rigorous, verifiable approach.Formal methods are mathematical and verifiable tools to specify and prove software specifications.While formal methods have been applied to database systems, there is a lack of a comprehensive, tool-supported methodology for formal development of practical database systems.This research tries to bridge the gap between the two areas by introducing an approach to rigorously design databases using the Event-B formal method.It follows a case study methodology and models this case gradually in a UML-like notation called UML-B which is translated to Event-B and verified in the Rodin platform.This PhD work presents general guidelines for modelling database applications in Event-B and proving their consistency, integrity and security considering different types of classes and relations.It provides translation method and tool to transform proved graphical models to efficient database systems.