The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/28931
Record Status Checked
Record Id 28931
Title On the Verification of VDM Specification and Refinement with PVS
Abstract This chapter describes using the PVS system as a tool to support VDMð SL. 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.
Organisation CCLRC , BITD
Funding Information
Related Research Object(s):
Licence Information:
Language English (EN)
Type Details URI(s) Local file(s) Year
Book Chapter or Section In Proof in VDM: a practioner's guide . by Bicarregui, J.C., Fitzgerald, J., Lindsay, P.A., Moore, R., Ritchie, B. , chapter 6, 157-190. Springer, 1998. http://www.resear…0cf2d8daaacb0ffa.pdf 1998