从Petri网到形式描述技术和协议工程
作者:
基金项目:

本文研究得到国家自然科学基金(No.69873009)和国家973信息技术与高性能软件项目基金(No.G1998030405)资助.


From Petri Nets to Formal Description Techniques and Protocol Engineering
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [1]
  • |
  • 相似文献 [20]
  • |
  • 引证文献
  • | |
  • 文章评论
    摘要:

    协议是计算机网络的命脉,协议复杂性的提高导致了协议工程学科的出现.该文首先分析了协议工程各项活动的内容、方法和相互关系,讨论了各种形式描述技术(formal description technique,简称FDT)的特性及其优缺点,从而引出基于Petri网理论的FDT.该文说明了Petri网作为协议描述技术的优势,指出当前基于Petri网的协议工程研究的难点,其中面向协议开发的网工具是一项重要的研究内容.按照开放系统互连参考模型的层次,总结了国际上的研究进展情况,并阐述了未来的研究趋势.最后从协议描述、协议验证与分析以及辅助测试与实现这3个角度给出了基于Petri网的协议工程的基本方法.

    Abstract:

    Protocol is the lifeline of computer network. The rapid increasing of protocol complexity results in a discipline of protocol engineering. Based on an analysis of the contents and methods of protocol engineering activities and their interrelations, first discusses main formal description techniques (FDTs) and their characteristics, compares corresponding strongpoints and weaknesses, and then leads to Petri nets based FDT. Secondly, the paper points out special advantages of the Petri nets based formal techniques and the current research difficulties in Petri nets based protocol engineering, among which protocol development oriented net tools are now very important research tasks. Thirdly, the paper summarizes international research advances in terms of OSI/RM layers and expounds research trends in this area. Finally, the authors give fundamental methodologies for Petri nets based protocol engineering in protocol specification, verification and analysis, and computer-aided testing and implementation.

    参考文献
    1  Gu Guan-qun, Gong Jian. Computer Network. Nanjing: Jiangsu Science and Technology Press, 1989 (顾冠群,龚俭.计算机网络.南京:江苏科学技术出版社,1989)  2  Rudin H. Protocol engineering: a critical assessment. In: Aggarwal S ed. Protocol Specification, Testing and Verification (ⅤⅠⅠⅠ). Amsterdam: North-Holland, 1988. 3~16  3  Jonsson B et al. Protocol Specification, Testing, and Verification (ⅩⅠ). Amsterdam: North-Holland, 1991  4  Linn R J et al. Protocol Specification, Testing, and Verification (ⅩⅠⅠ). Amsterdam: North-Holland, 1992  5  Aggarwal S et al. Protocol Specification, Testing, and Verification (ⅤⅠⅠⅠ). Amsterdam: North-Holland, 1988  6  Wheeler G R, Batten T J, Billington J et al. A methodology for protocol engineering. In: New Communication Services: A Challenge to Computer Technology. Amsterdam: North-Holland, 1986. 525~530  7  Cheung To-yat. Petri nets for protocol engineering. Computer Communications, 1996,19:1250~1257  8  Diaz M. Petri net based models in the specification and verification of protocols. In: Brauer W ed. Petri Nets: Applications and Relationships to other Models of Concurrency. LNCS 255, Berlin: Springer-Verlag, 1988. 135~170  9  Brauer W et al. Petri nets: applications and relationships to other models of concurrency. LNCS 255, Berlin: Springer-Verlag, 1988  10  Billington J. Protocol engineering and nets. In: Proceedings of the 8th European Workshop on Application and Theory of Petri Nets. Zaragoza, 1987. 137~156  11  Berthelot G, Terrat R. Petri nets theory for the connection of protocols. IEEE Transactions on Communications, 1982,30(12):2497~2505  12  Billington J. Specification of the transport service using numerical Petri nets. In: Sunshine C ed. Protocol Specification, Testing, and Verification. Amsterdam: North-Holland, 1982. 77~100  13  Diaz M et al. From multimedia models to multimedia transport protocols. Computer Networks and ISDN Systems, 1997,29:745~758  14  Feldbrugge F, Jensen K. Petri net tool overview 1986. In: Brauer W ed. Petri Nets: Applications and Relationships to other Models of Concurrency. LNCS 255, Berlin: Springer-Verlag, 1988. 20~61  15  Luo Jun-zhou, Gu Guan-qun, Xie Jun-qing. Petri net based protocol analyzer. Chinese Journal of Computers, 1997,20(3):206~212 (罗军舟,顾冠群,谢俊清.Petri网协议分析器.计算机学报,1997,20(3):206~212)  16  Watanabe T. Protocol verification tool with extended Petri nets and horn cluse. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, 1995,E78-A(11):1458~1467  17  Gu Guan-qun, Luo Jun-zhou. EPr/TN net system and the formal description technique of network protocols. Chinese Journal of Computers, 1994,17(supplement):93~96 (顾冠群,罗军舟.EPr/TN网系统及网络协议形式描述技术.计算机学报,1994,17(增刊):93~96)  18  Shen Jun, Luo Jun-zhou, Gu Guan-qun. Redundant concurrentable successor markings in reachability analysis of EPr/TN net. Computer Research and Development, 1988,35(3):251~254 (沈俊,罗军舟,顾冠群.EPr/TN网可达性分析的冗余并发后继标识.计算机研究与发展,1998,35(3):251~254)  19  Kelling C et al. Modeling priorities in token protocols with timed petri nets. International Journal of Mini and Microcomputers, 1995,17(1):35~41  20  Bettaz M et al. On reusing ATNet modules in protocol specification. Journal of System and Software, 1994,27(2):119~128  21  Souissi Y. Towards a modular specification and verification of protocols within layered architecture. IFIP Transactions on C: Communication System, 1994,C-22:35~50  22  Lee Jong-kun, Lee Kwuang-hui. Modeling of the multicast transport protocols using petri nets. In: Proceedings of IEEE Singapore International Conference on Network/International Conference on Information Engineering. 1995. 106~110  23  Hui J Y et al. Client-Server synchronization and buffering for variable rate multimedia retrievals. IEEE Journal on Selected Areas in Communications, 1996,14(1):226~237  24  Basyouni A M. New approach to cryptographic protocol analysis using colored Petri nets. In: Proceedings of the Canadian Conference on Electrical and Computer Engineering. 1997. 25~28  25  Lee Gang-Soo et al. Petri net based models for specification and analysis of cryptographic protocols. Journal of Systems and Software, 1997,37(2):141~159  26  Luo Jun-zhou, Shen Jun, Gu Guan-qun. Synchro-Net system: a Petri net model for high-layer protocols. Journal of Software, 1997,8(supplement),202~210 (罗军舟,沈俊,顾冠群.适合于网络高层协议描述的同步EPr/TN网.软件学报,1997,8(增刊):202~210)  27  Jirachiefpattana A. Estelle-NPN based system for protocol verification. In: COMPASS-Proceedings of the Annual Conference on Computer Assurance. 1995. 25~29
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

罗军舟,沈俊,顾冠群.从Petri网到形式描述技术和协议工程.软件学报,2000,11(5):606-615

复制
分享
文章指标
  • 点击次数:6440
  • 下载次数: 7316
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:1999-06-10
  • 最后修改日期:1999-12-06
文章二维码
您是第19783646位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号