On the Verification of VDM Specification and Refinement with PVS

Citation

Agerholm S, Bicarregui J & Maharaj S (1998) On the Verification of VDM Specification and Refinement with PVS. In: Bicarregui J (ed.) Proof in VDM: Case Studies. Formal Approaches to Computing and Information Technology (FACIT). London: Springer, pp. 157-189. http://link.springer.com/chapter/10.1007/978-1-4471-1532-8_6#

Abstract
This chapter describes using the PVS system as a tool to support VDMSL. It is possible to translate from VDM-SL into the PVS specification language in a very easy and direct manner, thus enabling the use of PVS for typechecking and verifying properties of VDM-SL specifications and refinements. The translation is described in detail and illustrated with examples. The drawbacks of the translation are that it must be done manually (though automation may be possible), and that the "shallow embedding" technique which is used does not accurately capture the proof rules of VDM-SL. The benefits come from the facts that the portion of VDM-SL which can be represented is substantial and that it is a great advantage to be able to use the powerful PVS proof-checker. A variety of examples of verifications using PVS are described in the chapter.