Automated proof support

Just as any model or piece of software, VDM models can contain errors. We can distinguish two kinds of errors: those that can be found purely by analysis of the model and those that can only be found when more information than just the model is given. The last type is in practice hard to detect automatically, since the extra information required to find them is usually not available to a computer. The first type is what this project focuses on.

Errors that can be found purely by inspection of the model are called model inconsistencies. A large body of inconsistencies can be found by the type checker, but the strength of this tool is limited to static verification. Model inconsistencies that are of a more dynamic nature cannot be detected automatically. Examples are inconsistencies that are caused by pre- and postconditions, type invariants, function termination, etc. Typically these inconsistencies will give run-time errors during execution (not only in VDM models, but in most programming languages, think for example about segmentation faults and NullPointerExceptions).

To ensure a run-time-error free execution of the model, the model has to be proved to be inconsistency-free (consistent). As manual proof is usually not the most favorite task to be performed, automatic proof is the goal of this project.

Main pages associated with this project:

• Downloads
• System Description A high-level description
• Usage Description How to set up and use the current implementation
• Case Studies Case studies used during development
• Open Issues

An extensive description of the project can be found in my MSc thesis.

Used technologies

Except for other Overture tools, this project makes use of:

• HOL4 (Higher Order Logic v4)
• VDMTools (specifically the integrity examiner and during developement the IDE)

Limitations

Currently, not all model are supported. The applicability of the tool has been restricted to a subset of OML, but should in the future support the entire language. The main restrictions are:

• Functional subset Only the functional subset is supported. Therefore, operations and operational language constructs (such as loops) are not supported.
• Mutual recursive dependencies As HOL does not easily allow for forward declarations, or a similar mechanism, mutual recursive dependencies are currently not an option.
• Disjoint type unions HOL does not allow type union of non-disjoint types and therefore only disjoint type unions are supported.

Contact

If you have any questions about the project or associated software, or would like to contribute to the project, please contact Sander Vermolen.

-- SanderVermolen - 17 Jan 2008