Specification and verification of temporal relationships in transaction modelling

摘要

The specification of temporal semantics of the universe of discourse has not been addressed in most data modelling methodologies. A technique for incorporating temporal semantics in a particular dynamic modelling methodology is outlined. This is done by deducing the relative orderings of the transactions from the specifications and then expressing these as propositional temporal logic formulae. The tableau method is then applied to construct a dependency graph. If the specification is correct, this method guarantees that all the possible execution paths satisfying the specification will be generated. The failure to generate the graph implies an incorrect specification.