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.
ABSTRACT
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.
Postscript