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

Direktlänk
Referera
Referensformat
  • apa
  • 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
Compositional specification and verification of distributed systems
RISE., Swedish ICT, SICS.
1990 (Engelska)Rapport (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
Swedish Institute of Computer Science , 1990, 1. , s. 49
Serie
SICS Research Report, ISSN 0283-3638 ; R90:10
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
URN: urn:nbn:se:ri:diva-21341OAI: oai:DiVA.org:ri-21341DiVA, id: diva2:1041375
Anmärkning

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.

Tillgänglig från: 2016-10-31 Skapad: 2016-10-31 Senast uppdaterad: 2020-12-02Bibliografiskt 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: 22 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • 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