Approach to verification of communication in distributed computing system software

Sik-Sang Yau, Kris W I Chen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

An approach is presented for verifying the communication among modules in distributed computing system software. This approach is based on the inductive assertion method. The inference rules used in this approach are derived for verifying the partial correctness of communicating sequential modules. In this approach, the virtual circuits are used for synchronous message-passing. The advantage of this approach is that proofs of the satisfaction and noninterference are not needed, since no assumptions about the effects of receiving messages are made in the sequential proofs and the uses of shared auxiliary variables and universal assertions are carefully controlled during the process verification. Without these proofs, the user only needs to deal with the individual modules instead of the entire distributed computing system. The technique for detecting the deadlock of a program is given.

Original languageEnglish (US)
Title of host publicationProceedings - International Conference on Distributed Computing Systems
Editors Anon
Place of PublicationPiscataway, NJ, United States
PublisherPubl by IEEE
Pages603-610
Number of pages8
StatePublished - Jun 1989
Externally publishedYes
Event9th International Conference on Distributed Computing Systems - Newport Beach, CA, USA
Duration: Jun 5 1989Jun 9 1989

Other

Other9th International Conference on Distributed Computing Systems
CityNewport Beach, CA, USA
Period6/5/896/9/89

ASJC Scopus subject areas

  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Approach to verification of communication in distributed computing system software'. Together they form a unique fingerprint.

Cite this