ePubs
The open archive for STFC research publications
Home
About ePubs
Content Policies
News
Help
Privacy/Cookies
Suggest an Enhancement
Contact ePubs
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
Contributors
S Agerholm
,
JC Bicarregui
,
S Maharaj
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
Keywords
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
Showing record 1 of 1
Recent Additions
Browse Organisations
Browse Journals/Series
Login to add & manage publications and access information for OA publishing
Username:
Password:
Useful Links
Chadwick & RAL Libraries
SHERPA FACT
SHERPA RoMEO
SHERPA JULIET
Journal Checker Tool
Google Scholar