A taxonomy of the causes of proof failures in applications using the HDM methodology

A methodology for formal verification and validation based on HDM (Hierarchical Development Methodology) is described. The HDM formula generator and theorem prover is used to perform data flow analysis on the system specification. In applying this methodology, the author discovered that although there may be a large number of individual proof failures, there were always only a small number of distinct causes of the failures. The taxonomy of the causes of these proof failures is discussed. The causes of proof failures are discussed in connection with the following categories: actual and formal parameters, printer copying, data dictionary, partial and complete copy, packed access, resolved in context, propagation resultant, and indirect integrity