Return to search

Specification-verification of protocols : the significant event temporal logic technique

This thesis addresses the problem of protocol verification. We first present a brief review of the existing specification methods for communication protocols, with emphasis on the hybrid techniques. The alternating bit protocol is specified in ISO/FDT, BBN/FST and UNISPEX to provide a comparison between three interesting hybrid models of protocol specification. A method for applying the unbounded state Temporal Logic to verify a protocol specified in a hybrid technique (in particular FDT) is outlined. Finally, a new specification and verification method called SETL is proposed, which is based on event sequences and temporal logic. To illustrate the method two data transfer protocols namely, the stop-wait and alternating bit protocols are specified in SETL and verified. We demonstrate that SETL is a generalization of the hybrid techniques, it is sound and that it can be semi-automated. / Science, Faculty of / Computer Science, Department of / Graduate

Identiferoai:union.ndltd.org:UBC/oai:circle.library.ubc.ca:2429/25047
Date January 1985
CreatorsTsiknis, George
PublisherUniversity of British Columbia
Source SetsUniversity of British Columbia
LanguageEnglish
Detected LanguageEnglish
TypeText, Thesis/Dissertation
RightsFor non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.

Page generated in 0.0016 seconds