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 language | English (US) |
|---|---|
| Title of host publication | Proceedings - International Conference on Distributed Computing Systems |
| Editors | Anon |
| Place of Publication | Piscataway, NJ, United States |
| Publisher | Publ by IEEE |
| Pages | 603-610 |
| Number of pages | 8 |
| State | Published - Jun 1989 |
| Externally published | Yes |
| Event | 9th International Conference on Distributed Computing Systems - Newport Beach, CA, USA Duration: Jun 5 1989 → Jun 9 1989 |
Other
| Other | 9th International Conference on Distributed Computing Systems |
|---|---|
| City | Newport Beach, CA, USA |
| Period | 6/5/89 → 6/9/89 |
ASJC Scopus subject areas
- Hardware and Architecture