We use the PVS specification language and its theorem proving environment to formally construct, reason with, and mechanically validate an example data model at various levels of abstraction. The methodology proposed here makes modeling resemble programming in a strongly typed language. Models are implemented as PVS theories consisting of type declarations, function definitions, axioms and theorems. Entities and relationships are expressed as types. Constraints on the data model are expressed as axioms relating entity and relationship sets. Additional correctness conditions are generated by PVS's type checker. Using the theory interpretation mechanism of PVS, we prove the correctness of the example's logical model with respect to its ER model.
The example model we consider has about fifteen attributes, entities and relationships, and twelve constraints. The complete hand-coded specification of the model is about 600 lines of PVS (including libraries). Verification of the correctness of the model reduces to interactively proving about thirty correctness conditions. The proofs of almost all of these are quite small (4 steps or less). With modest additional effort, it should be possible to automatically generate the specification and proofs, paving the way for automatic verification of data models. We see our work as the initial step towards this goal.
|
|