Abstract:

In summer 1996, while visiting the Rutherford Appleton Laboratory in England, I hand-translated some medium sized VDM specifications into the PVS language and used the PVS prover to verify some properties of these specifications. The VDM specifications relate to the MSMIE[1] (Multiprocessor Shared-Memory Information Exchance) protocal which was designed for use in nuclear safety systems at Westinghouse, and specified in VDM by Juan Bicarregui at RAL[2].

This exercise showed that it is fairly straightforward to translate a large fragment of VDM into PVS. The methods used are essentially those described by Agerholm[3]. The translation may be done in such a way that some VDM proof obligations are generated automatically as TCCs in PVS. However the translation is only superficial --- differences between the two logics mean that the semantics of VDM is not preserved. The translation may be extended to deal with refinement between specifications, at least in a superficial way, but the differences between the two logics mean that the VDM notion of refinement is not correctly captured.

Conclusions about the PVS system: it is relatively easy to learn to use, and quite fast at doing proofs, and it has a very useful and expressive specification language. However there are concerns about the lack of independently checkable proof objects, the difficulty of understanding the behaviour of the powerful tactics provided by the system, and the presence of bugs in the current implementation.