| A VERIFICATION METHOD FOR COMMUNICATION PROTOCOLS MODELED AS COMMUNICATING EXTENDED FINITE─STATE MAC |
| |
| 作者姓名： | Shao Fengjing\ Sun Xiaorui\ Liu Zunren |
| |
| 作者单位： | Department of Computer，Qingdao University，Qingdao 266071 |
| |
| 摘 要： | 本文建立了用于表述含有无限值状态成分的通讯协议机的抽象模型，给出了基于该模型的形式检证法，试制了检证系统．该检证法不需要假定信道的有界性．对于给定的通信协议，检证系统将判定其对指定状态的可到达性．做为检证例，从ＯＳＩ参照模型中抽出了大同步点设置功能单位，就“无死锁”、“无传输错误”等性质进行了实际检证
|
| 关 键 词： | 协议 检证 信道有界性 寄存器 |
A VERIFICATION METHOD FOR COMMUNICATION PROTOCOLS MODELED AS COMMUNICATING EXTENDED FINITE STATE MACHINES |
| |
| Shao Fengjing\ Sun Xiaorui\ Liu Zunren.A VERIFICATION METHOD FOR COMMUNICATION PROTOCOLS MODELED AS COMMUNICATING EXTENDED FINITE STATE MACHINES[J].Journal of Qingdao University(Natural Science Edition),1996(3). |
| |
| Authors: | Shao Fengjing\ Sun Xiaorui\ Liu Zunren |
| |
| Abstract: | This paper presents a mehtod for verifying eventuality properties of protocols in which protocol machines have not only finite controllers but also registers whose contents are integers. A protocol is modeled as a conditional 2CEFSM S which consists of two protocol machines with two channels connecting them and a substitute function. The protocol machine is modeled as an extended finite state machine and the channel is modeled as an unbounded FIFO queue. A verification system based on our method has been implemented. To confirm the effectiveness of our verification method, for a part of the OSI session protocol, we verified that neither protocol error nor deadlock occurs unless a transmission error occurs. |
| |
| Keywords: | protocol verification boundedness register |
| 本文献已被 CNKI 等数据库收录！ |
