Formal specification scheme for database applications using requirements particle networks

This paper proposes a systematic scheme for synthesizing formal specification from the definitions of relational data model – entity relationship diagram and their data dictionaries. The formal specification of both structural and behavioral properties of relational data model is generated in Z schemas. In our approach, the mandatory structural constraints – the uniqueness of primary key, foreign keys, and referential integrity constraints among the relations in the model, are preserved. We propose a set of transformation rules to produce Z schemas of the states and primitive operations – cascade insertion, deletion, and updating. Moreover, a composition technique of constructing the composite operations is presented by using requirements particle networks. The revision of the formal specification can be easily conducted with the mathematical proofs of the properties of the data model using Z prover tool.