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
On the Verification of Open Distributed Systems
RISE - Research Institutes of Sweden, ICT, SICS.
RISE - Research Institutes of Sweden, ICT, SICS.
1997 (English)Report (Other academic)
Abstract [en]

A logic and proof system is introduced for specifying and proving properties of open distributed systems. Key problems that are addressed include the verification of process networks with a changing interconnection structure, and where new processes can be continuously spawned. To demonstrate the results in a realistic setting we consider a core fragment of the Erlang programming language. Roughly this amounts to a first-order actor language with data types, buffered asynchronous communication, and dynamic process spawning. Our aim is to verify quite general properties of programs in this fragment. The specification logic extends the first-order $\mu$-calculus with Erlang-specific primitives. For verification we use an approach which combines local model checking with facilities for compositional verification. We give a specification and verification example based on a billing agent which controls and charges for user access to a given resource.

Place, publisher, year, edition, pages
Swedish Institute of Computer Science , 1997, 1. , p. 16
Series
SICS Research Report, ISSN 0283-3638 ; R97:01
Keywords [en]
Open Distributed Systems, Program Verification, Erlang, Parametric Verification, Agents
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:ri:diva-21412OAI: oai:DiVA.org:ri-21412DiVA, id: diva2:1041448
Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2018-02-02Bibliographically approved

Open Access in DiVA

fulltext(2083 kB)2 downloads
File information
File name FULLTEXT01.pdfFile size 2083 kBChecksum SHA-512
828186ad0e859d7eac371830bcc990c2217492d01d00296e3d227061d7249e46a7be6f0c463cdba8b39674b47c45abfdacefcee67ea81a3e3c2696b4884c3ca1
Type fulltextMimetype application/pdf

By organisation
SICS
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 2 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 26 hits
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.34.0