Using PVS for an Assertional Verification of the RPC-Memory Specification Problem

Jozef Hooman

Appeared in: Formal Systems Specification; The RPC-Memory Specification Case Study, LNCS 1169, Springer-Verlag, pages 275-304, 1996.


The RPC-Memory Specification Problem has been specified and verified in an assertional method, supported by the verification system PVS (Prototype Verification System). Properties of the components are expressed in the higher-order logic of PVS and all implementations have been verified by means of the interactive proof checker of PVS. A simplification of the memory specification - allowing multiple atomic reads - has been proved correct. Additionally, an implementation-oriented specification of the inner memory is shown to be equivalent to our original property-oriented formulation.