（计算机软件与理论专业论文）一种基于csp的协议模型技术的研究.pdf

主璺型堂垫查叁堂塑! ：兰堡垒竺 摘要 2 5 1 5 3 d 协议工程是形式化的协议开发过程，它使用形式化的方法束描述协议的设 计和维护中的各个活动，它是研究对象为通信协议的软件工程。协议工程的核心 部分是通信协议的形式化描述技术。 目f ；i ，常用的协议形式化描述技术主要包括：有限状态机( f s m ) 模型、 p e t r i 网模型；以及e s t c l l e 语占、l 0 1 d s 语言和s d l 语言等形式化描述语言。 这些方法各有优点和缺点，因此，非常有必要继续研究和探索这一领域的新理论 和新方法。 本文对通信顺序进程c s p 做了深入的研究，对它进行了扩充，在协议建模 和协议验证等各个方面进行研究，以拓展对这一领域的探索，推动协议形式化理 论的发展。 本论文的主要工作包括： 1 研究和分析比较了目f ；i 常用的协议形式化描述技术的特点。 2 深入研究和分析了c s p 的背景和特点。 3 通过实例深入研究了协议的c s p 模型的具体描述，总结了用c s p 建立模 型的大概方法。 4 针对一种新的形式化描述方法r s l 的特点，我们研究出一套从c s p 模型 到r s l 语言转换的规则和步骤，将协议模型和协议描述语言紧密结合。 5 对c s p 在协议验证上作了初步的研究，用严密的代数演算方法验证协议 性质。并且针对c s p 的不足，对它进行扩充，使它能够更方便的用于协 议描述。 6 本文还对f s m 模型到c s p 模型的转化以及测试用例的生成作了初步的研 究。 关键词：协议工程，形式化描述技术，c s p ，协议验证，协议测试 种培十c s p 的协淡攘型技术的研究 第i 虹 ! 堕型兰丝查叁兰! 坐! ：兰垡垦皇； 一一 a b s t r a c t p r o t o c o le n g i n e e “n gi saf o m 试p f o t o c o id e v e l o p m e n tp r o c e s s i t d e s c r i b e s f u n c i o n so fp m o c 0 1 d e s i g n a n dm a i n t e n a n c ew j t hf 0 册a lt e c b n j q u e ，w h i c h i s s o f t w a r ee n g i n e e “n go fc o m m u n i c a t i o np r o t o c 0 1 t bf o m a l i z et h e s es t e p so fp r o t o c o l e n g i n e e r i n g ，d i 仃e r e n tf o m a ld e s c r i p t i o nt e c h n i q u e s ( f d t ) a r e u s e d c u r r e n t l y t h ef d to fp r o t o c o l si nc o m m o nu s ei n c l u d ef i n i t es t a t em a c h i n e ( f s m ) m o d e l ，p e t r in e tm o d e i ，a n df o r n l a ld e s c r p t i o nl a n g u a g e s ( f d i 。) s u c ha s e s t e l l e l o t o s ，a n ds d l b e c a u s ed i 肫r e n tt c c h n i q u e s h a v ed i 肫r e n ta d v a n t a g e s a n dd i s a d v a n t a g e s ，i ti sn e c e s s a r yt od of u r t h e rr e s e a r c ha n de x p l o r en e wt h e o r ya n d n e w t e c h n i q u e si nt h i sf i e l d t h i sp a p e rd o e sad e e pa n de x t e n d e dr e s e a r c ho nt h ec o m m u n i c a t i n gs e q u e n t i a l p m c e s s e s ( c s p ) d i f r e r e n ta s p e c t s o fp m t o c o lm o d e l i n ga n dp m t o c o lt e s t a r e r e s e a 站h e dt oe x 把n dt h ee x p i o r a t i o no nt h i sf i e l d 锄dp r o m o 把c h ed e v e l o p m e n to f p r o t o c o lf o m l a l i z a t i o nt h e o r y t h i sp a p e rm a i n l yf o c u s e so nt h ef o l l o w i n gi s s u e s ： 1 a n a l y z ea n dc o m p a r et h ec h a r a c t e r i s t i c s o ft h ec u 玎e n t p o p u i a r f d to f p r o l o c o l s 2 d e e p i y r e s e a r c ha n da n a b ，西et h eb a c k g r o u n da l 【1 dc h a t e d s t i c so f c s p - 3 d e e p l yr e s e a r c h t h ed e t a i k dd e s c r i p t i o no fc s pm o d e l so fp r o t o c o l sb y p m c t i c a le x 鲫n p l e s ，a n ds u m m a r i z e t h eg e n c r a lm e 山o d st ob u i l dm o d e l sw i t h c s p 4 a c c o r d i n g t om ec h a r a c t e r i s t i c so f r s l ，a n e wf d t ，w eh a v ed e v i s e das e to f r e g u o n s 鲫ds t e p st ot 啪s f o n nc s p m o d e l st or s l l a i l g u a g e s ，w h i c hl i n k t h ep r o t o c o im o d e l sa n dt h ep r o t o c o id e s c r i p t i o ni a n g u a g e sc l o s e l y 5 d oe l e m e n t a r yr e s e a r c ho np r o t o c o la u m e n t i c a t i o nf o rc s p ，a n dv e r i 母t h e p r o t o c o lp r o p e r t i e s w i m r i g o r o u sa l g e b r a m e t h o d s a i m i n g a tt h e s h o r t c o m i n 盼o fc sp e x p 趴d t ol e ti tm o r ec o n v e n i e n tf o r p r o t o c o i d e s c r i p t i o n 6t h i sp a p e ra l s od o e se l e m e n t a r yr e s e a r c ho nh o wt oc o n v e nf s mm o d e l st o c s pm o d e i sa n dh o wl og e n e r a l et e s tc a s e s k e y w o r d s ：p r o t o c o l e n g i n e e r i n g f d r m a l d e s c r p t i o n t e c h n o l o g y ， c s p p f o t o c a fa u t h e n t i c a t i o n ，p r o t o c o lt 色s t i n g 种旌l 。c s p 的协议模j 掣技术的究筇i i 虹 中闭科学技术人学f | ；! i j 学位论义 第一章引言 1 1 研究背景 最近二：十年，随着计算机硬件技术的进步，通信网络技术得到了迅速的发展。 协议是计算机网络和通信网络中各种通信实体或进程问相互交换信息所遵守的 一组j ；! l ! 则。为了给网络硬件，软件、协议，存取控制和拓扑提供标准，国际标准 化组织i s o 提出了j r 放系统! i 联i s 0 0 s i 参考模型【l 】。而另一方面，以t c p i p 协议为核心的i n t e m e t 网络体系结构捌有更广泛的用户，成为了事实的计算机网 络工业标准f 2 1 。 随着计算机网络和通信网络的闩趋复杂，协议的种类和数量越来越多，其规 模也越来越大，如何设计出功能上讵确可靠，逻辑上一致完整的通信协议，并且 系统的进行协议实现，协议验证和协议测试，已经成为了一个非常具有挑战性的 课题。 协议足计算机通讯，计算机网络，多机系统等分布系统的灵魂，其丌发过 程包括协议设计与描述，协议验证与分析，协议实现，协议测试等几个主要阶段。 分仰系统的主要特征是分柿性，并发性，异步性，实时性以及信道的不可靠性。 这些特征意味着协议本身一定是复杂的。随着计算机网络和分布式系统的发展， 特别是丌放性异构的互联，协议本身的复杂性越来越高，提供的服务越来越丰富， 不同系统的互通能力和互操作能力也越来越强。这些都进一步增强了协议的复杂 性。而复杂的协议不但意味着协议的丌发难度大，周期长，而且分布系统产品中 的潜在错误多，而协议丌发过程中任何一点错误和缺陷都将给分布系统的稳定 性、可靠性、安全性带来危害。为此，一门新的计算机学科协议工程( p r o t o c o l e n g i n e e r i n g ) 便产生了 3 儿4 。 一体化，形式化的协议刀：发过程叫做协议工程。协议工程使用形式化的方法 来描述协议严格的设计和维护中的各个活动【5 】【6 】【7 】，它是研究对象为通信协议 的软件工程，但它建立套比现有软件工程一般方法更严格的协议设计方法，使 协议丌发过程一体化、系统化和形式化。协议工程旨在减少协议丌发中的潜在错 误，使通信协议的丌发过程能理论化和规范化的进行，从而提高协议丌发效率， 促进协议标准化发展。 协议的开发包括六个过程： 肌议设计：p d u 格式，协议机制，服务原语等设计： 协议揣述：川某种语i 芎确切的描述协议元素： 协议验证j 件能分析： 对说描述的协议验证其诈确性，分析其性能： 种堆j c s p 的协议模艘技术的i j f 究 始l ! i i 巾田科学技术人学倾f 。学位论文 协议实现：根据协议的描述产生网络硬件和软件： 肌议测试：对实现的协议进行测试； 协议维护：对网络硬件和软件进行维护。 通信协议一致性测试是协议测试中的一个重要部分，它的目的是测试通信协 议软件的工作行为是否与通信协议规范一致 8 】。它的工作过程一般是首先剥通 信协议进行形式化描述，然后使用通信协议的一致性描述生成测试序列，最后使 用此测试序列进行测试。 这罩，通信协议的形式化描述方法( f o n t l a ld e s c r i p t i o nt e c h n i q u e ：f d t ) 是 协议软件工程的核心部分，关联了协议软件工程中的各个过程【9 】。这里面的协 议设计、丌发、验证和测试构成了协议软件工程的主要内容，它的核心问题是找 到合适的通信协议形式化描述方法，通过这种协议形式化描述方法为以上的协议 软件工程建立一个形式化的丌发过程。 形式化描述方法不仅可以用来描述和定义一个系统的行为和动作，而且可 以用来验证和测试一个系统设计和实现是否满足一个系统功能的要求。由于不同 规范、模型、验证和测试使用不同的形式化描述方法，所以导致它们有不同的精 确程度。 一种形式化描述方法可以简单的表示为数学模型和程序语言概念的结合： 形式化描述方法= 数学模型+ 程序语言概念 形式化描述方法具有以下重要的属性： 数学模型； 程序语言概念( 例如数据类型、模块结构) ： 形式化的语法； 它是否可以方便的应用有效的工具来进行分析； 而形式化描述方法的描述能力可以粗略的分为以下三个级别： ( 1 ) 形式化描述系统的各个部分； ( 2 ) 不仅可以描述系统的各个部分，而且可以在此基础上进行手工的证 明，这样就可以使用详细的规范描述推导出更加抽象的系统规范： ( 3 ) 存在算法可以通过使用计算机来自动的完成级别2 的手工证明。 使用形式化技术方法好处有： ( 1 ) 使用形式化技术所描述的协议规范是精确的； ( 2 ) 可以通过严格的分析来确定给定规范的完整性和一致性； ( 3 ) 可以编写一个合适的编译器处理形式化规范来生成一个协议的部分 协议实现； ( 4 ) 协议的形式化描述可以作为一个协议的形式化文档； ( 5 ) 协议设计者可以使用形式化描述技术来描述协议，这样就可以和协 种皋十c s p 的悱波模型技术的研究 第21 j 中陶科学技术人学坝i j 学位论文 议实现者建口个精确的联系； 日前，协议r 稃所采用的模型技术一般使用些数学模型( 或方法) 年自动 机模型( 或程序模型) ，常用的通信协议的形式化模烈方法有限状态机( f s m ) 模型【1 0 】、p e t r i 网模型【1 1 】、时序逻辑t l ( t e m p o r a ll 0 9 i c ) 和通讯进程演算( c c s ) 【1 2 】等模型技术。最常j l j 的通信协议形式化描述语言有s d l 语言【1 3 】【1 4 】、e s t e i l e 语言【1 5 】和l o t d s 【1 6 】语言。另外还有描述协议数据结构的a s n 1 【1 7 】语苦和拙 述协议一致性测试用例的t t c n 1 8 】语言。 通过使用形式化的协议描述方法来描述的协议规范生成的测试用例，可以 对测试的覆盏程度、有效程度进行有效的分析。以上各种通信协议的形式化拙述 方法在描述协议的过程中，描述能力、分析能力、测试用例形式化生成能力有各 自的长处和短处，所以种的协议描述方法在描述特定的协议并生成测试序列时 可能存在不足。 有限状态机( f i n i t es 协t em a c h i n e ：f s m ) 是最常用的协议形式化描述技术。 有限状态机通常用状态转移图( s t a t e1 m 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 ) 【1 9 】【2 0 】和扩展有限状态机 ( e x t e n d e df i n i t es t a t em a c h i n e ：e f s m ) 【2 l 】【2 2 】。 p e 埘网( p e t “n e t ：p n ) 在通信领域得到广泛的应用。p e t “网可以清楚的表 达两个进程之问的通信 2 3 儿2 4 】，它也可以用作其他形式化描述方法的辅助方法 【2 5 】【2 6 】。通过增加一些特殊模型，p e t r i 网也有多种扩展，包括数字p e t r i 网 ( n u m e r i c a lp e t r n e t ：n p n ) f 2 7 1 和时间p e t r i 网( t i m ep e 啊n e t ：t p n ) 2 8 1 。 s d l ( s p e c 讯c a t i o n 锄dd e s c r i p t i o n ) 语言是由c c i t t ( 1 1 u t ) 组织丌发的电 信领域的国际标准。它的数学模型是扩展有限状态机模型( e f s m ) ，它可以精 确描述一个系统的动作特征。 l 0 1 d s ( l a n g u a g eo f t e m p o r a l0 r d e r i n gs p e c i f i c a t i o n ) 是由i s 0 组织丌发出 来语言。l o t o s 基本的思想是：一个通信系统可以描述成为一系列有时问顺序 的可以由外部观察到事件。l o t c i s 是用通信系统演算( c a l c u l u s o f c o m m u n i c a t i n g s y s t e m ：c c s ) 来描述进程的行为和交互，并且使用a c to n e 语言来描述数据 结构和表达式。a c t o n e 是一个抽象数据类型语言，它的数学模型是代数规范。 l 0 1 0 s 语言存在一些扩展，如d l o t d s 2 9 】，g l 0 1 d s 【3 0 】等等。 e s t e l l e 也是由i s o 组织丌发的一种语言，它也是基于扩展有限状态机模型 的( e f s m ) 。e s t e i l e 语言使用p a s c a l 作为基础，并且扩展它是他可以描述系统 的细节、进程的并发和进程问的通信。它通常被用作描述分布式系统和并行信息 处理系统。 种聃j 。c s p 的协议模型技术的研究 第3 贝 中国科学技术人学硕i ：学位论文 1 2 本文的研究内容和论文组织 本文对通讯顺序进程c s p 进行了深入研究 3 2 。 c s p 通讯顺序进程是c a r h o u r e 于1 9 7 8 年提出的一种并发分布式程序语言模 型，一经出现就被广泛地应用于计算机科学的诸多领域，如网络通信协议的形式化 描述等。c s p 模型的目的是描述一种在计算机应用的广泛领域中适用的最简单的数 学理论。其主要贡献是它把计算机所涉及的各种计算形式及其性质建立在一套严密 的形式系统上。c s p 主要通过进程事件的集合和进程的迹来描述进程的行为。c s p 可以通过并发、选择、递归等来描述进程之间的关系。 本文首先研究和分析比较了目前常用的协议形式化描述技术的特点，然后特别 针对c s p 模型进行了深入的研究和介绍，通过几个协议的具体的c s p 模型的描述， 研究出一套关于c s p 建模的大概方法和步骤。 接下来，本文针对一种新的形式化描述语言r s l ，研究了c s p 模型和r s l 形式 化描述语言的对应点，总结出一套c s p 模型转换到r s l 形式化描述语言的规则和步 骤，将形式化技术晕的模型和描述语言紧密结合起来。 最后，对c s p 在协议验证上作了初步的研究，用严密的代数演算方法验证协议 性质。并给出两个实例。针对c s p 的不足，本文还对它进行扩充，使它能够更方便 的用于协议描述。本文还对f s m 模型到c s p 模型的转化以及测试用例的生成作了初 步的研究。 本文的组织结构为： 第一章，介绍了研究背景和现状，对协议工程作了总体的介绍。 第二章， 对协议模型技术作了总体的分析，并对本文要研究的c s p 模型技 术作了详细的介绍。 第三章， 通过几个协议的具体的c s p 模型的描述，研究出一套关于c s p 建 模的大概方法和步骤。 第四章， 针对一种新的形式化描述语言r s l ，研究了c s p 模型和r s l 形式 化描述语言的对应点，总结出一套c s p 模型转换到r s l 形式化描 述语言的规则和步骤，将形式化技术里的模型和描述语言紧密结 合起来。 第五章， 对c s p 在协议验证上作了初步的研究，用严密的代数演算方法验 证协议性质。并给出两个实例。针对c s p 的不足，本文还对它进 行扩充，使它能够更方便的用于协议描述。本文还对f s m 模型到 c s p 模型的转化以及测试用例的生成作了初步的研究。 第六章， 是本文的结束语，总结了全文，且提出了一些需要进一步研究的 问题。 一种堆十c s p 的协议模型技术的研究 第4 贝 中国科学技术人学倾i j 学位论空 2 1 协议模型技术 第二章协议模型技术 2 1 1 引言 协议模型技术是协议一j ：耙! 的核心技术之一，它是协议工程的基础。形式描 述语南总足以某种模型技术为壤础，协议正确性验证必定基于某种协议技术，协 议f 动化实现以及协议测试等都以某种模型技术为基础。 计算机网络以及分布计算机系统可抽象成一个分层嵌套的系统模型。第n 层的 全局系统由多个分前j 的局部系统组成。而这些局部系统有一个或多个信道系统( 通 讯系统) 耦合起来。n 层的各个局部系统以及信道系统本身又可以看作是n l 层的 全局系统。n 层的全局系统构成n 一1 层的外部环境。 n 层协议全局系统有多个局部系统( 协议实体) 和( n 1 ) 层通道构成，模型 技术旨在精确地表述( n 1 ) 层通道，n 层局部系统和全局系统的行为和性质。n 层局部系统有多种协议元素组成，进步地说，模型技术还必须精确的表述各种协 议元素的性质和行为，以及它们之问的作用关系( 即协议机制) 。 ( n + 1 ) n 层 f ni s e r 2 n s a p n 层协议 图一协议的分层系统模型图 2 1 2 协议性质 协议性质，也就是全局系统性质，指一个好协议应该具有的性质，它包括四个 主要方面：活动性、安全性、一致性和完整性。 l 活动性( 1 iv e n e s s ) 协议活动性是指协议运行时一些好事情会发生。这些好事情包括：预定的事件 会，“啦，指定的协议状态会达到，应该进行的冼议行动会进行。协议的活动性 体现在终止性( t e r m j n a t i o n ) 和进展性( p r o g r e s s ) 两个方面，或者说，如果协议 彳终“：性和进展性，它就有活动性。终止性指协议从任何一个状态丌始运行，总能 i f ：确地达到终j i ：状态：进展t l 指协议从初始状态运行，总能一确地达到指定状态。 种牡i c s p 的脚议模型技术的研究 第5 贝 中因科学挫术人学坝i 学位论义 某螳情况卜- ，终j l 状态和初始状态是同的。这样，协议从初始状态丌始运行总能 f 确的i 叫到初始状态，并可反复运行，这就是协议的回归性( r e c u r r e n c c ) 。旧归性 = 终l l ：性+ 进展性= 活动性。 2 安全性( s a f e l y ) 协议安全性是指协议运行时没有坏事情出现。这些坏事情包括不可接受事件， 不可进步向前状态、错误的行为、错误的条件、错误的环境、变量值越界等等。 坏事情一般会导致两种现象：死锁( d e a d l o c k ) 或是活锁( 1i v e l o c k ) 。死锁指协议 堵塞在某一个状念而无法向前，活锁指协议做无意义的循环。 3 一致性( c o n s i sl e n c y ) 协议致性是指协议服务行为和协议性质一致。n 层协议的用户所要求的服务 以及它所能观察到服务性质与n 层协议内部机制所表现出的总体行为和性质是一致 的，那么协议就有一致性。一致性包括两个方面：协议应该提供用户要求的服务和 协议无需提供用户没有要求的服务。 4 完备性( c o m p le l e n e s s ) 完备性是指协议性质完全符合协议环境的各种要求，即协议的构造考虑了用户 要求、用户特点、通道性质、工作模式等各种潜在因素的影响，考虑了各种错误事 件，异常情况处理。 5 备注 关于协议性质还有多种说法，它们和上述四种说法的关系如下。有的学者将协 议分为一般性质和特殊性质。一般性质指那些与协议具体内容无关的性质，特殊性 质指那些与协议具体内容相关的性质。安全性和活动性属于一般性质，而一致性和 完备性属于特殊性质。协议验证技术着重一般技术，而协议测试着重于特殊性质。 2 1 3 协议元素性质 许多协议元素性质对协议模型技术有重要影响。此处列出其中一部分。 l 事件成对性 事件分通讯事件和内部事件两类，通讯事件是成对出现的，而内部事件( 如超 时事件) 不是成对出现的。 2 事件原子性 不论通讯事件还是内部事件要么不发生，一旦发生就一定完成，这种性质称作 事件的原子性，有原子性的事件称作原子事件。 3 事件时序性 服务原语和p d u 的交换规则决定了通讯事件时序性。 4 状态时序性 争件时序性决定了状态时序性。 5 变疑有限性 种捧j 1c s p 的饥议模型挫术的研究 蚺6 贝 ! ：堕! ! 兰垫查叁兰堡! ! 兰丝堡塞一 协议变最的舣值范围的明确定义叫做变最有限性。 6 过程的原f 性 个协议过程可能包括多个协议行动，过程一旦启动之后，所有包括的行动 次性完成，不经历中问协议状念，不被其它过程打断，这种性质叫做过程的原予性， 有原子性的过程叫做原予过程。协议运行时，它从一个状态到另外个状态的转 换可处理成原子过程。 2 1 4 通道类别 我们将通通分成：! 类，它们是：空通道，非缓冲通道和缓冲通道。 空通道：报文的传送时间和延时时日j 为0 的通道叫做空通道。 非缓冲通道：任何时刻，最多只有一个币在传送中保文的通道叫做非缓冲通道。 缓冲通道：允许有多个报文停留的通道叫做缓冲通道。 通道的两端为两个通讯事件发生点，一个报文从通道一端传送到另外端的过 程中，两个事件点产生四个事件。如果我们将两个端点分别标记为a 和b ，并假设 报文从a 端发到b 端，那么这四个事件的含义分别是： a ! ma 端的用户向通道的a 端发送报文，! 表示“发送”，a 表示a 端，m 表示 报文。 a ? m 通道从a 端接收一个报文，并启动传送，? 表示“接收”。 b ! m 通道完成报文的传送，将报文发送给b 端用户。 b ? mb 端用户从b 端接收报文。 a ! m 和a ? m 为协同事件，b ! m 和b ? m 为协同事件，而a ! m 和b ? m 以及a ? m 和 b ! m 为异步事件。 通道可以是单工、半双工和全双工的工作方式，全双工通道可视为两个分离的 单工通道。 2 1 5 协议模型的选取 目前，协议工程所采用的模型技术全部来自数学家以及计算机科学理论家所提 出的一些数学模型和自动机模型。比如，有限状念机模型( f s m ) ，p e t r i 网模型， 时序逻辑( t l ) 等等。 我们根据以下两个方面来选取协议模型： 1 能够方便充分的表示协议元素和通道的各种性质， 2 容易观察协议性质( 全局系统性质) 。 达到以上两点的模型技术就是一种理想的模型技术。“方便充分的表示”意味着 所采用的模型技术有足够强的表达能力和实用性，“容易观察”则意味着协议验证和 测试容易实现。 种埔，+ c s p 的m 议模堑技术的研究第7 虹 中阳科学技术人学坝l + 学位论义 2 2 各种协议模型简介 i | 前已经研究丌发出多种形式模型，主要有：有限状态机f s m ( f i n i t e s t a t e m a c h i n e ) 模型、p e t “i 嘲模型、通讯进程演算c c s ( c a c u l a so fc o m m u n i c a t i o n s y s t e m ) 、时序逻辑t l ( t e m p o r a ll 0 9 i c ) 、形式文法f g ( f o n i l a lg m m m a r ) 、过 程语言p l ( p r o c e d u m ll a n g u a g e ) 等数学模型和逻辑模型，下面分别简要介绍 f s m 模型、p e t r i 嘲模型、时序逻辑t l 模型。 2 2 1 有限状态机f s m 在迄今已经出现的各种形式化描述技术中，有限状态机f s m 是最为重要 的一种形式描述技术，它是很多形式化方法的基础。这主要是由于它直观性强， 町实现与其它形式方法的组合和转换，且易于自动实现，因而在形式化描述中占 有重要地位。 f s m 模型包括基本f s m 、扩展f s m 、结构化f s m 、通信f s m 等。 下面以扩展f s m 为例来说明。 f s m 定义为”一个血元组a = ( x ，i ，o ，n ，m ) ，其中： x 为有穷状念集，网络和分匍系统中，状态可理解为发送、接收、空闲或 等待等。 l 为输入集，它既可以为有限集，也可以为无限集，输入值与时| 、日j 有关，它 可由报文来表示。 o 为输出的有穷集合，其有关规则与l 相似。 n 为状态迁移函数，它由同一个时刻的输入信息及前一个时刻的状态决定， 即存在一个映射( n ：ix x 一 x ) 。 m 为动作及输出函数，输出信息可以看作输入信息及状态的函数。它由t 时 刻的输入信息及t 时刻的状态决定，即存在一个映射( m ：x xi - 0 ) 。 n 和m 表示f s m 的行为，在任何一个状念，若收到一个输入，那么状态迁 移函数n 将指出自动机的新状态，而、动作输出函数m 则指出f s m 产生的动作 和输出。 一个有限状态机可以采用状态转移图、状态转移矩阵或状态转移表等多种方 法来表示，其中最常用的是状态转移图。 f s m 最常使用的技术是可达性分析技术，可达性分析试图产生和检查协议 所有或部分可达状态。所谓可达状态是指协议从初始状态开始经理有限次转换之 后可达到的状态，所有可达状念构成可达图。可达性分析最重要的工作是产生和 检查町达图，判定是否存在死锁、活锁等协议错误。 f s m j ：简单直观而得到广泛应用，但不利于协议验证的实现，不易r 描 述复杂的系统，、匕进行人型复杂协议的构造时，f s m 模型将面临状态爆炸的问 种捧j c s p 的悱泌模型技术的研究 笫8 挺 中闭科学技术人学坝l 。学位论文 题。 2 2 2p e t r i 网 p e t r i 网是德国学者c a p e t r i 在其博士论文中首次提出的一种特殊的自动 机模型，它可j j 束描述通讯系统中异步成分之问的关系。这种自动机后来被称为 p e t “网。拒此之后，p e t r i 网很快得到了应用和发展，如时间p e t “网、随机p e t r i i ：c ) 9 、高级p e t r i 网、着色p e t r i 网等。p e t r i 网应用如此广泛的原因是：采用图形表 示，很清晰直观：j l 有很好的适应性，不仅能适应计算机科学而且也适应于社 会、物理等领域：它能描述系统的并发行为，使用p e t r i 网的分析技术对模拟 系统进行分析，能得到系统行为方面的信息；具有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 网柬进行说明。 应用p e t r i 网，首先要建立p e t r i 网模型，这种模型是被模拟系统抽象，它有 助于从概念上理解系统的结构。p e t r i 网可以定义为一个五元组c = ( p ，t ，i ， o 。m ) ，其中： p = p i ，p 2 ，p n 是位置( p l a c e ) 的有穷集合； t = t i ，t 2 ，t n 是迁移( t r a i l s i t i o n ) 的有穷集合。且t 与p 不相交； l 是输入函数集，是迁移t 到位置集的映射，即i ：t ) p 。i = i ( t 1 ) ，i ( t 2 ) ， ，i ( t 。) ，) ，对于每一个t 。t ，可以得出相应的i ( t i ) = p _ i ，p k 。 0 是输出函数，也是迁移t 到位置集的映射。即0 ：t ) p 。对于每一个t t ，可以得出相应的0 ( b ) = p j ，p k 。 m 为标记( m a r k i n g ) 集，m = m o ，m i ，“2 ，m k ， 。m o 为初始标 记，m k 为第k 次标记。标记m k 为一个向量，m k = p l ( n ) ，p 2 ( n ) ，p i ( n ) ， ，p i ( n ) 为一个正整数，表示位置p i 的令牌数。p e t r i 网的标记也叫p e t r i 网的状态。m o 为初始状态，m k 为状念k ，m 为p e t r i 网的状态集合。 p e t r i 网的分析技术主要有两种：可达树分析方法和矩阵方程分析方法。借助 p e t r i 网的分析技术能得到被模拟系统的有界性、安全性、守恒和可达性等方面 的性能评价。 p e t r i 网在刻划复杂系统时会显得异常繁琐，也不利于描述协议的进展情况， 当进行大型复杂协议的构造时，p e 雠模型也将面临状态爆炸的问题。 2 2 3 时序逻辑t l 从逻辑角度来说，时序逻辑t l 是模态逻辑的扩充，以状态为可能世界，以 状态的演变次序荚系为可能i 髓界问的可到达关系。时序逻辑的种类很多，随时问 结构4 i 同，算子的选择也有差异。 种璀j c s p 的龇泌模靼技术的f l j 究 蚺9 贝 中闻科学技术人学坝i 。学位论文 p n u e “最先将时序逻辑引入计算机科学，用它作为并发程序的推理 ：具。时 序逻辑公式般描述异类过程的性质，丽很少描述单个过程的性质。时序逻辑的 成功之处西1 ：它具订表达并发程序性质的能力，同时也因为它是很多证明方法的 耩础，其中些证明方法已写成算法，最有价值的证明算法式模型算法。 目前研究较多的时序逻辑包括：p n u e l 的线性时序逻辑m p tl 区间时序逻 辑d c ( d u r a t i o nc a l c u l u s ) 、分支时序逻辑c t l ( c o m p u t a t i o n t r e el o g i c ) 。 时序逻辑是通过状态关联进行推理的一种技术，它附加有与时阳j 相关的操作 属性。采用形式化方法定义动念语义和静态语义，其中动态语义用推力规则描述； 静念语义由属性语法进行定义。操作的语义基于等价关系的若干类型，用之可证 明描述的等价性和币确性。 如果一个系统的某个性质能用一个确定的逻辑表达式描述，并且恒为真( 不 随系统的状念变化或执行序列而改变) ，那么这个性质称为系统的不变性质，简 称系统不变性。 时序逻辑常用不变性分析方法验证协议性质。协议不变性分析往往采用归纳 法，包括两个工作：第一是完全币确地找出系统( 协议) 的不变性质，形成严格 定义的不变性表达式；第二是以某种方式执行协议，验证不变性表达式是否恒为 真。我们所说得不变性表达式指的是第二项工作。第一项工作由手工进行，许多 协议描述文本也包含了不变性表达式。 时序逻辑应用较为成熟，并且数学抽象能力很强，它侧重于通过定义系统外 部可见的行为事件来描述系统，即直接描述系统的输入输出行为，而不关心协 议实体的内部变化，比f s m 、p e t r i 网更易于刻划协议的活动性，因而有利于对 协议的各种性质进行分析验证。时序逻辑因其逻辑推理机制，使之在通信协议形 式化验证中得到了广泛的应用。 2 3 通讯顺序进程c s p 数学家的任务之一是从现实世界中识别并定义一类目标，然后对该类目标建立 一套严密的演算系统。进程( p r o c e s s ) 是计算机科学与工程中广泛使用的概念，一些 数学家已成功地将它们作为演算目标建立了几种不同的进程代数( t h ea l g e b r ao f p r o c e s s ) 系统进程代数的丌拓性工作是由r m i l e r 进行的，他的通讯进程演算 c c s ( t h ec a l c u l af o rc o 唧u n i c a t i n gs y s t e m ) 已在协议工程等领域内得到重要的应 用。c a r h o a r e 在c c s 的基础上创立了通讯顺序进程c s p ( t h ec o m m u n i c a t in g s e a u e n l j a l 【r o c e s s e s ) 。 根抓r a is e 规范语言的特点，我们决定采用c s p 模型( t h ec o m m u n ic a t i o n s e q u o n li a i p r o c e s s ) 来描述协议。 c 通汛顺序进程是c a r h o u r e 】二1 9 7 8 年提出的一种并发分布式程序语言模 种埔f c s p 的 j 改模型技术的i j f 究 始1 0 贝 扣嘲科学技术人学坝i 学位论殳 型，一经出现就被j 一泛地应用于汁算机科学的诸多领域，如网络通信协议的形式化 描述等。 c s p 模型的j j 的是描述一种在计算机应用的广泛领域中适用的最简单的数学理 论。其 ：要贡献足它把计算机所涉及的各种计算形式及其性质建立在套严密的形 式系统j 二。 c s f ) 主要通过进程事件的集合和进程的迹来描述进程的行为。c s p 可以通过并 发、选择、递归等束描述进程之间的关系。 卜i 边简单介绍。些c s p 的属性，描述方法。 2 2 1 进程 我们刚进程这个诃来代表客体的行为模型，并规定这些客体的行为足能用 组成字母表的事件的有限集仑来说明的。 我们约定 i 小写的字符串表示不同的事件，如：c o i n ，c h o c ，i n 2 p ，o u t l p ： 有时也用字母来表示事件，如：a 巾，c ，d ，e 。 2 大写的字符串表示具体定义的进程。如：v m s 一简单自动售货机、 v m c 一复杂自动售货机。 在后面法则中出现的字母p ，q ，r 表示任意进程。 3 小写字母x ，y ，z 是表示事件的变量。 4 大写字母a ，b ，c 表示事件集合。 5 大写字母x ，y 表示进程的变量。 6 进程p 的字母表记做。沪。如：口附据= c d f h ，c o f 。 2 2 1 1 前缀 一尸) 描述一个进程，第步是一个事件x ，之后便是进程p 。 口( x p ) = o 户i fx o p 这个前缀描述符号我们把它进行了扩充。它可以描述：事件一事件 事件一进程 进程一进程 2 2 1 2 递班1 “j 力年翟式拓边进稃名的所有递归出现前至少缀有一个事件时，这种自参考或递 种艰j c s p 的协议模型技术的研究 2 f l l ! j 上 巾周科学技术人学坝i ：学位论文 归的进程定义方法爿+ 是有效的。我们把以| j i 缀丌始的进程表达式称作是卫式表达式。 记做：肛：爿f ( x ) 例如： x 1八永远f i 停的钊，。它的递归定义： c o c k = ，： ，f c 七 ( f 耙七 ) x 2一只简单自动售货机，投入多少枚硬币就送出多少块巧克力，它的递归定义是： 脚舔= 肛v ： c o f ”，c o c ) ( c d 加一( c 向o c 寸x ) ) 2 2 1 3 选择 很多客体在所处的环境中与环境相互作用，导致客体的行为受到环境影响。 则表达式( x pjy q ) 表述了这么一种客体，一丌始时，它既可以执行事 件x ，也可以执行事件y 。如果发生的事件是x ，则客体的后续行为按p 进行动作； 如果是事件y ，则客体按q 进行动作。 例如： x l一台售货机，它每笔交易或卖巧克力或太妃糖，定义为 m 纪r = ，c o m 一( c d c x l f q 艉p x ) 2 2 1 4 法则 我们可以运用一些代数法则证明或否证字母表相同的两个进程的等同形 这些代数法则和算术中的法则和类似。 l 1 ：( x ：a p ( x ) ) = ( y ：b q ( y ) ) 兰( 彳= b ) 州p ( x ) = q ( x ) ) i 1 a ：s 丁d j p ( d p ) l 1 b ：( c 尸) ( d q ) l 。l c ：( c 斗j p p _ q ) = ( d _ q | c 寸j p ) l ld ：( c 斗尸) = p 斗q ) ；j i ) = q 种捕fc s p 的悱泼模盟技术的究第1 2 贝 中冈科学技术入学坝 j 学位论史 2 2 1 5 迹( t r a c e ) 个进私彳r 为的迹足符号的个有限序列，它记录了进程到某4 刻为j ：发牛的 再个穹 件。 一个迹将表示为符号的个序列，中间有逗号隔丌，并且括号在一对角括号内。 有两个事件组成，y 跟在x 后发生； 只包含一个事件x 的序列： 不包含 任何事件的空序列。 例如： x l ：简单自动售货机v 幅，若刚好完成了为两个顾客服务这时它的迹为 。 2 2 1 6 迹的运算 2 局限 表达式( t a ) 表示迹l 局限于集合a 中的符号，即把t 中所有不属于a 的 符号去掉后留f 的迹。 例如： f x )= 3 首部与尾部 假设s 为一非空序列，取它的第一个符号记做s 。去掉s 。的结果记做s 。例如： 。= x k 4 星号