Search: onr:"swepub:oai:DiVA.org:uu-411671" >
Formal specificatio...
Formal specification and validation of a cache-coherence protocol
-
- Eriksson, Lars-Henrik (author)
- RISE,SICS,RISE - Research Institutes of Sweden, SICS
-
- Orava, Fredrik (author)
- RISE,SICS,RISE - Research Institutes of Sweden, SICS
-
(creator_code:org_t)
- 1
- Swedish Institute of Computer Science, 1995
- English.
-
Series: SICS Research Report, 0283-3638 ; R95:04
- Related links:
-
https://urn.kb.se/re...
-
show more...
-
https://urn.kb.se/re...
-
show less...
Abstract
Subject headings
Close
- We specify a cache coherence protocol for cache-only shared memory multiprocessor architectures using the $\pi$-calculus. The analysis of the specification of the protocol is discussed, with emphasis on the use of the modal $\mu$-calculus to express correctness properties. The protocol specification is expressed using recursion variables inside parallel composition and thus it does not adhere to the syntactic requirements for finite control. We argue that the specification still belongs to a class of $\pi$-calculus processes for which model checking and bisimilarity checking is decidable. The relaxation of the syntactical requirement for finite control permits more natural specifications to be made. We expect that specifications which are naturally expressed using recursion variables inside parallel compositions but still permit decidable analyses are common in practise.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Keyword
- Process algebra
- p-calculus
- µ-calculus
- specification
- automatic verification
- model checking
- cache-coherence protocol
- Computing Science
- Datalogi
Publication and Content Type
- vet (subject category)
- rap (subject category)
To the university's database