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

The taxonomy of the causes of proof failures and a verification methodology called the hierarchical development methodology (HDM) are presented. The verification process is specified by describing the data that flows into the process, the analysis that is performed on the data, and the data that flows out of the process. It is discovered that in spite of the verification tools, there is always going to be a significant amount of analysis that must be done manually. Manual analysis of proof failures reveals that there are typically only a small number of distinct causes of the failure. Some failures are the propagation of a single error such as one in the data dictionary. Some failures occur because of conventions used in the verification methodology