The RPC-Memory Specification Problem has been specified and verified in an assertional method, supported by the verification system PVS. 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, to increase the confidence in the specification, an implementation-oriented specification of the inner memory is shown to be equivalent to our original property-oriented formulation.
|Title of host publication||Formal Systems Specification: The RPC-Memory Specification Case Study|
|Editors||M. Broy, S. Merz, K. Spies|
|Place of Publication||Berlin|
|Publication status||Published - 1996|
|Name||Lecture Notes in Computer Science|