PDA系统通信协议研究与实现
摘要
本论文结合一个PDA项目的开发，设计和实现了利用固定电话网进行信息传输的一套通信协议。
基于通信协议开发的一般过程——协议工程，同时针对于本项目的特点，本文首先分析了协议工程的缺陷，对协议工程的各项活动提出了适当的修改和裁减建议。
文章重点探讨了，如何依据修改的协议工程活动来指导通信协议的开发：在体系结构上，应用并描述C/S模式的网络架构，及其相比于交叉式的网络构架的优势所在。对比ISO七层模型，设计了简单实用的三层网络模型(物理层，链路层，消息层)。在通用的时序图描述通信协议动态交互的基础上，用一种形式化描述技术——Petri网抽象通信协议的动态行为规范为一种链路层半双工停止-等待协议，从简单到复杂建立4个不同侧重点的Petri网模型，分别描述通信协议的不同动态行为：交互，超时，出错处理。提出了对于Petri网通信模型的信道约束条件公式：∑m_t≤1。利用Petri网理论对协议进行一致性验证，并修正验证时所发现的错误。在协议实现上，为了降低实现的复杂度，提高系统性能将通信模块嵌入到窗口系统的事件循环，而不采用传统的双进程模式(应用程序与通信模块各存在于一个单独进程)。构建了基于已有测试集的本地测试和远程测试框架，分别完成对协议静态格式和动态行为的测试，并通过实际情况下的测试结果来分析一致性验证中所发现的问题。
最后，基于通信协议的安全性进行讨论。
依据完整的解决方案，我们在嵌入式Linux平台下的开发环境上，利用多种技术手段，很好的完成了整个项目，实现了整套通信协议，最终使得软件较好地达到了用户的需求。
This paper laid a strong emphasis on the project how to realize the PDA's communication with distance server.
Based on the process, protocol engineer to develop the communication protocols, the paper modify and delete some activities of protocol engineering in order to be accustomed to the project.
The paper enhanced how to develop the communication system of this project under the modified protocol engineer. In architecture, it expounded the C/S pattern of network architecture and pointed out the merits between C/S pattern and distribution pattern. And we designed simple and useful 3 layers network model (physical, data link, and message layer) instead of ISO. The paper not only used the sequence diagrams to descript the cooperation of PDA and server in communications, but only adopt Petri net, a kind of FDT, to built four different models on protocol's dynamic actions. We proposed the constrict expressions: 1. Finding out and fixing the
errors, we validated the protocol with Petri net theories. We implanted communication module into message loops of windows module instead of .typical 2-processor mode. After finishing realization, we did build both local and remote testing skeleton with the set of test cases that was created in first to test static specifications and dynamic actions of protocol. And testing could help us to analyze the problems we had found in validation.
At the end of the paper, we discussed something about protocol security.
Based on the embedded Linux system, we study emphatically on the key technology of how to realize information mutually in the course of communicating among each module. And we find the corresponding solution. With this, we carry out the whole software successfully to meet the end user's demands.
基于通信协议开发的一般过程——协议工程，同时针对于本项目的特点，本文首先分析了协议工程的缺陷，对协议工程的各项活动提出了适当的修改和裁减建议。
文章重点探讨了，如何依据修改的协议工程活动来指导通信协议的开发：在体系结构上，应用并描述C/S模式的网络架构，及其相比于交叉式的网络构架的优势所在。对比ISO七层模型，设计了简单实用的三层网络模型(物理层，链路层，消息层)。在通用的时序图描述通信协议动态交互的基础上，用一种形式化描述技术——Petri网抽象通信协议的动态行为规范为一种链路层半双工停止-等待协议，从简单到复杂建立4个不同侧重点的Petri网模型，分别描述通信协议的不同动态行为：交互，超时，出错处理。提出了对于Petri网通信模型的信道约束条件公式：∑m_t≤1。利用Petri网理论对协议进行一致性验证，并修正验证时所发现的错误。在协议实现上，为了降低实现的复杂度，提高系统性能将通信模块嵌入到窗口系统的事件循环，而不采用传统的双进程模式(应用程序与通信模块各存在于一个单独进程)。构建了基于已有测试集的本地测试和远程测试框架，分别完成对协议静态格式和动态行为的测试，并通过实际情况下的测试结果来分析一致性验证中所发现的问题。
最后，基于通信协议的安全性进行讨论。
依据完整的解决方案，我们在嵌入式Linux平台下的开发环境上，利用多种技术手段，很好的完成了整个项目，实现了整套通信协议，最终使得软件较好地达到了用户的需求。
This paper laid a strong emphasis on the project how to realize the PDA's communication with distance server.
Based on the process, protocol engineer to develop the communication protocols, the paper modify and delete some activities of protocol engineering in order to be accustomed to the project.
The paper enhanced how to develop the communication system of this project under the modified protocol engineer. In architecture, it expounded the C/S pattern of network architecture and pointed out the merits between C/S pattern and distribution pattern. And we designed simple and useful 3 layers network model (physical, data link, and message layer) instead of ISO. The paper not only used the sequence diagrams to descript the cooperation of PDA and server in communications, but only adopt Petri net, a kind of FDT, to built four different models on protocol's dynamic actions. We proposed the constrict expressions: 1. Finding out and fixing the
errors, we validated the protocol with Petri net theories. We implanted communication module into message loops of windows module instead of .typical 2-processor mode. After finishing realization, we did build both local and remote testing skeleton with the set of test cases that was created in first to test static specifications and dynamic actions of protocol. And testing could help us to analyze the problems we had found in validation.
At the end of the paper, we discussed something about protocol security.
Based on the embedded Linux system, we study emphatically on the key technology of how to realize information mutually in the course of communicating among each module. And we find the corresponding solution. With this, we carry out the whole software successfully to meet the end user's demands.
引文
[1] Gerard Holzmann, Design And Validation of Computer Protocols, Pearson Education POD; Facsimile edition, 1990
[2] Bill Blunden, Virtual Machine Design and Implementation in C/C++, Wordware Publishing, 2002
[3] Travis Russell, Telecommunications Protocols, McGraw-Hill Professional Publishing; 2nd edition, 1999
[4] T. Sridhar, Designing Embedded Communications Software, CMP Books, 2003
[5] 基于电话网的信息终端及综合平台技术规范 第六分册 中文信息终端服务接口规范v1.2，中国电信集团公司，2001/1
[6] Arnold S. Berger, Embedded Systems Design: An Introduction to Processes, Tools, and Techniques, CMP Books, 2002
[7] Qing Li and Carolyn Yao, Real-Time Concepts for Embedded Systems, CMP Books, 2003
[8] Xiaodong Wang, H. Vincent Poor, Wireless Communication Systems: Advanced Techniques for Signal Reception, Prentice Hall PTR, 2003
[9] Miehah Lerner, George Vanecek, Nino Vidovic, Dado Vrsalovic, Middleware Networks: Concept, Design and Deployment of Internet Infrastructure, Kluwer Academic Publishers, 2000
[10] 袁崇义，Petri网原理，电子工业出版社，1998
[11] Andrew S. Tanenbaum, Computer Networks, Fourth Edition, Prentice Hall, 2003
[12] Martin Fowler, UML Distilled. A Brief Guide to the Standard Object Modeling Language, Third Edition. Addison Wesley, 2003
[13] Kent Beck, Extreme Programming Explained: Embrace Change, Addison-Wesley, 2000
[14] Martin Fowler, Re factoring: Improving the Design of Existing Programs, Addison-Wesley, 1999
[15] Erieh Gamma, Richard Helm, Ralph Johnson, and John Vlissides, Design Patterns: Elements of Reusable Object-Oriented Software, Addison-Wesley, 1995
[16] Craig Larman, Applying UML and Patterns, 2d ed, Prentice-Hall, 2001
[17] Steve McConnell, Rapid Development: Taming Wild Software Schedules, Microsoft Press, 1996
[18] Michael Pont, Patterns for Time-Triggered Embedded Systems, Addison-Wesley,2001
[19] 古天龙，蔡国永，网络协议的形式化分析与设计，电子工业出版社，2003
[20] 邹思轶，嵌入式Linux设计与应用，清华大学出版社，2002
[21] Kenneth D．Reed，Protocol Analysis，电子工业出版社，2002
[22] W．Richard Stevens，Advanced Programming in the UNIX Environment，机械工业出版社，2002
[23] KirK Zurell，CProgramming for Embedded Systems，机械工业出版社，2002
[24] John GProakis，Digital Communications,Fourth Edition，电子工业出版社，
2001
[25] R. Esser, J. Teich, L. Thiele, CodeSign: An embedded system design environment, in IEE Proc. Computers and Digital Techniques, vol. 145, May 1998, pp. 171-180
[26] Luis Alejandro Cort(?)s, Petru Eles, Zebo Peng, A Petri Net based Model for Heterogeneous Embedded Systems, in Proc. NORCHIP Conference, 1999, pp. 248-255
[27] H. J. Genrich, K. Lautenbach, System modelling with high-level Petri nets, in Theoretical Computer Science, vol. 13, Jan. 1981, pp. 109-136
[28] Luis Alejandro Cort(?)s, Petru Eles, Zebo Peng, Verification of Embedded Systems using a Petri Net based Representation, in Proc. ISSS, 2000, pp. 149-155
[29] 胡家宝，Petri网及其随机Petri网的性能分析方法，系统工程与电子技术，1994年第2期，pp．32-40
[30] 蔡荣希，基于Petri网的舰载指控系统性能评价，系统工程与电子技术，1997年第5期，pp．18-24
[31] Stefan Boecking，Object-Oriented Network Protocols，机械工业出版社，2000
[32] 吴克，周正康，LAPD协议的Petri网描述与验证，计算机工程第21卷，第6期，1995．11，pp．63-67
[33] 李正明，黄如，半双工协议的Petri网分析及FPGA实现，江苏理工大学学报第22卷第5期，2001．9，pp．64．68
[34] 邓莹，古天龙，基于Petri网的协议分析技术以工具，桂林电子工业学院学报，第22卷第1期，2002．2，pp．6．11
[35] 李旭，费敏锐，时间Petri网载现场通信系统中的分析方法，测控技术第19卷第12期，2000，pp．28-32
[36] 林闯，吴建平，王鼎兴，随机高级Petri网用于计算机网络传输协议的模型与性能评价，通信学报第15卷第6期，1994．11，pp．9-16
[37] 张俊荣，一种数据链路层协议的Petri网模型，广州师院学报(自然科学版)第20卷第2期．1998，pp．17-21
[38] P. Maeiel, E. Barros, and W. Rosenstiel, A Petri Net Model for Hardware/Software Codesign, in Design Automation for Embedded Systems, vol. 4, Oct. 1999, pp. 243-310
[39] Saiedai H, An Introduction to Formal Methed, in IEEE Computer, 1996, 29(4), pp. 16-30
[40] P. M. Merlin, D. J. Farber, Recoverability of Communication Protocols—Implications of a Theoretical Study, in IEEE Trans. Communications, vol. COM-24, Sept. 1976, pp. 1036-1042
[41] R. Alur, T. A. Henzinger, P.-H. Ho, Automatic Symbolic Verification of Embedded Systems, in IEEE Trans, Software Engineering, vol. 22, March 1996, pp. 181-201
[42] 罗军舟，沈俊，顾冠群，从Petri网到形式描述和协议工程，软件学报，2000．11， pp．606-615
[43] 褚秉华，仇佩亮，电信协议工程与形式化方法，浙江大学学报(工学版)第 37卷第1期，2001，pp．37-41
[44] 罗军舟，顾冠群，协议工程技术，电信科学第10卷第7期，1994，pp．57-59
[45] 郭云川，古天龙，董荣胜，李凤英Kerberos协议安全性的符号模型检验分析，计算机工程与应用2003年29期，2003，pp．177．180
[46] 杨朝晖，面向电信维护的嵌入式系统研究，西北工业大学硕士学位论文， 2004
[47] 郭相国，嵌入式浏览器研究，西北工业大学硕士学位论文，2002
[48] 常衡生，水情自动测报系统设计与实现，西南交通大学硕士学位论文，2002
[49] 吴鹏，Bluetooth服务发现协议的验证、实现与测试，硕士学位论文
[50] 于振华，基于高级Petri网的控制系统应用研究，西安电子科技大学硕士论文，2003
[51] 王安荣，柔性制造系统死锁分析与控制，西安电子科技大学硕士论文，2003
[52] Alan Harbitter, A Methodology for Analyzing the Performance of Authentication Protocols, dissertation for George Mason University, 2001
[53] Randy W. Ho, Automatic Design of Network Security Protocols, dissertation for the degree of Doctor of Philosophy in The University of Michigan, 2002
[54] Michael D. Jones, Formal Verification of Parameterized Protocols on Branching Networks, dissertation for the degree of Doctor of Philosophy in The University of Utah, 2001
[55] 刘钊，C/S模式在监控系统中的研究与应用，西北工业大学硕士学位论文，2003
[56] 王建平，PDA 线务通通信协议的研究与实现，西北工业大学硕士学位论文，2003
[57] Bill Blunden, Memory Management: Algorithms and Implementation in C/C++, Wordware Publishing 2003
[2] Bill Blunden, Virtual Machine Design and Implementation in C/C++, Wordware Publishing, 2002
[3] Travis Russell, Telecommunications Protocols, McGraw-Hill Professional Publishing; 2nd edition, 1999
[4] T. Sridhar, Designing Embedded Communications Software, CMP Books, 2003
[5] 基于电话网的信息终端及综合平台技术规范 第六分册 中文信息终端服务接口规范v1.2，中国电信集团公司，2001/1
[6] Arnold S. Berger, Embedded Systems Design: An Introduction to Processes, Tools, and Techniques, CMP Books, 2002
[7] Qing Li and Carolyn Yao, Real-Time Concepts for Embedded Systems, CMP Books, 2003
[8] Xiaodong Wang, H. Vincent Poor, Wireless Communication Systems: Advanced Techniques for Signal Reception, Prentice Hall PTR, 2003
[9] Miehah Lerner, George Vanecek, Nino Vidovic, Dado Vrsalovic, Middleware Networks: Concept, Design and Deployment of Internet Infrastructure, Kluwer Academic Publishers, 2000
[10] 袁崇义，Petri网原理，电子工业出版社，1998
[11] Andrew S. Tanenbaum, Computer Networks, Fourth Edition, Prentice Hall, 2003
[12] Martin Fowler, UML Distilled. A Brief Guide to the Standard Object Modeling Language, Third Edition. Addison Wesley, 2003
[13] Kent Beck, Extreme Programming Explained: Embrace Change, Addison-Wesley, 2000
[14] Martin Fowler, Re factoring: Improving the Design of Existing Programs, Addison-Wesley, 1999
[15] Erieh Gamma, Richard Helm, Ralph Johnson, and John Vlissides, Design Patterns: Elements of Reusable Object-Oriented Software, Addison-Wesley, 1995
[16] Craig Larman, Applying UML and Patterns, 2d ed, Prentice-Hall, 2001
[17] Steve McConnell, Rapid Development: Taming Wild Software Schedules, Microsoft Press, 1996
[18] Michael Pont, Patterns for Time-Triggered Embedded Systems, Addison-Wesley,2001
[19] 古天龙，蔡国永，网络协议的形式化分析与设计，电子工业出版社，2003
[20] 邹思轶，嵌入式Linux设计与应用，清华大学出版社，2002
[21] Kenneth D．Reed，Protocol Analysis，电子工业出版社，2002
[22] W．Richard Stevens，Advanced Programming in the UNIX Environment，机械工业出版社，2002
[23] KirK Zurell，CProgramming for Embedded Systems，机械工业出版社，2002
[24] John GProakis，Digital Communications,Fourth Edition，电子工业出版社，
2001
[25] R. Esser, J. Teich, L. Thiele, CodeSign: An embedded system design environment, in IEE Proc. Computers and Digital Techniques, vol. 145, May 1998, pp. 171-180
[26] Luis Alejandro Cort(?)s, Petru Eles, Zebo Peng, A Petri Net based Model for Heterogeneous Embedded Systems, in Proc. NORCHIP Conference, 1999, pp. 248-255
[27] H. J. Genrich, K. Lautenbach, System modelling with high-level Petri nets, in Theoretical Computer Science, vol. 13, Jan. 1981, pp. 109-136
[28] Luis Alejandro Cort(?)s, Petru Eles, Zebo Peng, Verification of Embedded Systems using a Petri Net based Representation, in Proc. ISSS, 2000, pp. 149-155
[29] 胡家宝，Petri网及其随机Petri网的性能分析方法，系统工程与电子技术，1994年第2期，pp．32-40
[30] 蔡荣希，基于Petri网的舰载指控系统性能评价，系统工程与电子技术，1997年第5期，pp．18-24
[31] Stefan Boecking，Object-Oriented Network Protocols，机械工业出版社，2000
[32] 吴克，周正康，LAPD协议的Petri网描述与验证，计算机工程第21卷，第6期，1995．11，pp．63-67
[33] 李正明，黄如，半双工协议的Petri网分析及FPGA实现，江苏理工大学学报第22卷第5期，2001．9，pp．64．68
[34] 邓莹，古天龙，基于Petri网的协议分析技术以工具，桂林电子工业学院学报，第22卷第1期，2002．2，pp．6．11
[35] 李旭，费敏锐，时间Petri网载现场通信系统中的分析方法，测控技术第19卷第12期，2000，pp．28-32
[36] 林闯，吴建平，王鼎兴，随机高级Petri网用于计算机网络传输协议的模型与性能评价，通信学报第15卷第6期，1994．11，pp．9-16
[37] 张俊荣，一种数据链路层协议的Petri网模型，广州师院学报(自然科学版)第20卷第2期．1998，pp．17-21
[38] P. Maeiel, E. Barros, and W. Rosenstiel, A Petri Net Model for Hardware/Software Codesign, in Design Automation for Embedded Systems, vol. 4, Oct. 1999, pp. 243-310
[39] Saiedai H, An Introduction to Formal Methed, in IEEE Computer, 1996, 29(4), pp. 16-30
[40] P. M. Merlin, D. J. Farber, Recoverability of Communication Protocols—Implications of a Theoretical Study, in IEEE Trans. Communications, vol. COM-24, Sept. 1976, pp. 1036-1042
[41] R. Alur, T. A. Henzinger, P.-H. Ho, Automatic Symbolic Verification of Embedded Systems, in IEEE Trans, Software Engineering, vol. 22, March 1996, pp. 181-201
[42] 罗军舟，沈俊，顾冠群，从Petri网到形式描述和协议工程，软件学报，2000．11， pp．606-615
[43] 褚秉华，仇佩亮，电信协议工程与形式化方法，浙江大学学报(工学版)第 37卷第1期，2001，pp．37-41
[44] 罗军舟，顾冠群，协议工程技术，电信科学第10卷第7期，1994，pp．57-59
[45] 郭云川，古天龙，董荣胜，李凤英Kerberos协议安全性的符号模型检验分析，计算机工程与应用2003年29期，2003，pp．177．180
[46] 杨朝晖，面向电信维护的嵌入式系统研究，西北工业大学硕士学位论文， 2004
[47] 郭相国，嵌入式浏览器研究，西北工业大学硕士学位论文，2002
[48] 常衡生，水情自动测报系统设计与实现，西南交通大学硕士学位论文，2002
[49] 吴鹏，Bluetooth服务发现协议的验证、实现与测试，硕士学位论文
[50] 于振华，基于高级Petri网的控制系统应用研究，西安电子科技大学硕士论文，2003
[51] 王安荣，柔性制造系统死锁分析与控制，西安电子科技大学硕士论文，2003
[52] Alan Harbitter, A Methodology for Analyzing the Performance of Authentication Protocols, dissertation for George Mason University, 2001
[53] Randy W. Ho, Automatic Design of Network Security Protocols, dissertation for the degree of Doctor of Philosophy in The University of Michigan, 2002
[54] Michael D. Jones, Formal Verification of Parameterized Protocols on Branching Networks, dissertation for the degree of Doctor of Philosophy in The University of Utah, 2001
[55] 刘钊，C/S模式在监控系统中的研究与应用，西北工业大学硕士学位论文，2003
[56] 王建平，PDA 线务通通信协议的研究与实现，西北工业大学硕士学位论文，2003
[57] Bill Blunden, Memory Management: Algorithms and Implementation in C/C++, Wordware Publishing 2003