Consistency checking between data and process diagrams based on formal methods

One of the most important problems in software development using CASE tools is that it is impossible to verify semantical consistency between data and procedure descriptions expressed in structured diagrams. We introduce formal methods into the CASE tools in order to verify strictly the consistency between them. In this paper, we present methods for verifying that behavior of PAD (Process Action Diagram) keeps the data constraints of ERD (Entity Relationship Diagram) using the Z notation. We may improve accuracy of specification by means of giving assurance of validity among different kinds or different abstract levels of diagrams, based on the formal descriptions in Z.