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

All Science Journal Classification (ASJC) codes

  • 工程 (全部)

指紋

深入研究「Backward protocol verification method」主題。共同形成了獨特的指紋。

引用此