论文部分内容阅读
摘 要：随着形式化方法和技术的日趋完善，网络协议的开发已逐步从非形式化描述、手工方法实现过渡到已形式化描述技术为基础，渗透到网络协议分析、综合、测试等各环节的软件工程方法。本文从网络协议的基本要素、协议的形式化模型介绍了网络协议，并从协议的性质描述、不变性分析、可达性分析、基于有序二叉判决图的符号模型检验对网络协议进行了形式化设计与验证，最后进行了测试。
关键词：网络协议 形式化分析 符号模型检验
中图分类号：T298K2 文献标识码：A 文章编号：1672-3791（2013）（03）（b）-0034-02
协议一词最早出现在通信系统，协议历史拥有像通信一样古老的历史。从古至今，人们一直都在不断的探索研究，怎样才能建立一个能够在快速在远距离上传输信息的系统。如果想要实现信息在远距离间传递，不光需要硬件设备，也就是发送和接收信号的设备，还需要建立一整套能够规定信号所代表的意义以及传递接收信号方式的规则、标准或者约定，这个规则就是协议。
1 网络协议的基本要素
一套完整的，能够确保计算机网络可以顺利进行数据通信的网络协议要包括下边的五点基本要素：（1）协议所提供的服务。（2）对协议运行环境所进行的假设。（3）用来实现协议的消息词汇。（4）对该词汇中每个消息的编码。（5）用来控制消息一致性的过程规则。
实现计算机之间高度自动化数据通信的网络协议，一般都会极其复杂。借鉴对复杂系统问题分析研究的思想，分层结构对于理解和设计网络协议有着重要的作用。“七层”协议结构模型是目前网络协议的标准体系结构，也成为了网络协议开发的基础。
2 协议的形式化模型
协议分析和设计其中一项核心技术就是形式化模型。网络协议的形式化规格可以在形式化模型的基础上实现，从而为协议的形式化分析与验证、协议综合、协议测试、以及协议实现等提供良好的基础。形式化模型包括以下几点。
2.1 协议的有限状态机模型
有限状态机包括有限状态集、输入集和状态转移规则集；有限状态集，用于描述系统中的不同状态；输入集用于表征系统所接收的不同输入信息；状态转移规则集用于表述系统在接收不同输入下从一个状态转移到另外一个状态的规则。
2.2 Petri网模型
Petri网是一种适合于并发、异步、分布式系统描述与分析的图形数学工具。Petri网已成为网络协议分析和设计的典型形式模型之一。它作为系统描述和分析的工具，除了具有静态结构外，还包括了描述系统动态行为的机制。这一特征是通过允许位置中包含令牌，令牌可以依据迁移的引发而重新分布来实现的。
2.3 协议的时态逻辑模型
时态逻辑是模态逻辑的扩充，它涉及含有时间信息的事件、状态及其关系的命题、谓词和演算。要描述一个协议，首先要标识系统中的个体常量，定义变量，表达命题、谓词函数。以下为命题与谓词的表达。
（1）个体常量m0，m1表示序号为0，1的报文；any表示无序号的任意报文；ack0，ack1表示序号为0，1的认可报文。
（2）个体变量m代表m0，m1，any；ack代表ack0，ack1；seq代表0，1序号；a代表原子行动或事件。
（3）谓词at（a）开始一个协议行动或事件。
2.4 通信进程演算模型
通信进程演算是计算机通信系统的基本理论模型，它也是许多形式化语言的基础。通信进程演算的基本成分是事件与进程，而进程是通过顺序、选择和并行三个基本算子来定义的。一般用大写字母来表示进程，用小写字母来表示事件。
3 协议的形式化设计与验证
协议的设计验证是对协议的功能和性能进行校验的过程，是保证协议开发质量的必要环节。协议形式化验证首先需要对协议性质进行系统的语言描述，然后基于协议的形式模型或者形式语言进行描述，通过适当的技术对协议性质进行分析校验。
3.1 协议的性质描述
设计网络协议的目的就是设计出的协议要满足功能和性能。一方面，协议本身应用问题的特征性对协议的功能和性能具有特殊的要求；另外一方面，协议的功能和性能所拥有的协议的性质，是独立于问题的一般性要求。协议的性质包括活性、安全性、一致性、完备性、可恢复性和有界性六方面。
（1）活性就是指无死锁性，如果在协议运行时候发生一些好事，就叫协议的活性，像发生预定的事情，能够到达指定的协议状态，可以进行应该进行的协议活动等都是协议的好事情。协议的终止性和进展性两反面可以体现协议的活性。也就是说具有终止性和进展性的协议就拥有活性。如果协议能够在从任何一状态下开始运行都能正确的到达终止状态，就是协议的终止性。终止状态在某些情况下也会和初始状态是同一个。所以协议总能从初始状态开始运行然后正确的回到初始状态，并可反复运行，这就是协议的可重复性，即可重复性=终止性+进展性=活动性。
（2）安全性就是没有坏的事情出现在协议运行的时候。像不可接收事件、不可进一步向前的状态、错误的行动、错误的条件、变量值越界等都是坏的事情。坏事情一般会导致死锁和活锁两种情况发生。
（3）一致性就是指协议的服务行为和协议行为保持一致。像协议需要为用户提供的所要求的业务和不用提供用户没有要求提供的业务都体现了协议的一致性。
（4）完备性，协议拥有完全符合协议环境各种要求的性质，也就是在考虑了用户要求、用户特点、通道性质、工作模式等各种潜在影响因素之后构建的协议构造，同时兼备考虑各种错误事件以及异常情况的处理。
（5）可恢复性是指当协议出现差错后，协议本身能否在有限的步骤内返回到正常状态下执行。可恢复性是和可重复性相关联的一个性质。
（6）有界性是与协议中的变量和参数有关的一个性质，用来衡量协议中的变量和参数是否超过其限定值。 3.2 不变性分析
系统不变性是某一逻辑公式表达的系统性质的永真性，它不随系统的状态变化或执行序列而改变。系统不变性分析实际包含两个任务。第一是分析系统应该具有的不变性质，并用逻辑公式来表示，第二个任务是分析系统的执行，证明该逻辑公式成立。
3.3 可达性分析
可达性分析是试图产生和检查协议所有部分的可达状态，进而检验基于状态或者基于状态序列的协议性质。所谓可达状态是指协议从初始状态开始经历有限次转换之后可达到的状态，所有可达状态构成了系统状态空间。可达性分析算法是用来生成并检验一个特定的初始状态可达的所有状态算法。
3.4 基于有序二叉判决图的符号模型检验
符号模型检验是采用紧凑的信息压缩形式来隐式表示系统可达状态和要求证明性质的逻辑公式的模型检验。有序二叉判决图是隐式、高效率表示状态空间的一种数据结构。基于有序二叉判决图的符号模型检验是分析验证协议系统的有效技术。
基于有序二叉判决图实现的模型检验算法能有效地避免状态爆炸的问题，使得验证系统适用的系统规模扩大，现已能对具有多达1020个状态的系统进行验证。基于有序二叉判决图的符号模型验证主要考虑以下几个方面：状态的布尔公式表示；状态转移关系的布尔公式表示；Kripke结构的布尔公式表示；CTL公式在布尔公式表示的Kripke结构上的解释。
现用QBF公式表示Kripke结构，并把用这些符号表示的Kripke结构上的CTL算子用QBF上的算子来描述。实际上，因为逻辑连接词在CTL*和QBF上有着相同的意义，所以只需要刻画算子EN，而其它的CTL*的算子可以通过EN和逻辑运算的函数不动点进行描述。
4 网络协议的测试
测试是保证网络协议质量的一个重要手段，是协议实现过程中的一种实验活动。尽管测试并不能完全证明协议实现的正确性，但是在系统的测试活动检查下，可以把协议在实现过程中出错的概率降低到实际应用可以接受的程度。
相对而言，基于有限状态机模型的协议测试方法有比较高的错误覆盖率。然而，在实际中，协议规格的状态机模型并不满足对有限状态机的假设，即便满足，相应的测试生成算法也太复杂，生成的测试序列也太长，测试成本太高。随时着各种各样的有限状态机规格的广泛使用，借助于软件数据流测试的思想，基于数据流的协议测试序列生成方法相应得到了研究应用。数据流测试通常基于有向数据流图。在理想情况下，测试所有可能的输入数据将提供最完全的程序行为信息，而在实际测试中，通常选择一个可以代表整个输入域的子集。
5 结语
形式化方法是基于严密的、数学上的形式机制的系统研究方法。客观地讲，有了数学的应用，就有了形式化的方法。迄今为止，形式化方法成功地应用于空中交通管制系统、铁路信号系统、核电站控制系统、通信系统、医疗监护系统、硬件电路等诸多领域。网络协议的形式化分析和设计正在向完善化、系统化、自动化和标准化方向发展。
参考文献
[1] 鲁来凤，吴振强，马建峰.基于PCL的改进型Helsinki协议的形式化分析[J].华中科技大学学报（自然科学版），2011（4）.
[2] 王惠斌.安全认证协议的设计与分析[D].解放军信息工程大学，2010.
关键词：网络协议 形式化分析 符号模型检验
中图分类号：T298K2 文献标识码：A 文章编号：1672-3791（2013）（03）（b）-0034-02
协议一词最早出现在通信系统，协议历史拥有像通信一样古老的历史。从古至今，人们一直都在不断的探索研究，怎样才能建立一个能够在快速在远距离上传输信息的系统。如果想要实现信息在远距离间传递，不光需要硬件设备，也就是发送和接收信号的设备，还需要建立一整套能够规定信号所代表的意义以及传递接收信号方式的规则、标准或者约定，这个规则就是协议。
1 网络协议的基本要素
一套完整的，能够确保计算机网络可以顺利进行数据通信的网络协议要包括下边的五点基本要素：（1）协议所提供的服务。（2）对协议运行环境所进行的假设。（3）用来实现协议的消息词汇。（4）对该词汇中每个消息的编码。（5）用来控制消息一致性的过程规则。
实现计算机之间高度自动化数据通信的网络协议，一般都会极其复杂。借鉴对复杂系统问题分析研究的思想，分层结构对于理解和设计网络协议有着重要的作用。“七层”协议结构模型是目前网络协议的标准体系结构，也成为了网络协议开发的基础。
2 协议的形式化模型
协议分析和设计其中一项核心技术就是形式化模型。网络协议的形式化规格可以在形式化模型的基础上实现，从而为协议的形式化分析与验证、协议综合、协议测试、以及协议实现等提供良好的基础。形式化模型包括以下几点。
2.1 协议的有限状态机模型
有限状态机包括有限状态集、输入集和状态转移规则集；有限状态集，用于描述系统中的不同状态；输入集用于表征系统所接收的不同输入信息；状态转移规则集用于表述系统在接收不同输入下从一个状态转移到另外一个状态的规则。
2.2 Petri网模型
Petri网是一种适合于并发、异步、分布式系统描述与分析的图形数学工具。Petri网已成为网络协议分析和设计的典型形式模型之一。它作为系统描述和分析的工具，除了具有静态结构外，还包括了描述系统动态行为的机制。这一特征是通过允许位置中包含令牌，令牌可以依据迁移的引发而重新分布来实现的。
2.3 协议的时态逻辑模型
时态逻辑是模态逻辑的扩充，它涉及含有时间信息的事件、状态及其关系的命题、谓词和演算。要描述一个协议，首先要标识系统中的个体常量，定义变量，表达命题、谓词函数。以下为命题与谓词的表达。
（1）个体常量m0，m1表示序号为0，1的报文；any表示无序号的任意报文；ack0，ack1表示序号为0，1的认可报文。
（2）个体变量m代表m0，m1，any；ack代表ack0，ack1；seq代表0，1序号；a代表原子行动或事件。
（3）谓词at（a）开始一个协议行动或事件。
2.4 通信进程演算模型
通信进程演算是计算机通信系统的基本理论模型，它也是许多形式化语言的基础。通信进程演算的基本成分是事件与进程，而进程是通过顺序、选择和并行三个基本算子来定义的。一般用大写字母来表示进程，用小写字母来表示事件。
3 协议的形式化设计与验证
协议的设计验证是对协议的功能和性能进行校验的过程，是保证协议开发质量的必要环节。协议形式化验证首先需要对协议性质进行系统的语言描述，然后基于协议的形式模型或者形式语言进行描述，通过适当的技术对协议性质进行分析校验。
3.1 协议的性质描述
设计网络协议的目的就是设计出的协议要满足功能和性能。一方面，协议本身应用问题的特征性对协议的功能和性能具有特殊的要求；另外一方面，协议的功能和性能所拥有的协议的性质，是独立于问题的一般性要求。协议的性质包括活性、安全性、一致性、完备性、可恢复性和有界性六方面。
（1）活性就是指无死锁性，如果在协议运行时候发生一些好事，就叫协议的活性，像发生预定的事情，能够到达指定的协议状态，可以进行应该进行的协议活动等都是协议的好事情。协议的终止性和进展性两反面可以体现协议的活性。也就是说具有终止性和进展性的协议就拥有活性。如果协议能够在从任何一状态下开始运行都能正确的到达终止状态，就是协议的终止性。终止状态在某些情况下也会和初始状态是同一个。所以协议总能从初始状态开始运行然后正确的回到初始状态，并可反复运行，这就是协议的可重复性，即可重复性=终止性+进展性=活动性。
（2）安全性就是没有坏的事情出现在协议运行的时候。像不可接收事件、不可进一步向前的状态、错误的行动、错误的条件、变量值越界等都是坏的事情。坏事情一般会导致死锁和活锁两种情况发生。
（3）一致性就是指协议的服务行为和协议行为保持一致。像协议需要为用户提供的所要求的业务和不用提供用户没有要求提供的业务都体现了协议的一致性。
（4）完备性，协议拥有完全符合协议环境各种要求的性质，也就是在考虑了用户要求、用户特点、通道性质、工作模式等各种潜在影响因素之后构建的协议构造，同时兼备考虑各种错误事件以及异常情况的处理。
（5）可恢复性是指当协议出现差错后，协议本身能否在有限的步骤内返回到正常状态下执行。可恢复性是和可重复性相关联的一个性质。
（6）有界性是与协议中的变量和参数有关的一个性质，用来衡量协议中的变量和参数是否超过其限定值。 3.2 不变性分析
系统不变性是某一逻辑公式表达的系统性质的永真性，它不随系统的状态变化或执行序列而改变。系统不变性分析实际包含两个任务。第一是分析系统应该具有的不变性质，并用逻辑公式来表示，第二个任务是分析系统的执行，证明该逻辑公式成立。
3.3 可达性分析
可达性分析是试图产生和检查协议所有部分的可达状态，进而检验基于状态或者基于状态序列的协议性质。所谓可达状态是指协议从初始状态开始经历有限次转换之后可达到的状态，所有可达状态构成了系统状态空间。可达性分析算法是用来生成并检验一个特定的初始状态可达的所有状态算法。
3.4 基于有序二叉判决图的符号模型检验
符号模型检验是采用紧凑的信息压缩形式来隐式表示系统可达状态和要求证明性质的逻辑公式的模型检验。有序二叉判决图是隐式、高效率表示状态空间的一种数据结构。基于有序二叉判决图的符号模型检验是分析验证协议系统的有效技术。
基于有序二叉判决图实现的模型检验算法能有效地避免状态爆炸的问题，使得验证系统适用的系统规模扩大，现已能对具有多达1020个状态的系统进行验证。基于有序二叉判决图的符号模型验证主要考虑以下几个方面：状态的布尔公式表示；状态转移关系的布尔公式表示；Kripke结构的布尔公式表示；CTL公式在布尔公式表示的Kripke结构上的解释。
现用QBF公式表示Kripke结构，并把用这些符号表示的Kripke结构上的CTL算子用QBF上的算子来描述。实际上，因为逻辑连接词在CTL*和QBF上有着相同的意义，所以只需要刻画算子EN，而其它的CTL*的算子可以通过EN和逻辑运算的函数不动点进行描述。
4 网络协议的测试
测试是保证网络协议质量的一个重要手段，是协议实现过程中的一种实验活动。尽管测试并不能完全证明协议实现的正确性，但是在系统的测试活动检查下，可以把协议在实现过程中出错的概率降低到实际应用可以接受的程度。
相对而言，基于有限状态机模型的协议测试方法有比较高的错误覆盖率。然而，在实际中，协议规格的状态机模型并不满足对有限状态机的假设，即便满足，相应的测试生成算法也太复杂，生成的测试序列也太长，测试成本太高。随时着各种各样的有限状态机规格的广泛使用，借助于软件数据流测试的思想，基于数据流的协议测试序列生成方法相应得到了研究应用。数据流测试通常基于有向数据流图。在理想情况下，测试所有可能的输入数据将提供最完全的程序行为信息，而在实际测试中，通常选择一个可以代表整个输入域的子集。
5 结语
形式化方法是基于严密的、数学上的形式机制的系统研究方法。客观地讲，有了数学的应用，就有了形式化的方法。迄今为止，形式化方法成功地应用于空中交通管制系统、铁路信号系统、核电站控制系统、通信系统、医疗监护系统、硬件电路等诸多领域。网络协议的形式化分析和设计正在向完善化、系统化、自动化和标准化方向发展。
参考文献
[1] 鲁来凤，吴振强，马建峰.基于PCL的改进型Helsinki协议的形式化分析[J].华中科技大学学报（自然科学版），2011（4）.
[2] 王惠斌.安全认证协议的设计与分析[D].解放军信息工程大学，2010.