Key Analysis of Normalization Process Using Formal Techniques in DBRE

Database systems are considered as an integral part of any software system, therefore, all complex systems maintain a database in different formats. Relational database management systems are based on relational model for creation and storage of databases. Database reverse engineering (DBRE) is a process of extracting the database requirements from an operational database system. Objective of DBRE is to enhance and maintain an existing system in an optimal way. Of course, DBRE process requires a detailed mathematical analysis to achieve the objective of optimality. For efficient data manipulation in a database system mathematical techniques and algorithms are required. Formal methods can be used to achieve this objective from existing code to a conceptual model. Formal methods are mathematical based techniques which can be used for analyzing and specifying the properties of software and hardware systems. In this paper, we have applied formal methods to formalize some of the processes of DBRE techniques. We have formalized the process of extracting primary and foreign keys, strong and weak entities using Z notation. The model is analyzed and validated using Z/EVES tool. It is observed that application of formal methods in DBRE was not only useful in capturing the requirements of a system but it has also increased the confidence throughout the process.