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/28922
Record Status
Checked
Record Id
28922
Title
On the Verification of VDM Specification and Refinement with PVS
Contributors
S Maharaj
,
J Bicarregui
Abstract
Although the formal method VDM has been in existence since the 1970's, there are still no satisfactory tools to support verification in VDM. This paper deals with one possible means of approaching this problem by using the PVS theorem-prover. It describes a translation of a VDM-SL specification into the PVS specification language using, essentially, the very transparent translation methods described in [1]. PVS was used to typecheck the specification and to prove some non-trivial validation conditions. Next, a more abstract specification of the same system was also expressed in PVS, and the original specification was shown to be a refinement of this one. 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.
Organisation
CCLRC
,
BITD
Keywords
Funding Information
Related Research Object(s):
Licence Information:
Language
English (EN)
Type
Details
URI(s)
Local file(s)
Year
Paper In Conference Proceedings
In ASE'97, 12th IEEE International Conference on Automated Software Engineering, , Lake Tahoe , Date 1-5 Nov. 1997 , (1997).
https://doi.org/10.1109/ASE.1997.632849
1997
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