Verification of distributed real-time and fault-tolerant protocols

J.J.M. Hooman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)

Abstract

An assertional method to verify distributed real-time and fault-tolerant protocols is presented. To obtain mechanical support, the verification system PVS is used. General PVS theories are developed to deal with timing and failures. As a characteristic example, we verify a processor-group membership protocol, dealing with a dynamically changing network of processors and reasoning in terms of local clocks. Further we show some basic theories for the verification of the underlying synchronous atomic broadcast service.
Original languageEnglish
Title of host publicationAlgebraic Methodology and Software Technology (Proceedings 6th International Conference, AMAST'97, Sydney, Australia, December 13-17, 1997)
EditorsM. Johnson
PublisherSpringer
Pages261-275
ISBN (Print)3-540-63888-1
DOIs
Publication statusPublished - 1997

Publication series

NameLecture Notes in Computer Science
Volume1349
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Verification of distributed real-time and fault-tolerant protocols'. Together they form a unique fingerprint.

Cite this