Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Compositional specification and verification of distributed systems
Number of Authors: 1
1990 (English)Report (Refereed)
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.

Place, publisher, year, edition, pages
Swedish Institute of Computer Science , 1990, 1. , 49 p.
Series
SICS Research Report, ISSN 0283-3638 ; R90:10
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:ri:diva-21341OAI: oai:DiVA.org:ri-21341DiVA: diva2:1041375
Note
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.Available from: 2016-10-31 Created: 2016-10-31Bibliographically approved

Open Access in DiVA

No full text

Other links

fulltext
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
v. 2.26.0