Open Collections

UBC Theses and Dissertations

UBC Theses Logo
Featured Collection

UBC Theses and Dissertations

Total correctness of an ISO transport protocol subset Jürgensen, Wolfgang

Abstract

In this thesis, a new Petri net based model called CSP nets is proposed to specify the control state aspects of a communication protocol. This model is combined with a CSP programming language specification to produce a formal model of a significant subset of the ISO transport protocol. The two compatible models are validated. The CSP programming language specification is checked for partial correctness and system safety and liveness using assertion proofs and temporal logic. A satisfaction proof is provided, too. The CSP net specification, checked by an automatic validation tool called "cspnet" contains no deadlock and is cyclic. The combined validation results show our ISO transport protocol specification to be totally correct. This thesis argues that a communication protocol should be specified using a combined programming language and state transition model to produce a rigorous and complete proof of its correctness.

Item Metadata

Title
Total correctness of an ISO transport protocol subset
Creator
Jürgensen, Wolfgang
Publisher
University of British Columbia
Date Issued
1984
Description
In this thesis, a new Petri net based model called CSP nets is proposed to specify the control state aspects of a communication protocol. This model is combined with a CSP programming language specification to produce a formal model of a significant subset of the ISO transport protocol. The two compatible models are validated. The CSP programming language specification is checked for partial correctness and system safety and liveness using assertion proofs and temporal logic. A satisfaction proof is provided, too. The CSP net specification, checked by an automatic validation tool called "cspnet" contains no deadlock and is cyclic. The combined validation results show our ISO transport protocol specification to be totally correct. This thesis argues that a communication protocol should be specified using a combined programming language and state transition model to produce a rigorous and complete proof of its correctness.
Genre
Thesis/Dissertation
Type
Text
Language
eng
Date Available
2010-05-15
Provider
Vancouver : University of British Columbia Library
Rights
For 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.
DOI
10.14288/1.0051864
URI
http://hdl.handle.net/2429/24707
Degree
Master of Science - MSc
Program
Computer Science
Affiliation
Science, Faculty of; Computer Science, Department of
Degree Grantor
University of British Columbia
Campus
UBCV
Scholarly Level
Graduate
Aggregated Source Repository
DSpace

Item Media

Item Citations and Data

Rights

For 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.