基于petri网的tcp协议研究

《基于petri网的tcp协议研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、硕士学位论文形式代表了不同开发阶段的结果。协议的表示形式有：非形式描述文本(InformalSpecincation)：用自然语言和图表表述的协议，易读易懂，但不严密，有多义性。形式描述文本(FormalSpecmcation)：用FDL描述的协议，严密，无二义性，可符号执行，可转换成程序设计语言的程序。与机器无关的源程序代码(Machine—IndependentSourceCode)：这是由形式描述文本翻译过来的程序设计语言(Pascal、C等)程序。协议本身有一定抽象性，即协议没有指明这个协议在某个机器上怎样实现，正因为协议本身是抽象的，它才适合

2、用FDL描述。这样，形式描述文本翻译后的程序就是与机器无关的代码了。实现代码(ImplementationCode)：这是协议实现后的最终代码。一般与机器无关的源程序代码只占最终实现代码的一部分(50％)。协议在一种机器上的实现还包括大量协议文本没有描述的程序，例如缓冲器分配管理、系统输入／输出操作等，这部分程序称作与机器相关代码。测试套具(TestSuite)：这是一组关于协议测试步骤和测试数据的文件，它由协议的形式描述文本产生。测试套具是用另外一种语言描述的(形式描述语言或非形式描述语言)。性能分析非形式描述文本验证鳖蔗程序代码l／／铡试套工炒(／

3、前T芒』皇V图1．1协议工程系统【11协议工程包括下列多个子系统，每个子系统由多个软件工具构成。1)转换(Transformation)系统该系统将协议的非形式描述文本转换成形式描述文本。该系统要求高智能化3善不基于Petri网的TCP协议的研究的软件去识别和读懂非形式描述文本，因此该系统实际上是一个人工系统。2)验证(Verincation，Validation)系统对协议进行验证检查，发现并修改潜在的错误。3)性能分析(PerformanceAnalysis)系统对协议性能进行分析评价，修改协议，提高性能。4)翻译(Translation)系统将形

4、式描述文本翻译成程序代码。5)实现(Implementation)系统它实际是具体操作系统所提供的程序开发环境(编辑、编译、连接、调试、排错等)。实现代码在这个系统中产生。6)测试(Test)系统测试套具在该系统中执行，对实现代码进行测试，分析结构，检测错误，将错误反馈给实现系统，修改实现代码。在某些情况下，错误信息还必须反馈给协议实现者。7)测试套具生成(TestSuiteGeneration)系统根据协议的形式化描述文本产生测试程序和测试数据，该系统的部分工作可有人工完成。图1．1所示是一个完整的协议工程系统，随着协议工程技术的发展，系统中的软件工

5、具将越来越完善，越来越方便，自动化程序也将逐步提高。形式化描述方法是协议工程核心部分，关联了协议工程中的各个过程。目前适用于协议工程的形式化描述方法种类繁多，各具特色，但也各有不足，使用什么样形式化描述方法进行协议设计、验证，乃至后续的协议测试，是协议工程领域中的一个重要的核心问题。协议验证(Protoc01verincation)是协议工程的重要组成部分，是对通协议本身的逻辑性和正确性进行验证的过程。它处于协议工程中协议设计阶段之后，协议实现阶段之前。其工作过程一般是通过选择合适的形式化描述方法对协议进行形式化描述，然后用基于数学的方法，检验或证明协

6、议设计的逻辑正确性。1．2课题的研究现状1．2．1形式化描述技术利用形化技术对模型进行描述以及验证理论的研究将直接影响到计算机通信协议开发技术的进步和发展。所以很多国家都投入了大量的人力物力从事这方面的研究工作。例如：英国的国家物理局NPL、法国国家通信研究中心、德国国家通信研究局GMD、美国国家标准化研究局、美国新罕布什尔大学互操作研究4硕士学位论文实验室都在这个领域投入了大量的研究力量。为了提供协议设计的坚实基础，要使用数学的方法，不但能够提供无二义性的描述，而且能够对描述进行形式分析和细化。协议形式化指使用形式描述技术(FormalDescrip

7、tionTechnique)贯穿协议开发的各个阶段，起始于协议规范描述，使得协议的研究开发可以独立于非形式的自然语言文本和最终实现代码，避免协议验证测试的复杂性。理想的FDT应能支持协议工程活动的各个环节，特别是协议综合、验证、自动实现和一致性测试。利用数学技术允许开发描述语言的编译器和由描述派生的自动测试序列，这将大大提高协议实现和维护的能力，降低提供和维持信息服务的代价。作为一个FDT，它有如下重要特性【4】：1)完整的语法和语义定义；2)体系结构、服务和协议的可表达性；3)协议重要特性(如：无死锁)的可分析性；4)支持复杂协议的管理(如：构造能力

8、)；5)支持渐进细化的方法；6)支持实现独立性(包括并发性、非确定性和适当的抽象机制)；7)支