Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Formal specification and validation of a cache-coherence protocol
RISE - Research Institutes of Sweden, IKT, SICS.
RISE - Research Institutes of Sweden, IKT, SICS.
1995 (Engelska)Rapport (Övrigt vetenskapligt)
Abstract [en]

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.

Ort, förlag, år, upplaga, sidor
Swedish Institute of Computer Science , 1995, 1.
Serie
SICS Research Report, ISSN 0283-3638 ; R95:04
Nyckelord [en]
Process algebra, p-calculus, µ-calculus, specification, automatic verification, model checking, cache-coherence protocol
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
URN: urn:nbn:se:ri:diva-22156OAI: oai:DiVA.org:ri-22156DiVA, id: diva2:1041699
Tillgänglig från: 2016-10-31 Skapad: 2016-10-31 Senast uppdaterad: 2018-01-14Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Av organisationen
SICS
Data- och informationsvetenskap

Sök vidare utanför DiVA

GoogleGoogle Scholar

urn-nbn

Altmetricpoäng

urn-nbn
Totalt: 6 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
v. 2.35.7