Backward protocol verification method

Chung-Ming Huang, Duen Tay Huang

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

1 Citation (Scopus)

Abstract

Using the formal Communication Finite State Machine (CFSM) model, a communication protocol consists of several communicating entities which can be represented in some CFSMs. Global state reachability analysis is one of the most straightforward ways to automatically detect logical errors in a communication protocol specified in the CFSM model. Global state reachability analysis generates all of the reachable global states and checks the correctness one by one. Even though communication protocols are error free, global state reachability analysis still needs to be executed completely. In this paper, we propose a new verification method, which is called the backward protocol verification method, to detect logical errors. By analyzing the properties of deadlock error, unspecified reception error, and channel overflow error, some candidate erroneous global states are generated. Then, each candidate global state is checked whether there is a path, i.e., a global state sequence, connects to the original initial global state. If there is a path, then the candidate global state is really an erroneous global state and the communication protocol does have some logical errors. Otherwise, if there is no candidate global state or none of the candidate global state has a path, then the communication protocol is error free.

Original languageEnglish
Title of host publicationProceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering
PublisherPubl by IEEE
Pages515-518
Number of pages4
ISBN (Print)0780312333
Publication statusPublished - 1993
EventProceedings of the 1993 IEEE Region 10 Conference on Computer, Communication, Control and Power Engineering (TENCON '93). Part 1 (of 5) - Beijing, China
Duration: 1993 Oct 191993 Oct 21

Other

OtherProceedings of the 1993 IEEE Region 10 Conference on Computer, Communication, Control and Power Engineering (TENCON '93). Part 1 (of 5)
CityBeijing, China
Period93-10-1993-10-21

Fingerprint

Network protocols
Finite automata
Communication

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Cite this

Huang, C-M., & Huang, D. T. (1993). Backward protocol verification method. In Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering (pp. 515-518). Publ by IEEE.
Huang, Chung-Ming ; Huang, Duen Tay. / Backward protocol verification method. Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering. Publ by IEEE, 1993. pp. 515-518
@inproceedings{865e54fdb06c4325bed4cc997cd94ba5,
title = "Backward protocol verification method",
abstract = "Using the formal Communication Finite State Machine (CFSM) model, a communication protocol consists of several communicating entities which can be represented in some CFSMs. Global state reachability analysis is one of the most straightforward ways to automatically detect logical errors in a communication protocol specified in the CFSM model. Global state reachability analysis generates all of the reachable global states and checks the correctness one by one. Even though communication protocols are error free, global state reachability analysis still needs to be executed completely. In this paper, we propose a new verification method, which is called the backward protocol verification method, to detect logical errors. By analyzing the properties of deadlock error, unspecified reception error, and channel overflow error, some candidate erroneous global states are generated. Then, each candidate global state is checked whether there is a path, i.e., a global state sequence, connects to the original initial global state. If there is a path, then the candidate global state is really an erroneous global state and the communication protocol does have some logical errors. Otherwise, if there is no candidate global state or none of the candidate global state has a path, then the communication protocol is error free.",
author = "Chung-Ming Huang and Huang, {Duen Tay}",
year = "1993",
language = "English",
isbn = "0780312333",
pages = "515--518",
booktitle = "Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering",
publisher = "Publ by IEEE",

}

Huang, C-M & Huang, DT 1993, Backward protocol verification method. in Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering. Publ by IEEE, pp. 515-518, Proceedings of the 1993 IEEE Region 10 Conference on Computer, Communication, Control and Power Engineering (TENCON '93). Part 1 (of 5), Beijing, China, 93-10-19.

Backward protocol verification method. / Huang, Chung-Ming; Huang, Duen Tay.

Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering. Publ by IEEE, 1993. p. 515-518.

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

TY - GEN

T1 - Backward protocol verification method

AU - Huang, Chung-Ming

AU - Huang, Duen Tay

PY - 1993

Y1 - 1993

N2 - Using the formal Communication Finite State Machine (CFSM) model, a communication protocol consists of several communicating entities which can be represented in some CFSMs. Global state reachability analysis is one of the most straightforward ways to automatically detect logical errors in a communication protocol specified in the CFSM model. Global state reachability analysis generates all of the reachable global states and checks the correctness one by one. Even though communication protocols are error free, global state reachability analysis still needs to be executed completely. In this paper, we propose a new verification method, which is called the backward protocol verification method, to detect logical errors. By analyzing the properties of deadlock error, unspecified reception error, and channel overflow error, some candidate erroneous global states are generated. Then, each candidate global state is checked whether there is a path, i.e., a global state sequence, connects to the original initial global state. If there is a path, then the candidate global state is really an erroneous global state and the communication protocol does have some logical errors. Otherwise, if there is no candidate global state or none of the candidate global state has a path, then the communication protocol is error free.

AB - Using the formal Communication Finite State Machine (CFSM) model, a communication protocol consists of several communicating entities which can be represented in some CFSMs. Global state reachability analysis is one of the most straightforward ways to automatically detect logical errors in a communication protocol specified in the CFSM model. Global state reachability analysis generates all of the reachable global states and checks the correctness one by one. Even though communication protocols are error free, global state reachability analysis still needs to be executed completely. In this paper, we propose a new verification method, which is called the backward protocol verification method, to detect logical errors. By analyzing the properties of deadlock error, unspecified reception error, and channel overflow error, some candidate erroneous global states are generated. Then, each candidate global state is checked whether there is a path, i.e., a global state sequence, connects to the original initial global state. If there is a path, then the candidate global state is really an erroneous global state and the communication protocol does have some logical errors. Otherwise, if there is no candidate global state or none of the candidate global state has a path, then the communication protocol is error free.

UR - http://www.scopus.com/inward/record.url?scp=0027816335&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0027816335&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0027816335

SN - 0780312333

SP - 515

EP - 518

BT - Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering

PB - Publ by IEEE

ER -

Huang C-M, Huang DT. Backward protocol verification method. In Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering. Publ by IEEE. 1993. p. 515-518