Verification of a multiprocessor cache protocol using simulation relations and higher-order logic

Autor:	Paul N. Loewenstein, David L. Dill
Rok vydání:	1992
Předmět:	Theoretical computer science Correctness Finite-state machine CPU cache Computer science HOL Higher-order logic Theoretical Computer Science TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Hardware and Architecture Cache Protocol (object-oriented programming) Formal verification Software
Zdroj:	CAV (DIMACS/AMS volume)
ISSN:	1572-8102 0925-9856
DOI:	10.1007/bf00709156
Popis:	We present a formal verification method for concurrent systems. The technique is to show a correspondence between state machines representing an implementation and specification behaviour. The correspondence is called a simulation relation, and is particularly well-suited for theorem-provers. Since the method does not rely on enumerating all the states, it can be applied to systems with an infinite or unknown number of states. This substantially expands the class of hardware designs that can be formally verified. The method is illustrated by proving the correctness of a particularly subtle example which is likely to be of increasing importance: a directory-based multiprocessor cache protocol. The proof is carried out using the HOL (“higher-order logic”) theorem-prover.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::669ace6c6f13b41ea56c5b891dbe681b https://doi.org/10.1007/bf00709156 Zobrazit plný text záznamu Full text from SpringerLink