（测试计量技术及仪器专业论文）基于sip协议的形式化描述及验证技术的研究.pdf

南京邮电大学硕士研究生学位论文摘要摘要协议工程是通信及计算机网络研究的一个重要的领域，目的是减少协议开发中潜在的错误，提高协议开发的效率，促进标准化的发展。它主要包括协议形式化描述、协议验证、协议实现、协议测试等方面的理论和方法的研究，其中形式化描述与验证技术是整个协议设计与实现的基础，对协议实现的正确性、完整性和复杂度有至关重要的影响。本文以协议工程的理论为依据，在对s i p 协议深入分析和研究的基础上，利用t e l e l o g i ct a u 工具软件对s i p 协议的通信流程进行了形式化描述，并对协议模型进行了仿真和验证，以保证协议模型实现了协议规范描述的功能，证明该s i p 协议模型设计正确。本文还进一步讨论了协议验证的相关概念，主要讨论了基于f s m 模型的可达性分析方法，并且重点介绍了最大化前进状态搜索，并对该方法进行了改进，提出了一种更加优越的方法，消除了搜索中存在的重复性工作，从而降低了产生的状态空间，有效地避免了状态爆炸。最后通过对s i p 协议模型的验证分析，显示了改进方法的优越性。关键词：协议工程形式化描述技术协议验证有限状态机s d l南京邮电大学硕士研究生学位论文a b s t r a c ta b s t r a c tp r o t o c o le n g i n e e ri sa l li m p o r t a n tr e s e a r c ha r e ao fc o m m u n i c a t i o na n dc o m p u t e rn e t w o r k i ti st od e c r e a s et h ep o t e n t i a le n d r s ，t oi n c r e a s et h ee f f i c i e n c yo fe m p o l d e r , t oa d v a n c et h ed e v e l o p m e n to fs t a n d a r d i z a t i o n t h er e s e a r c h e so np r o t o c o le n g i n e e r i n gi n c l u d es e v e r a lt h e o r i e sa n dm e t h o d s ，s u c ha sp r o t o c o ls p e c i f i c a t i o n ，p r o t o c o lv a l i d a t i o n ，p r o t o c o lt e s t i n ga n dp r o t o c o li m p l e m e n t a t i o n p r o t o c o lf o r m a ld i s c r i p t i o n sa n dp r o t o c o lv a l i d a t i o na r ep r o t o c o le n g i n e e r i n g sf o u n d a t i o n ，a n dh a v es i g n i f i c a n ti n f l u n e c eo nt h ec o r r e c t n e s s ，i n t e g r a l i t ya n dc o m p l e x i t yo ft h ew h o l ep r o t o c o li m p l e m e n t a t i o n t h i sp a p e rb a s e so nt h et h e r yo fp r o t o c o le n g i n e e r b ys t u d y i n gs i pp r o t o c o ld e e p l y ，t h ep a p e rg i v e st h es p e c i f i cm e t h o da b o u th o wt od e s i g nt h ek e yf u n c t i o no fs i pp r o t o c o lu s i n gt h et e l e l o g i ct a ut o o l s t h es y s t e m ss i m u l a t i o na n dv a l i d a t i o nh a v eb e e nc o m p l e t e dt om a k es u r et h a tt h em o d e lh a sr e a l i z e st h ef u n c t i o ni nt h ep r o t o c o lc r i t e r i o na n dt h ed e s i g no ft h em o d e li sc o r r e c t t h e r ea r ef u r t h e rs t u d i e so nt h e r e l a t e dc o n c e p t sa b o u tp r o t o c o lv a l i d a t i o n t h ep a p e rd i s c u s s e st h er e a c h a b i l i t ya n a l y s i sb a s e do nf s mm a i n l y o n ei m p r o v e dm e t h o di sp r o p o s e dt oe l i m i n a t er e d u n d a n tw o r ko nt h eb a s eo fm a x i m a lp r o g r e s ss t a t ee x p l o r a t i o n t h em e t h o dh a st h es a m ea n a l y t i c a lp o w e rb u tr e q u i r e sl e s st i m ea n ds p a c e ，a v o i d i n gs t a t ee x p l o s i o ne f f i c i e n t l y w i t ht h i si m p r o v e dm e t h o d ，t h ef s ma b o u ts i pp r o t o c o li sv a l i d a t e d t h ea d v a n t a g eo ft h em e t h o di sr e v e a l e da f t e rt h ec o m p a r a t i o no ft h ev a l i d a t a t i o nr e s u l t k e y w o r d s ：p r o t o c o le n g i n e e r ；f o r m a ld e s c r i p t i o nt e c h n i q u e ；p r o t o c o lv a l i d a t i o n ；f i n i t es t a t em a c h i n e ；s d li l南京邮电大学学位论文独创性声明本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含为获得南京邮电大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。研究生签名：隧避缢日期：逊：丝匹南京邮电大学学位论文使用授权声明南京邮电大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学位论文的复印件和电子文档，可以采用影印、缩印或其他复制手段保存论文。本人电子文档的内容和纸质论文的内容相一致。除在保密期内的保密论文外，允许论文被查阅和借阅，可以公布( 包括刊登) 论文的全部或部分内容。论文的公布( 包括刊登) 授权南京邮电大学研究生部办理。研究生签名：隧避缓导师签名：南京邮电大学硕士研究生学位论文第一章绪论1 1 研究背景第一章绪论通信协议是网络和分布式系统中两个或多个实体间相互通信时所必须遵守规则的集合，是网络的重要组成部分。近年来，随着计算机通信和网络技术的不断提高，网络系统的复杂性在协议方面体现出空间分布性、并发性、异步性、不稳定性和多样性。这不仅意味着协议开发难度大，周期长，而且潜在错误多，开发过程中任何一点错误和缺陷都将给通信系统的稳定性、可靠性、坚固性、安全性、容错性以及系统之间互通性和互操作性带来巨大的危害。因此，需要合适的方法、技术和计算机辅助工具，使协议开发过程工程化，以便提高协议的开发效率，促进标准化的协议实现，由此产生了协议工程( p r o t o c o le n g i n e e r i n g ) 【1 】学科，它涉及到计算机科学与工程的各个分支。所谓协议工程，是指一体化和形式化的协议开发过程。它的宗旨是为协议软件的研制和开发提供一整套工程规范。一体化即系统化，其含义是：协议的设计、验证、实现和测试，在技术上前后衔接，并在同一个开发系统中完成。而形式化，是指将协议以及由协议提供的服务用形式化描述方法( f o r m a ld e s e f i p t i o nt e c h n i q u e s ：f d t ) 描述出来。它包括了以下六个过程：1 ) 协议设计：p d u 格式，协议机制，服务原语等设计；2 ) 协议描述：用某种语言确切地描述协议元素；3 ) 协议验证：对所描述的协议验证其正确性；4 ) 协议实现：根据描述的协议产生网络硬软件；5 ) 协议测试：对实现的协议进行测试；6 ) 协议维护：对网络硬软件进行维护。南京邮电大学硕士研究生学位论文第一章绪论1 协议设计i非形式化描述文本形式化描述上试化宁模型协议实现图1 1 协议工程流程图在这些形式化技术中，形式化描述与验证技术是整个协议设计与实现的基础。对协议实现的正确性、完整性和复杂度有至关重要的影响。形式化描述方法是协议工程的核心技术之一，它是协议工程的基础。协议正确性验证必定基于形式化描述方法，所以，利用形式化的描述方法( 包括模型技术及形式描述语言f d l ：f o r m a ld e s c r i p t i o nl a n g u a g e ) 描述协议，是进行正确性验证和协议测试的前提。协议验证( p r o t o c o lv e r i f i c a t i o n ) 是协议工程的重要组成部分，是对通信协议本身的逻辑性和正确性进行验证的过程。它处于协议工程中协议设计阶段之后，协议实现阶段之前。其工作过程一般是通过选择合适的形式化描述方法对协议进行形式化描述，然后用基于数学的方法，检验或证明协议设计的逻辑j 下确性。1 2 研究现状1 2 1 形式描述技术目前己经开发出大量的，种类繁多的形式化描述方法，并被应用到系统开发当中。常用的通信协议的形式化模型方法有有限状态机( f s m ) 模型，p e t r i 网模型、通讯进程验算( c o s ) 等模型技术。常用的通信协议形式化描述语言有s d l 语言，e s t e l l e 语言，l o t o s 语言。有限状态机( f i i l i t es t a t em a c h i n e ：f s m ) 【2 】是最常用的协议形式化描述技术。有限状态机2南京邮电大学硕士研究生学位论文第一章绪论通常使用状态转移图( s t a t et r a n s i t i o ng r a p h ：s t g ) 来表示。状态转移图是一个有向图，节点代表状态，有向边代表状态转移。它的每一条有向边都标记了输入和输出。还有一些对有限状态机的扩展，如通信有限状态机( c o m m u n i c a t i o nf i n i t es t a t em a c h i n e ：c f s m ) 和l 扩展有限状态机( e x t e n d e df i n i t e s t a t e m a c h i n e ：e f s m ) 等等。p e t r i 网( p e t r i n e t ：p n ) 在通信领域得到了广泛的应用。p e t r i 网可以清楚的表达两个进程之间的通信，它也可以用作其它形式化描述方法的辅助方法。通过增加一些特殊模型，p e t r i网也有多种扩展，包括数字p 弧网( n u m e r i c a lp e t r in e t ：n p n ) 、有色p e t r i n - - ( c o l o u r e dp e t r in e t ：c p n ) 和时间p e t r i 网( t i m ep e t r in e t ：t p n ) 等等。s d l ( s p e c i f i c a t i o na n dd e s c r i p t i o nl a n g u a g e ) 语言是由c c i t t ( i t u - t ) 组织开发的电信领域的国际标准。它的数学模型是扩展有限状态机模型( e f s m ) ，它可以精确描述一个系统的动作特征。l o t o s ( l a n g u a g eo f t e m p o r a lo r e d e r i n gs p e c i f i c a t i o n ) 是眭l i s o 组织开发出来的语言。l o t o s 的基本思想是：一个通信系统可以描述成为一系列有时间顺序的可以由外部观察到的事件。l o t o s 是用通信系统验算( c a l c u l u so f c o m m u n i c a t i o ns y s t e m ：c c s ) 来描述进程的行为和交互，并且使用a c to n e 语言来描述数据结构和表达式。e s t e l l e 也是由i s o 组织开发的一种语言，它也是基于扩展有限状态机模型( e f s m ) 的。e s t e l l e 语言使用p a s c a l 作为基础，并且将之扩展以描述系统的细节、进程的并发和进程间的通信。它通常被用作描述分布式系统和并行信息处理系统。每一种语言均有其优点，但是e s t e l l e 和l o t o s 有三个弱点：( 1 ) 语义需重新定义；( 2 ) 缺乏分析技术；( 3 ) 实现不具有独立性。因此本文使用的是s d l 语言，主要原因是它能提供形式语义，保证描述不存在二义性，便于验证和一致性测试理论的研究。1 2 2 协议验证技术协议验证【3 l 的主要目的是试图在协议开发的前期最大限度地检测和纠正协议错误和缺陷，包括死锁( d e a d l o c k ) 、活锁( 1 i v e l o c k ) 、不可执行地行动、协议外部性能不符合服务要求等。只有通过正确性验证的协议，才能有保障地进行协议实现，继而对协议实现进行测试。协议有多种表达形式，这包括用自然语言描述的非形式话协议文本，用形式化描述语言( e s t e l l e ，l o t o s ，s d l 等) 描述的协议规范，用协议模型技术( f s m ，p e t r i n e t ，c c s 等)表达的协议模型，以及用程序设计语言描述的协议代码。协议验证可在任何种表达形式上进行，一般的说，通常在协议模型或形式化描述语言描述的协议规范上进行协议验证( 简南京邮电大学硕士研究生学位论文第一章绪论单，容易形成算法) 。协议验证技术多种多样，但主要可以分为两类：逻辑证明( l o g i cp r o o f ) 可达性分析( r e a c h a b i l i t ya n a l y s i s )逻辑证明用推理验算的方法严密地证明各种协议性质，所采用的技术要来自于时态逻辑、谓词逻辑、代数验算等数学领域。可达性分析是最常用的技术，是一种传统的、易于自动化处理的、有效的协议验证方法。但可达性分析需要从初始状态开始，枚举协议中的所有可达状态，随着通信协议的复杂性的不断增加，它所面临的状态爆炸问题( s t a t ee x p l o s i o np r o b l e m ) 也随之变得越来越突出。为了缓解状态空间爆炸问题，现在已提出大量的各种各样的改进技术。如：随机状态搜索( r a n d o m w a l ks t a t ee x p l o r a t i o n ) ，最大化前进状态搜索( m a x i m u mp r o g r e s s s t a t e e x p l o r a t i o n ) 等等。1 3 研究内容和论文结构本文将对协议工程的形式化描述方法和协议验证作详细的分析和研究，并以i e t f ( i m e m e te n g i n e e r i n gt a s kf o r c e ) 组织提出的一个在基于i p 网络中，特别是在i n t e m e t中实现实时通信应用的信令协议s i p ( s e s s i o ni n i t i a t i o np r o t o c o l ，会话发起协议) 为例，从理论到实践研究了协议的形式化开发过程，实现了对协议工程的相关理论的应用。本文利用t e l e l o g i ct a u 工具软件对s i p 协议的通信流程进行了形式化描述，然后利用工具软件中的s i m u l a t o r 对协议模型进行了仿真，证明该协议模型基本实现了协议规范描述的功能，最后在v a l i d a t o r 环境中，采用不同的自动验证算法对协议模型进行了验证，保证了该s i p 协议模型设计的正确性。为了减少开发成本，在形式化描述的建模阶段采用验证方法来验证模型是很有必要的。可达性分析是最常用的技术，但它所面临的状态爆炸问题限制了其使用范围。为了缓解状态空间爆炸问题，现在已提出大量的各种各样的改进技术。最大化前进状态搜索方法就是其中之一，该方法将状态搜索的任务分成两个独立的子任务，这两个子任务可以并行进行，所需的执行时间和内存通常会少很多。但经研究发现，该方法中存在着重复性工作，本文将提出一种改进方法来解决该问题，进一步节省时间和空间，并通过对s i p 协议模型的验证分析显示该方法的优越性。本文的组织结构如下：4南京邮电大学硕士研究生学位论文第一章绪论第一章绪论，阐述了协议工程的定义，并对形式化描述和验证技术做了简要的介绍。第二章协议形式化描述方法，主要讨论了几种状态机模型，如有限状态机，扩展有限状态机，通信有限状态机等。并重点介绍了形式化描述语言s d l 。第三章协议验证技术，本章节主要研究了基于f s m 模型的可达性验证技术，介绍了传统可达性分析方法以及两种缓解状态空间爆炸问题的改进方法。第四章s i p 协议介绍，系统地概述了s i p 协议基本特点、协议结构和消息流程，为后面的设计和实现提供了理论依据。第五章基于s d l 的s i p 协议形式化描述，本章节利用s d l 语言在t a u 平台上实现了对s i p 协议的描述，仿真以及验证。第六章基于最大化前进状态搜索的改进算法。在现有技术的基础上，提出了一种新的改进技术。还通过改进的方法实现了对s i p 协议状态机的验证，在此基础上阐述了改进方法的优越性。第七章总结，对本次论文工作进行总结。南京邮电大学硕士研究生学位论文第二章协议形式化描述方法第二章协议形式化描述方法2 1 形式化描述模型协议模型技术是协议工程的核心技术之一，它是协议工程的基础。形式描述语言总是以某种模型技术为基础，协议的正确性验证必定基于某种模型技术，协议自动化实现以及协议测试等都以某种模型技术为基础。目前，协议工程所采用的模型技术全部来自数学家以及计算机科学理论家所提出的一些数学模型( 或方法) 和自动化模型( 或程序模型) ，从事协议工程的学者也许会提出一些新的模型。常用的通信协议的形式化模型方法有有限状态机模型f s m ( f i n i t es t a t e m a c h i n e ) ，p e t r i 网( p e t r i n e t ：p n ) ，通讯进程演算( c a l c u l u so f c o m m u n i ct e m p o r a l a t i n g s y s t e m s ：c c s ) 等【4 】o2 1 1 有限状态机f s m2 1 1 1f s m 的基本定义f s m 是一种数学模型，包括以下几个部分：一个有限状态集，用于描述系统中的不同状态；一个输入集，用于表征系统所接收的不同输入信息；一个状态转移规则集，用于表述系统在接收不同输入下从一个状态转移到另外一个状态的规则。有限状态机可由如下形式定义给出：定义：有限状态机是一个五元组m = ( q ，6 ，9 0 ，f ) ，其中( 1 ) q = q 0 ，q 。，以) 是有限状态集合。在任一确定的时刻，有限状态机只能处于一个确定的状态仍；( 2 ) y t - o 。，o ：，o 。 是有限输入字符集合，在任一确定时刻，有限状态机只能接收一个确定的输入0i ：( 3 ) 6 ：q _ q 是状态转移函数，如果在某一确定的时刻，有限状态机处于某一状态g q ，并接收一个输入字符q ，那么下一时刻将处于一个确定的状态9 7 = 6 ( 吼，q ) 。在这里规定q = 万( g ，s ) ，即：对任何状态q ，当读入空字符占时，有限状态机不发生任何状6南京邮电大学硕士研究生学位论文第二章协议形式化描述方法态转移；( 4 ) q 。q 是初始状态，有限状态机由此状态开始接收输入；( 5 ) f q 是终结状态集合，有限状态机在达到终态后不再接收输入。2 1 1 2 扩展有限状态机e f s m一个扩展的有限状态机m 可以表示为一个五元组m = ( q ，i ，o ，t ，x ) ，其中：1 ) q = q 。，q 。，吼) 是有限状态集合；2 )i = f l ，之，乙) 是有限输入字符集合；3 ) 0 = 0 。，0 2 ，0 ，) 是有限的输出字符集合；4 ) t = ( q ，吼，d ，4 ) 为变迁集合，其中吼( q 。q ) 是变迁的起始状态，q ，( q ，q ) 是变迁的终止状态，( f f i ) 和o ，( d ，0 ) 分别表示变迁的输入和输出。( x ) 表示与当前状态的变量集x ( x e x ) 相关的谓词约束，4 ( x ) 表示与当前状态的变量集x ( x e x ) 的赋值操作。表示如f ：吼寺g ，；5 ) x 为变量集合。a ，1x-o，眨二3 兢图2 1e f s m 状态图通过对e f s m 的分析可以看出，e f s m 与f s m 最大的区别在变量：谓词约束和赋值动作。e f s m 是f s m 的一种简化了的表示方法，e f s m 中的状态可以抽象化为一组状态配置的结合体，其变量可在相应的值域范围内进行取值，同时，由于受到谓词约束的影响，对e f s m 中的状态而言，并不是每一条指出的变量都是可以被触发的。从变迁可触发性的角度而言，如果将e f s m 中所有变迁的谓词约束置为永真( t r e e ) ，那么e f s m 相应也就变成了一个f s m ，这便是对e f s m 进行可达性分析的原则。7南京邮电大学硕士研究生学位论文第二章协议形式化描述方法2 1 1 3 通信有限状态机c f s m一般情况下，很难用一个状态机描述现实世界的系统，往往是先把系统分解成多个功能比较单一，相互独立的子系统，每一个子系统用一个状态机描述，所有的状态机构成一个大系统，因为是多状态机，所以称为m f s m ( m u l t if s m ) ，又因为多状态机之间要相互通信，也称为通信有限状态机( c f s m ) 2 1 。通信有限状态机和前面定义的f s m 相似：它接收输入消息，产生输出消息，并根据一些预定的方案改变内部状态。所不同的是：c f s m 包含多个有限状态机，状态机之间通过有界的先进先出( f i f o ) 队列通信，队列用来把一个状态机的输出映射到另一个状态机的输入上。为了支持通信有限状态机，我们先引入消息队列的定义。一个消息队列是一个三元组 ，每个元素的含义如下： s 是队列的符号集，是一个有限状态集； n 是一个整数，定义队列的长度； c 是队列的内容，它是s 中成员的一个有序集。我们称s 和c 的成员为消息。每一条消息都有一个唯一的名字。现在，我们可以使用上面定义的队列来定义c f s m 。c f s m 可以看成一个四元组 ，每个元素的含义如下： s 是一个有限的，非空的状态集； 是初始状态； q 是上面定义的队列； t 是状态转移关系。状态转移关系t 表示在一个状态下，从队列收到一条消息后对应的动作，即它表示状态，消息和动作( a c t i o n ) 的关系，也可以说成：t 以当前状态和消息作为参数，产生一个动作。这里的动作包含对消息的处理，产生的输出，状态的转移。2 1 2p e t r i 网p e t r i 网是1 9 6 2 年由德国的c a p e t r i 在他的博士论文“c o m m u n i c a t i o nw i t ha u t o m a t a ( 用自动机通信) 中首次提出网状结构的信息流模型。p e t r i 的这一工作引起了美国和欧洲一些科学家的重视，a w h o l t 随后在他的“f i n a lr e p o r to ft h ei n f o r m a t i o ns y s t e mt h e o rp r o j e c t 和“e v e n t sa n dc o n d i t i o n 论文中用p e t r i 网模拟和分析了具有并行分支的系统，8南京邮电大学硕士研究生学位论文第二章协议形式化描述方法并称这种网状结构为p e t r in e t s ，以后这个名字为大家所接受。p e t r i 网理论是在并发的概念上建立起来的，它直观地表示了非确定性，可用于表达不同抽象级上的系统概念。p e t r i 网能用许多方法构造，例如，用简单c h a n n e l a g e n c y 网来表示系统结构，在逐步求精后定义系统的行为。p e t r i 网通常表示为一种物理系统极为相近的图形形式，使人们能够比较容易地学习和理解这种描述语言。p e t r i 网有一套成熟的数学理论工具，建立了许多分析技术，包括可达性分析、不变量分析( 使用线性代数方法) 、保持特性的变换( 包括化简) 以及网的分解和等价。网的形式基础使网与其他并发模型建立了连接，这对于分布式系统的描述和分析是很有益的。近几年来，人们的注意力集中在如何将代数的抽象数据类型融合在高级网结构中。p e t r i 网是一种非常优秀的图形化的形式化模型，直观、易懂和易用，适合于描述并发和分布式系统的动态行为，使用p e t r i 网的分析技术对模拟系统进行分析，能得到系统行为方面的信息，具有坚实的数学基础和分析技术。运用p e t r i 网进行的系统验证主要有检测死锁、活锁等。但是，p e t r i 网缺乏建模能力，以及数据抽象和提炼的技巧，而且p e t r i 网不能区分系统的内部事件和外部事件，因此它在刻画复杂系统时会显得异常繁琐，也不利于描述协议的进展情况，当进行大型复杂协议的构造时，p e t r i 模型也将面临状态爆炸的问题。2 1 3 通讯进程演算( c c s ) 模型进程代数是- - f 3 2 0 世纪八十年代才发展起来的数学，r m i l e r 在这方面作了开拓性工作，并因此荣获1 9 9 1 年的图灵奖。他的通讯进程演算c c s 已在协议工程等领域内得到重要的应用，是所有进程代数的基础。以c c s 为基础，其它学者也提出了一些进程代数，其中比较成熟的是通讯顺序进程c s p ( c o m m u n i c a t i n gs e q u e n t i mp r o c e s s e s ) 。c c s 用三个基本算子定义一个进程，这三个算子是： 顺序算子：用于描述进程顺序执行事件的行为，一个进程既使同时执行多个事件，观察者也可以将它们按顺序描述。顺序算子用句点“ 表示； 选择算子：用于描述进程从多个事件中选择执行一个的行为，用符号“+ 表示； 并行算子：也称组合或并发算子，用于将多个进程组合成一个进程，用符号“i 表示，并行算子不能用于事件。以上三个基本算子过于简练，它不能表达实际进程的复杂行为。引入附加算子或三个基本算子的变种算子可大大提高c c s 的表达能力。c s p 定义的算子比c c s 多，且大多都是c c s 基本算子的变种算子。一般地说，算子越多，表达能力就越强，代数变换规则就丰富。9南京邮电大学硕士研究生学位论文第二荦协议形式化描述万法表达式的等价变换规则是代数系统的核心。在c c s 中，表达式的变换规则基于“观察等价：即对外部观察者来说，如果进程执行两个表达式所表现的行为是不能区分的，那么这两个表达式是等价的。由于c c s 的代数变换规则是基于较强的“观察等价 原则，可以得出结论：用c c s 证明是正确的协议一定是正确的协议，反之不一定。从c c s 的表达式可判定协议是否有活动性、安全性、一致性和完备性，因此可用于验证协议，判定协议的正确性。进程执行事件的记录叫做迹，它可用图表示。c c s 的迹和f s m图或p e t r i 网有很好的映射关系，可以从f s m 图和p e t r i 网中得出c c s 描述。2 2 形式化描述语言标准化组织如i s o 和c c i t t 开发了一些形式化描述语言，目前较流行的有如下三种： e s t e l l e ：e s t e l l e 由e s t l ( e x t e n d e ds t a t e t r a n s i t i o nl a n g u a g e ，扩展的状态转换语言)而得名，基于e f s m 模型，它能够完整地描述协议的控制行为和数据行为，可以把系统描述为具有层次结构的一些相互通信的模块，能够用来描述o s i 中的各服务和协议； l o t o s ：即l a n g u a g ef o rt e m p o r a lo r d e r i n gs p e c i f i c a t i o n ( 时间次序描述语言) 。l o t o s也是国际标准化组织i s o 为分布式系统或并行处理系统开发的一种形式描述语言，可以用来描述并行、不确定、同步和异步系统，并且支持多种层次的抽象，提供多种说明类型。l o t o s 的基本描述对象是并行进程，这些进程的行为用它与外部环境之间的交互动作序列来描述。它特别适于用来描述o s i 中的服务和协议。l o t o s 和其他基于状态的形式描述技术不同，它是通过描述外部事件的时序关系来描述系统的。它由基于c c s 和c p s 的进程代数部分( p r o c e s sa l g e b r a i cp a n ) 和基于抽象数据类型语言的数据代数部分( d a t aa l g e b r a i cp a r t ) 组成。进程代数部分描述系统的动态行为，数据代数部分描述系统的数据结构和变量。 s d l 即规范说明与描述语言。该语言基于扩展的有限状态自动机( e f s m ) 模型，特别适合于描述软件系统的离散过程。s d l 既适用于通信软件概要设计阶段，也适用于详细设计阶段。由于已有工具支持s d l 到c 语言或c + + 语言的翻译，即代码自动生成，使得s d l 语言在通信软件设计中得到越来越多的应用。本课题采用s d l 语言对s i p协议的核心功能进行形式化描述。下面详细讨论s d l 。1 0南京邮电大学硕士研究生学位论文第二章协议形式化描述方法2 3 规范说明和描述语言s d l规范说明和描述语言s d l l 5 1 是一种应用较广的形式化描述语言，由原来c c i t t ( 国际电报电话咨询委员会) 现i t u t ( 国际电信联盟电信标准局) 制定形成z 1 0 0 建议，第一版形成于1 9 7 6 年，1 9 8 0 - 1 9 9 2 年又推出了多个版本。1 9 9 9 年1 1 月i t u t 推出了s d l 2 0 0 0 版，该版本在面向对象的数据方面做了扩展：为了使s d l 语言更简炼，合并了部分特性。2 3 1s d l 的基本概念在协议软件的开发流程中，s d l 被应用在系统规范描述和设计阶段。t e l e l o g i c t a u 公司提供的s d l 软件不仅可以用于规范描述和设计，它还可以把s d l 的描述和设计直接生成标准的c 代码，用户也可以直接在s d l 描述和设计中嵌入c 代码，从而完成“实现 部分的功能。s d l 系统的理论模型是基于有限状态机( f s m ) 的【6 1 ，各个进程将并行处理，进程间使用信号传递信息。除用于协议软件的描述及开发外，s d l 还被广泛用于其他些如工业进程控制、交通控制等领域。事实上，凡是能够由e f s m 模型有效模拟的领域都可以用s d l 。作为规范描述语言，s d l 具有两种不同的形式，但两者都建立在同样的语意模型之上。一种是图形文法定义( s d l 佑r ) ，它的基础是一套标准化的图形符号；另一种是文本文法定义( s d l p r ) ，这两种文法是完全等效的。图形文法直观易懂，便于交流，适合于设计开发人员使用，而文本文法更适合于机器理解。一般的开发工具都支持图形编辑，然后把s d l g r 转换成s d l p r ，最后再翻译成编程语言的源代码。本文主要以s d l g r 图形文法为主。2 3 2s d l 结构用s d l 设计的系统是一个等级结构的系统，它包括系统( s y s t e m ) 、功能块( b l o c k )和进程( p r o c e s s ) 等。一个系统可以包含多个块，每个块可由一个或多个进程组成，进程是s d l 系统中的最小处理单元，采用e f s m 来描述，所有用户的处理和操作都在进程中完成。在系统级下定义的内容( 信号、数据结构等) 可以在该系统下所有的块和进程中使用，在块下定义的内容可以在该块下的任何进程中使用。南京邮电大学硕士研究生学位论文第二章协议形式化描述方法p r o c e s sp 1r 。一。ii ii-_-图2 2s d l 结构图 系统系统是由许多用信道连接起来的功能块组成。每个功能块相对于其它功能块而言是独立的。在两个不同功能块的进程之间，通信的唯一手段是发送信号。信号通过信道来传递。把系统适当地分成几个功能块的依据是：其大小规模便于处理；能与实际的软件( 硬件) 划分相适应；与自然的功能划分相一致；把交互作用减少到最小。 功能块顾名思义，功能块被用来对系统内的不同功能进行划分，按功能把一些进程合理地组合在一起。系统设计时，应先把系统( 或功能块) 分解成功能单位，然后再定义功能块里的诸进程。在功能块内部，进程间可通过信号或共享值来相互通信。这样，功能块不仅提供了一种把进程组合起来的合适机构，也提供了数据可见性的边界。在功能块内部，能够定义诸进程之间的通信路径，或是进程与功能块的环境之间( 即功能块边界) 的通信路径，这1 2南京邮电人学硕士研究生学位论文第二章协议形式化描述方法种通信路径称为通信路由。 信道信道是系统的不同功能块之间或功能块和环境( 属于s d l 系统描述之外的部分) 之间进行通信的手段，一条信道可以是单向地或双向地将一个功能块连接到另外的一个功能块或者连接到环境。通常信道是一种功能性的实体，可用来表示特定的信息通路。 信号信号用来在不同进程或不同实例之间传递信息。信号可以在系统层次、功能块层次或进程的内部来定义，在进程内部定义的信号只能在同一进程内的诸实例间互相交换。在某个层次上定义的信号可以在该层次上和较低级的层次上使用。 信号路由与信道相类似，信号路由也用来表示通信路径。它们可使用在功能块层次上，也可以使用在进程层次上。和信道一样，信号路由可以是单向的或双向的。在功能块层次上，它们表示一种在功能块诸进程之间或在进程、功能块与环境之间通信的手段，这里功能块环境也就是通向或离开功能块的一条信道。在进程层次上，信号路由可用在将进程分解成服务子结构的场合。在这种情况下它们把服务互相连接起来，或把服务连接到进程的信号路由上。当一个信号被传到通向功能块边界的一条信号路由时，该信号即被交付给连接到该信号路由的信道。当一个信号从一条信道到达功能块，且该信道连接到一条或多条信号路由时，该信号即传向能够传递该信号的信号路由。 进程进程是一种扩展的有限状态机，它规定一个系统的动态行为。进程基本上都处于等待接收信号的状态。当收到一个信号时，进程作出响应，执行特定的动作。一个进程可以包含许多不同的状态，使它们收到一个信号( 甚至是同一信号) 时能执行不同的动作。这些状态提供了对早先己出现过的动作的记忆。在完成相应的动作之后，就进入到下一个状态，这时进程又等待接收下一个信号。进程可以在系统创建时就存在，或者因另一进程发出创建请求而被创建。进程能够一直生存下去，也可以执行一个停止动作而停止。进程主要由状态、输入、保存和输出等要素组成。过程s d l h h 的过程类似其它编程语言中的过程。在s d l 规范中。过程可以在所有的层次( s y s t e m ，b l o c k ，p r o c e s s ) _ k 定义。在一定层次上定义的过程只能在该层次及其以下的层次上1 3南京邮电大学硕士研究生学位论文第二章协 义形式化描述方法使用。2 3 3 数据处理s d l 数据类型是抽象数据类型( a b s t r a c t d a t a t y p e s a d t ) ，即数据取值与数据相关操作的集合。预定义的抽象数据类型有布尔型，整型，实数，字符，字符c h a r s t r i n g ，位b i t ，位b i t s t r i n g ，字节o c t e t ，字节o c t e t s t r i n g ，以及进程识别号p i d ( p r o c e s si d e n t i f i c a t i o n ) ，时间点t i m e ，时间段d u r a t i o n 等等。p i d 用来指示某个进程实例，初始状态只有一个字面值：n u l l ，其它值通过s d l 预定义的变一e l f s e n d e r ，p a r e n t 和l o f f s p r i n g 得到。基于这些预定义的s d l 数据类型，开发人员还可自定义一些专用数据类型，对此s d l提供了关键词n e 咖e 和e n d n e y p e ，表达式如下所示：n e w t y p ee x a m p l e ls t r u c ta i n t e g e r ；bc h a r a c t e r ；e n d n e w t y p e ；n e w t y p e 定义引入了一种独立的数据类型，不与其它类型兼容。因此，若定义另外一个n e w t y p e ，即使二者实际内容完全一样，两种类型对应的变量之间也不能相互赋值。s d l 语言还提供了其它关键词如s y n t y p e ，表达式如下所示s y n t y p ee x a m p l e 2 = i n t e g e rc o n s t a n t s0 ：1 0e n d s y n t y p e ；e x a m p l e 2 也是整型，但此类型的变量取值只在s y n t y p e 定义的范围之内，定义 的c o n s t a n t语句就是值域条件，编译s d l 系统时将检查这些值域条件。没有值域限制的s y n t y p e 定义只是为原类型引入了新的名称。此外，s d l 还支持结构、数组等类型，同时提供- j i n h e r i t sb i t f i e l d ，s t r i n g 等形式扩充了可使用的数据类型。s d l 还支持用户通过增加新操作来定义新类型，基本表达形式如下例所示：n e w t y p ec o o r d i n a t e ss t r u c tai n t e g e r ；bi n t e g e r ；a d d i n g1 4南京邮电大学硕士研究生学位论文第二章协议形式化描述方法o p e r a t o r s+ ：c o o r d i n a t e s ，c o o r d i n a t e s c o o r d i n a t e s ；l e n g t h ：c o o r d i n a t e s - r e a l ；e n d n e w t y p e ；尽管s d l 有如此丰富的数据类型定义可供开发者使用，其数据处理能力远不如进程描述能力强。而且基于s d l 的开发工具一般不支持全局变量的使用，不方便使用指针、线性链表等非常灵活的方式，因此实际开发过程中采用了内嵌c 代码方式来弥补不足。2 3 4s d l 中的时钟处理时钟在通信系统中具有重要的作用，在s d l 中时钟操作是一种特殊的动作。一个时钟经过设置( s e t ) ：a 能进入活动状态。设置时钟时要带有一个具体数值作为时钟超时周期，一旦超时，系统将发出一个超时消息，同时时钟进入不活动状态。对活动的时钟进行设置，时钟将继续处于活动状态，但是具有新的超时时间值。重置( r e s e t ) 时钟将导致时钟进入不活动状态。时钟声明为t i m e r 类型的变量，s d l 系统中还有两种与时钟有关的特殊的数据类型t i m e和d u r a t i o n ，分别表示时间点和时间段的概念。t i m e 类型的表达式 n o w + d ”表示未来的一个时间点，即操作符n o w 返回的当前时间经过d u r a t i o n 类型的变量d 表示的一段延时后的时间点。如果设置一个时钟时带上变量“n o w + 5 ，表示从当前时间点开始5 秒钟后时钟将超时。超时消息是s d l 系统的一个内部消息，但是对于进程而言，超时消息与其它消息并没有区别。通信系统中常常要用到时钟，对系统的某些处理加上时间限制，比如各种请求的响应，等待已丢失的数据等，如果没有时钟机制，进程会由于没有响应而陷入无限等待，导致整个系统没有响应。南京邮电大学硕士研究生学位论文第三章协 义验证技术3 1 概述3 1 1 协议验证的定义第三章协议验证技术对协议本身的逻辑正确性进行校验的过程称为协议验证( p r o t o c o lv e r i f i c a t i o n ) ，它是协议工程的重要组成部分。协议验证处于协议工程中协议设计阶段之后，协议实现阶段之前。