Backward protocol verification method

Chung-Ming Huang, Duen Tay Huang

研究成果: Conference contribution

1 引文 (Scopus)

摘要

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.

原文English
主出版物標題Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering
發行者Publ by IEEE
頁面515-518
頁數4
ISBN(列印)0780312333
出版狀態Published - 1993
事件Proceedings of the 1993 IEEE Region 10 Conference on Computer, Communication, Control and Power Engineering (TENCON '93). Part 1 (of 5) - Beijing, China
持續時間: 1993 十月 191993 十月 21

Other

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

指紋

Network protocols
Finite automata
Communication

All Science Journal Classification (ASJC) codes

  • Engineering(all)

引用此文

Huang, C-M., & Huang, D. T. (1993). Backward protocol verification method. 於 Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering (頁 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. 頁 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. 於 Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering. Publ by IEEE, 頁 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.

研究成果: Conference 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. 於 Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering. Publ by IEEE. 1993. p. 515-518