Using PVS for an assertional verification of the RPC-memory specification problem

J.J.M. Hooman

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureHoofdstukAcademicpeer review

Samenvatting

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.
Originele taal-2Engels
TitelFormal Systems Specification: The RPC-Memory Specification Case Study
RedacteurenM. Broy, S. Merz, K. Spies
Plaats van productieBerlin
UitgeverijSpringer
Pagina's275-304
ISBN van geprinte versie3-540-61984-4
DOI's
StatusGepubliceerd - 1996

Publicatie series

NaamLecture Notes in Computer Science
Volume1169
ISSN van geprinte versie0302-9743

Vingerafdruk Duik in de onderzoeksthema's van 'Using PVS for an assertional verification of the RPC-memory specification problem'. Samen vormen ze een unieke vingerafdruk.

Citeer dit