Formal development of databases in ASSO and B

Matthews B, Locuratolo E

Formal methods  Refinement  Conceptual modelling  Logical design 

ASSO is a formal methodology for conceptual databases design which uses aspects of the B method. In this paper, we discuss the formal relationship between specification in ASSO and in B, defined in terms of a translation which we prove to be sound. Further we go onto discuss refinement in ASSO, which separates behavioural and data refinement, their formal relationship and their relation to refinement in B. In this manner we can use B theory and tools to support database development in ASSO.