Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Compositional specification and verification of distributed systems
RISE., Swedish ICT, SICS.
1990 (engelsk)Rapport (Fagfellevurdert)
Abstract [en]

We present a method for specification and verification of distributed systems that communicate via asynchronous message-passing. The method handles both safety and liveness properties. It is compositional, i.e., a specification of a composite system can be obtained from specifications of its components. Specifications are given as labeled transition systems with fairness properties, using a program-like notation with guarded multiple assignments. A specification denotes a set of allowed sequences of message transmissions and receptions, in analogy with the way finite automata are used as acceptors of finite strings. A lower-level specification implements a higher-level specification if all sequences allowed by the lower-level specification are also allowed by the higher-level one. We present a verification technique which reduces the problem of verifying the correctness of an implementation to classical verification conditions. Safety properties are verified by establishing a simulation between transition systems. Liveness properties are verified using methods for proving termination under fairness assumptions. Since specifications can be given at various levels of abstraction, the method is suitable in a development process where a detailed implementation is developed from an abstract specification through a sequence of refinement steps. The method is applied to a sliding window protocol, and to an algorithm by Thomas for updating a distributed database.

sted, utgiver, år, opplag, sider
Swedish Institute of Computer Science , 1990, 1. , s. 49
Serie
SICS Research Report, ISSN 0283-3638 ; R90:10
HSV kategori
Identifikatorer
URN: urn:nbn:se:ri:diva-21341OAI: oai:DiVA.org:ri-21341DiVA, id: diva2:1041375
Merknad

Original report number R90010. A revised and extended version of a paper that has appeared under the titel "Modular Verification oh Asynchronous Networks" in the Proceedings of the 6th Annual ACM Symposium of Principles of Distributed Computing, Vancouver, Canada, August 1987.

Tilgjengelig fra: 2016-10-31 Laget: 2016-10-31 Sist oppdatert: 2020-12-02bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric

urn-nbn
Totalt: 22 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
v. 2.43.0