（通信与信息系统专业论文）基于正确性验证的sdh协议测试.pdf

表目录表1 发送s d h 帧过程( s e n d ) 表2 接收s d h 帧过程( r e c e i v e ) 表3 一个s d h 的协议扩展命令描述( 参数配置)表4 一个s d h 的协议扩展命令描述( 特殊命令)表5 阶段性测试报告列表445999图曰习之图1 信号分插示意图1 4图2s t m - n 帧结构图1 5图3 流程1 ：c 一4 一 v c 一4 一 a u 一4 - - s t m - 1 1 9图4 流程2 ：c 一3 v c 一3 - - t u 一3 - - t u g 一3 - - v c - 4 一 a u 一4 - - s t m l 1 9图5 流程3 ：c 1 2 v c 一1 2 - - t u ，1 2 - - t u g 1 2 - - t u g 一3 一 v c - 4 一 a u 一4 一 s t m 1 1 9图6 局内分配的同步网结构2 0图7 局问分配的同步网结构2 0图8 形式化描述方法分类2 3图9 发送s d h 帧过程的e f s m 模型简图2 8图1 0 接收s d h 帧过程的e f s m 模型简图2 8图1l 发送s d hl 防过程的p e t r i 网模型简图2 9图1 2 接收s d h 帧过程的p e 删网模型简图2 9图1 3 植入错误的发送s d h 帧过程的e f s m 模型简图2 8图1 4 植入错误的发送s d h 帧过程的e - p e t r i 网模型简图2 8蹦j5 植入错误的接收s d h 帧过程的e f s m 模型简图2 8图1 6 植入错误的接收s d h 帧过程的e p e t r i 网模型简图2 8图17 验证后的发送s d h 帧过程的e f s m 模型简图2 8图1 8 验证后的接收s d h 帧过程的e f s m 模型简图2 8图1 9 一致性测试基本模型4 2图2 0 一致性测试工作流程4 3图2 l 四种端系统抽象测试方法的结构4 4图2 2 两种中继系统抽象测试方法的结构4 4圈2 3 用u l o 方法产生f s m 测试序列的示例4 4图2 4s d h 协议测试过程5 3图2 5 被测逻辑示意图6 0图2 6 测试系统整体结构示意图6 l图2 7s d h 测试平台与被测逻辑之间地通讯关系6 2图2 8s d h 测试平台的总体结构图6 2图2 9s d h 成帧示意图6 3图3 0s d h 的虚级联映射示意图6 3图3l 成帧模块总体设计示意图6 4图3 2 缓冲区管理机制示意图6 5圈3 3s d h 分析示意图6 6图3 4s d h 的虚级联解映射示意图一6 6图3 5 分析模块总体设计示意图图3 6 参数管理机制原理图图3 7s d h 成帧器之虚级联映射子界面示例图3 8 测试系统工作流程图6 76 86 97 1一t 厂幼即弓2 ； - f 钆、。p 譬j摘要s d h 协议在现代信息传输中显露出了强大的生命力。s d h 收发器是用于s d h 光网络的重要器件，是s d h 的协议实现。为了对s d h 协议进行更彻底、更正确、更全面的测试，本文将在对s d h 形式化模型进行正确性验证的基础上，利用开发的测试系统工具对逻辑仿真的s d h 收发器进行测试，最终完成对s d h协议的测试工作。形式化模型采用了直观高效的e f s m 模型和p e t r i 网模型，并以这两种模型为例，提出了基于模型转换的正确性验证方法，对s d h 形式化模型进行了验证，随后依据一致性测试理论，本文提供了采用u i o 方法生成s d h 测试序列的途径，并为补充测试序列完备性增加了相应的测试用例。利用t c l t k 开发的s d h 测试系统采用管道一过滤器技术设计，并使用缓冲区管理机制对管道进行了扩展；同时系统平台还提供了t c l 扩展接口，测试者可以通过测控软件的人机交互接口直接对s d h 测试过程进行动态控制。对s d h 协议进行形式化建模，是贯穿此项协议工程始末的核心技术，对s d h形式化模型进行正确性验证，是进行协议测试的保障，我们开发的s d h 测试系统，又为s d h 这种新型的传输机制提供了一个有效的测试工具。基于正确性验证的s d h 协议测试，从理论的高度为协议测试拓展了一条新颖的思路，而后续开展的测试实践又直观地展示了此项研究最终能达到的效果。本文主要完成了利用e f s m 模型以及p e t r i 网模型为s d h 协议进行形式化建模的示例；随后研究模型间相互转换的理论，提出了基于模型互换的正确性验证方法，并利用此法对s d h 的形式化描述进行了验证；在正确性验证的保证下，分析s d h 协议一致性测试中不完备的部分，针对发现的协议错误补充测试用例，生成更完备测试序列集合：最终利用开发的s d h 测试系统工具，对s d h 的被测实现进行测试并分析了测试结果。关键词：同步数字传输体制，形式化描述，扩展有限状态机，p e t r i 网，正确性验证，模型转换，协议一致性测试，测试序列，可执行测试例，工具命令语言，测试系统6a b s t r a c ts d hp r o t o c o lh a ss h o w ns t r o n gv i t a l i t yi nt h em o d e mi n f o r m a t i o nt r a n s m i s s i o n s d ht r a n s m i t t e r r e c e i v e ri sa l li m p o r t a n td e v i c eo fs d ho p t i c a ln e t w o r k ，w h i c hi st h ei m p l e m e n to fs d hp r o t o c 0 1 t ot e s tt h es d hp r o t o c o lm o r et h o r o u g h l y , m o r ec o r r e c t l ya n dm o r ec o m p r e h e n s i v e l y ，t h i sa r t i c l ec o m p l e m e n tt h es d ht e s tb yt e s t i n gt h es i m u l a t o ro fs d ht r a n s m i t t e r r e c e i v e r , u s i n gt h et e s ts y s t e mt o o l sw eh a v ed e v e l o p e d b a s e do nt h ec o r r e c t n e s sv e r i f i c a t i o no ft 1 1 ef o r m a l i z a t i o nm o d e lo ft h es d hp r o t o c 0 1 t h ef o h n a l i z a t i o nm o d e l se m p l o yt h ee f f e c t i v ee f s mm o d e la n dp e t r in e tm o d e l -a n dp u tf o r w a r dt h ei d e ao ft h em o d e l c o n v e r s i o n - b a s e dc o r r e c t n e s sv e r i f i c a t i o n ，t h e nv e r i f vt h es d hf o r m a l i z a t i o nm o d e li nt h ec a s eo ft r a n s f o r m i n gt h e s et w om o d e l so n et ot h eo t h e r a n da c c o r d i n gt h ec o h e r e n c et e s t i n gt h e o r y , t h ea r t i c l eg e n e r a t e ss d ht e s ts e q u e n c e sb yu s i n gu i ot e c h n i q u et oc r e a t es d hp r o t o c o lt e s ts e q u e n c e sa n dt h ea d d i t i o n a lt e s tc a s e sf o rt h em a t u r i t y s d ht e s t i n gs y s t e mi sd e v e l o p e di nt h ec h a n n e l f i l t e rm e t h o d ，a n dt h ec h a n n e l si nt h em e t h o da l ee x t e n d e db ys o m eb u f f e rm a n a g e m e n tm e c h a n i c s a n dt h es y s t e mp l a t f o r ma l s op r o v i d e sat c le x t e n di n t e r f a c e s t h et e s t e r sc a nc o n t r o lt h et e s tp r o c e d u r ed y n a m i ct h r o u g ht h ei n t e r f a c e so f t h et e s tc o n t r o ls o f t w a r e t h ef o r m a l i z a t i o nm o d e l i n go ft h es d hi st h ec o r et e c h n o l o g yo ft h i sp r o t o c o lp r o j e c t 。t h ec o r r e c t n e s sv e r i f i c a t i o no fs d hf o r m a l i z a t i o nm o d e li st h eg u a r a n t e eo ft h ep r o t o c o lt e s t t h es d ht e s ts y s t e mw eh a v ed e v e l o p e di sa ne x c e l l e n tt o o lf o rt e s t i n gt h i sn e wt r a n s m i s s i o nm e c h a n i c 1 1 1 es d ht e s t i n gb a s e do nt l l ec o r r e c t n e s sv e r i f i c a t i o ni sp r o v e dt oh a v ep r o v i d e dan e ww a yt ot h ep r o t o c o lt e s ti nt h et h e o r e t i c a ll e v e l a n dt h ef o l l o w i n gp r a c t i c a lt e s t si n 协ea r t i c l ew i l ls h o wt h ee f r e c to ft h i sr e s e a r c hv i s u a l l y t i l i sa r t i c l em a i n l ye s t a b l i s ht h ee f s ma n dp e t r in e tm o d e l so fs d hp r o t o c o la f t e rt h er e s e a r c ho ff o r m a l i z a t i o nm o d e i s ；p u tf o r w a r dt h ei d e ao fm o d e l c o n v e r s i o n b a s e dc o r r e c t n e s sv e r i f i c a t i o n ，w h i c hb a s e do nt h et h e o r yo fm o d e l c o n v e r s i o n ，t h e nv e r i f yt h ef o r m a l i z a t i o nm o d e lo fs d ht h r o u g ht h ei d e a ；u n d e rt h eg u a r a n t e eo fc o l t e c t n e s sv e r i f i c a t i o n a n a l y z et h ei m m a t u r ep a r to ft h es d ht e s ts e q u e n c e s ，s u p p l yt h ea d d i t i o n a lt e s tc a s e sa n dg e tt h em o r ec o m p l e t ea g g r e g a t i o no ft e s ts e q u e n c e s ；u s et h es d ht e s ts y s t e mt ot e s tt h es i m u l a t o ro fs d ht r a n s m i t t e r r e c e i v e ra n da n a l y z et h ef i n a 】r e s u l t s k e yw o r d s ：s d h ，s p e c i f i c a t i o n ，e f s m ，p e t r in e t ，c o r r e c t n e s sv e r i f i c a t i o n ，c o n v e r s i o n ，p r o t o c o lc o n f o r m a n c et e s t i n g ，t e s ts e q u e n e e ，e x e c u t a b l et e s ts u i t e ，t c l t k ，t e s ts y s t e m71 1 研究背景第一章绪论1 1 1 协议工程通信协议是计算机网络和通信网络中，各通信实体或通信进程间进行交互的信息所遵守的一组规则f 1 】。随着计算机通信和网络技术的不断提高，网络系统的复杂性在协议方面体现出空间分布性、并发性、异步性、不稳定性和多样性。这不仅意味着协议开发难度大，周期长，而且潜在错误多，协议开发过程中任何点错误和缺陷都将给通信系统的稳定性、可靠性、坚固性、安全性、容错性以及系统之间互通性和互操作性带来巨大的危害。因此，需要合适的方法、技术和计算机辅助工具，使开发过程工程化，以便提高协议的开发效率，促进标准化的协议实现，因此产生了协议工程( p r o t o c o le n g i n e e r i n g ) 学科1 2 。所谓协议工程，是指一体化和形式化的协议开发过程。它的宗旨是为协议软件的研制和开发提供一整套工程规范。它包括了以下六个过程【3 ：1 协议设计：p d u 格式，协议机制，服务原语等设计；2 协议描述：用某种语言确切地描述协议元素；3 协议正确性验证与性能分析：对所描述的协议验证其正确性，分析其性能；4 协议实现：根据描述的协议产生网络硬软件；5 协议测试：对实现的协议进行测试；6 协议维护：对网络硬软件进行维护。1 1 2 形式化描述形式化描述方法1 4 是保证设计正确性的一条重要途径，它用数学方法表达协议的规范或性质，并且根据数学理论来证明所设计的协议满足协议的规范或具有所期待的性质。在不能证明所期望的性质时，则可能发现设计错误。在协议设计中，从协议的设计规范，到对协议进行正确性验证，以及对协议实现的最后测试，都是用形式化的方法对该设计阶段的设计进行证明【5 j ，尽可能的在每个设计阶段发现错误，及时的更正，避免将设计错误引入下一个设计阶段错误。实践证明，形式化方法确实通过形式规范和证明增强了对系统的理解从而发现了设计错误，或者通过形式化的自动证明发现了用其他方法不能发现的设计错误。协议工程是形式化的协议开发过程，它使用形式化的方法来描述协议的设计和维护中的各个活动，是研究对象为通信协议的软件工程。形式化描述方法1 6 j是协议工程技术的核心技术之一，它是协议工程的基础。协议正确性证明必定基于形式化描述方法，所以，利用形式化的描述方法1 7 j ( 包括模型技术及形式描述语言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 ) 描述协议，是进行正确性验证和协议测试的前提。因此形式化建模是本文的第一个核心。1 1 3 正确性验证随着计算机通信和网络出现，通信协议自动运行于计算机之上，但是通信错误仍然会发生，而且错误发生的更快，更加不可能通过人为干预对不可预期的错误进行修正。因此，必须有一整套行之有效的方法，保证通信协议从设计、开发到实现、运行，都能够正确的完成，尽最大的可能避免错误的发生。这也就是协议验证的意义所在。协议的正确性验证1 8 试图在协议开发的前期最大限度地检测和纠正协议错误和缺陷，包括死锁( d e a d l o c k ) 、活锁( 1 i v e l o c k ) 、不可执行地行动、协议外部性能不符合服务要求等，是保证协议正确性的关键技术i 9 j ，只有通过正确性验证的协议，才能有保障的进行协议实现，继而对协议实现进行测试。因此正确性验证是本文的第二个核心。1 1 4 协议测试协议测试h j 可分为互操作测试、性能测试和一致性测试i ”j 。一致性测试是前两种测试的基础，是协议测试中的个重要部分。通信协议一致性测试旨在检验所实现的协议实体( 或系统) 与协议规范的符合程度。有了一个标准化的协议并不能确保协议的不同实现之间能够正确地进行通信，这有很多原因，如下所述：1 目前，协议规范一般都是采用自然语言描述，具有二义性；2 开发人员对协议规范的理解的差异会产生不同的协议实现：3 对没有进行详尽完备描述的协议规范，容易出现不同协议实现阃的不兼容；4 不同的实现手段也会产生不同的协议实现；5 协议的复杂度增大，协议开发人员在开发中容易如现失误。因此我们需要有一种有效的方法对各种协议实现进行测试，来判断该实现是否与协议规范相一致，这种方法便是协议一致性测试。在协议一致性测试研究中，主要解决两个问题 h i ：1 测试组织：即测试方法的研究与测试系统的建立；2 测试集：即如何从理论和方法上研究并产生高质量的测试集。协议一致性测试的测试组织问题具体到我们的对象协议，即要研究s d h 协议的测试方法并生成相应的测试序列。这是本文的第三个核心。1 1 5 协议测试系统协议的一致性测试系统是实现协议一致性测试的手段，一个好的测试系统可以极大地简化测试序列的设计，使得测试能方便、自动、高效地进行。目前的测试系统大致可以分为两类，一类是基于t t c n t l 2 的测试系统，是一种标准的研究方法；一类则基于其他语言。本文研究的测试系统就是基于t c l 语言的。文献【1 3 】【1 4 】【1 5 1 中分别报告了为o s i 协议一致性和互操作性测试而设计的有名的协议测试系统。t t c n ( t h et e s t i n ga n dt e s tc o n t r o ln o t a t i o n ) 1 1 2 是由i s o i e c 9 6 4 6 3 和i t ux 2 9 0 系列所提出的实现o s i 与i t u 协议定义的一致性测试方法的标斛m l ，它侧重于用形式化语言描述测试流程，在测试方法研究中用得比较多。但是t t c n所生成的c 代码未经优化，一般只能适用于对时间要求不是很严格的协议的测试【17 1 。t c l ( t o o lc o m m a n dl a n g u a g e ) 是一种可嵌入的命令脚本化语言【。“可嵌入”是指把很多应用有效，无缝地集成在一起。“命令”是指每一条t c l 语句都可以理解成命令加参数的形式。t c l 虽不是规范化的方法，但在工业界，它已经成为事实上的标准。t c l 突出的优点是执行效率高，虽然是解释执行，但大部分代码都是编译好的机器码。而且就对复杂协议的描述能力而言，t c l 的描9述能力相当于c 语言的描述能力。t c l 源于c 语言，又能与c 语言无缝组合，并具有很强的扩展性，它的一个重要特点就是可以根据具体环境需要，方便地进行命令扩展【伸l 。t c l 还提供了独有的组件技术，t k 是与t c l 相关联的用于进行图形用户界面编程的工具包。是t c l 最为著名的扩展模块( 即t c l ，r k ) 。t k定义了用来创建和操作用户界面组件( w i d g e t ) 的t c l 命令。针对s d h 协议的复杂性以及s d h 信号涉及到的大量参数，本文采用的是基于t c l 语言的一致性测试系统。同时，由于t c l 具有良好的移植性，它本身就是跨平台设计的，这更有利于我们在不同的操作系统上进行对s d h 协议的测试。s d h 测试系统是本文测试使用的工具。1 2 研究现状随着网络通信技术的飞速发展，协议工程在规摸、功能以及开发方面的要求越来越高。面对日趋复杂的设计，协议测试越来越成为协议工程流程中的瓶颈。一个简单的错误可能延缓整个工程的开发周期，一个协议实现中的隐含错误可能导致严重的后果。在设计的后期检查所有的逻辑错误是一项艰苦的任务，所以基于正确性验证的测试技术显得尤其重要。对协议本身的逻辑正确性进行校验的过程称之为协议的正确性验证( p r o t o c o lc o r r e c t n e s sv e r i f i c a t i o n ) ，它是保证协议设计正确性和完整性的一个重要阶段，处于协议工程中协议形式化描述阶段之后，协议测试阶段之前，其主要目的是试图在协议开发的前期最大限度地检测和纠正协议错误和缺陷，为后续的协议测试打好基础。因此，形式化描述、正确性验证、一致性测试是对特定协议进行完备测试的三大核心。目前的协议形式化描述语言大都基于以下几种形式化模型：有限状态机模型f s m 以及扩展有限状态机模型e f s m ；p e t r i 网；通信进程代数c c s ；消息流图m s c 等。关于这些模型的验证理论和方法非常多，但它们大都是对单一模型的验证理论和方法的研究，各有其针对性和侧重面，但不全面。形式化的正确性验证思想早在二十世纪七十年代末期久被提出来了，但早期的研究受状态空间爆炸问题的严重困扰，验证规模非常小，有人甚至认为此方法根本不可行。1 9 8 7 年，c a r n e g i em e l l o n 大学的研究生m e m i l l a n 在形式方法的运用上取得了突破，他用o b d d 简介表示系统的状态和转换关系，使得验证规模大大提高。从此，形式化的正确性验证技术开始迅速发展。随着形式验证技术的日趋成熟，开发应用工具，探索新的验证方法成为该领域一项重大课题，因此很多国家都投入了大量的人力物力从事协议验证的研究工作。例如：英国的国家物理局n p l 、法国国家通信研究中心、德国国家通信研究局g m d 、美国国家标准化研究局、美国新罕布什尔大学互操作研究实验室、中国清华大学计算机科学与技术系的计算机网络与协议测试实验室等单位都在这个领域投入了大量的研究力量。协议测试是保证协议实现正确性的高阶手段。随着通信协议的发展，测试技术日趋成熟，并且已经开发了不少成熟的测试工具，但如今广泛采用的测试技术并未能保证在协议设计的初级阶段就能完成完备的正确性验证，因此当被测试的协议非常复杂、庞大时，协议测试的错误覆盖率往往达不到要求，整个过程费时费力。为了能进行更彻底、更正确、更全面的进行协议测试，我们希望在分析评价各种形式化模型验证理论的基础上，提出基于模型组合、分离和互换理论的新的i 0验证方法，先对通信协议的形式化描述进行正确性验证，并在此基础上，完成对协议的一致性测试。本论文就是在此背景下开展完成的。1 3 本文的主要贡献及结构安排1 3 1 主要贞献1 分析和评价了现有的形式化描述模型，本文主要涉及到e f s m 模型以及p e t r i网模型；2 利用上述模型对s d h 协议进行了典型部分的形式化描述；3 以上述模型为基础，研究模型问相互转换的理论与方法，提出了基于模型互换的正确性验证方法，同时对s d h 协议的形式化模型进行了验证；4 在正确性验证的保证下，分析s d h 协议静态描述中不完备的部分，将发现的协议错误进行补充，生成了更完备测试序列集合；5 利用s d h 测试系统工具，对逻辑仿真的s d h 协议实现进行了测试并分析测试结果，最终完成对s d h 协议的测试。1 3 1 章节安排1 第二章介绍s d h 协议原理；2 第三章介绍形式化描述理论并对s d h 协议进行形式化建模；3 第四章介绍正确性验证理论，在此基础上提出基于模型互换的正确性验证方法，并利用此方法对s d h 协议的形式化模型进行正确性验证；4 第五章介绍协议一致性测试原理，并在通过正确性验证的s d h 协议模型的基础上，通过u i o 方法对s d h 的e f s m 模型生成协议动态部分的完备测试序列集合，并为补充协议静态部分的测试序列完备性增加了新的测试用例；5 第六章结合协议模块的开发原理，介绍s d h 协议的测试设计思想；6 第七章开发s d h 协议测试系统，并在测试分析理论的指导下，对利用该工具测试得到的结果进行测试结果分析；7 第八章总结和展望。第二章s d i t 协议的原理2 1 光纤通信近1 0 多年来，光纤通信在人类想信息社会过渡的过程中扮演着重要的角色。正如有关权威认识所说：纵观影响当今电信业的主要技术，很少象光纤和广播传输系统那样能够引发如此剧烈的变革。光纤通信的发展和广泛应用，极大的提高了信息的传输容量，是通信行业发生翻天覆地的变化。2 0 时机7 0 年代末，光纤通信开始进入实用化阶段，各种各样的光纤通信系统如雨后春笋在世界各地建立起来，逐渐成为电信传送网的主要传输手段。近几年来，光纤通信中的各种新技术也日新月异的发展着，在全球信息高速公路的建设热潮中扮演着重要角色 2 0 l 。2 1 1 光纤通信已成为信息传输的主要手段自1 9 7 0 年世界上第一根超低耗光纤问世以来，迄今为止只不过经历了近三十年的时间，但光纤通信技术却取得了极其惊人的进展。1 9 7 6 年，美国在亚特兰大开通的首个多模光纤通信实用化系统，其码率仅为4 5 m b i t s 、中继距离也不过1 0 公里。四年之后，多模光纤通信系统就全部商用化，传输速率达1 4 0 m b i t s 、中继距离可达6 0 公里以上。伴随研究工作的不断深入，人们发现单模光纤具有带宽极宽、传输容量大等优点，而且在长波范围( 1 o 1 8 微米) ，光纤会呈现更低的衰耗( v c - 4 一 a u 4 一 s t m 一18 58 6 + 。旺习+ 。旺习+ 。臣习c - 3 ( 9 * 8 4 )v c3 ( 9 * 8 5 )t u 一3 ( 9 * 8 5 + 3 ) t u g - 3 ( 9 * 8 6 )姐。+ 匹v c - 4 ( 9 2 6 1 )a u 一4 ( 9 2 6 1 + 1 9 )s t m 一1图4 流程2 ：c - 3 一 v c 3 一 t u - 3 一) 1 1 j 0 3 一 v c - 4 - - a u - 4 - - s t m 1。 二二： 。+ e 日。+ 。 二三三 + 。 三三习+ e 匪c - 1 2 ( 9 * 4 - 2 )v c - 1 2 ( 9 * 4 一1 ) t u 一1 2 ( 9 * 4 ) t o g 一2 ( 9 1 2 ) t i l 6 3 ( 9 * 8 6 )+ 。圈习+ t 旺。+v c 一4 ( 9 2 6 1 ) u 一4 ( 9 2 6 1 + 1 9 )图5 流程3 ：c 1 2 一 v c 1 2 一 t u 1 2 一 1 u g 1 2 一) 呵u g - 3 一 v c 4 一) a u 4 - - s t m 12 3 4s d h 的网同步概念网同步【2 5 】是数字网所特有的问题。其概念是指使网络中所有节点的时钟频率和相位都控制在预先确定的容差范围内，避免或减少由于数字传输系统中信息比特的溢出和取空导致的数字环的滑动损伤，并使数字交换机中产生的滑动限制在一定的范围内，以使得网的各交换节点的全部数字流实现正确、有效的交换，以保证通信质量。s d h 的引入对网同步提出了更高的要求。当网络工作在正常模式时，各节点同步于一个基准时钟，节点间时钟只存在相位差而不会出现频率差，因此只会出现偶然的指针调整事件。当某节点丢失了同步基准时钟信号而进入保持工作模式或自由运行模式时，该节点时钟与网络时钟之间出现频率差，会导致指针连续调整。s d h 网同步结构通常采用主从同步方式，要求所有网络单元时钟的定时都能最终跟踪至全网的基准主时钟。同步定时的分配则随网络应用场合不同而不同，局内采用星型拓扑，局问采用树型拓扑：1 9l局内分配的同步网结构：逻辑上的星型拓扑结构所有网络单元时钟都直接从本局内最高质量的时钟( b i t s ) 获取定时，只有b i t s 是从来自别的交换节点的同步分配链路中提取定时并能一直跟踪至全网的基准主时钟。该节点时钟一般至少为三级或二级时钟。定时信号再由该局内的s d h 网络单元经s d h 传输链路送往其他局的s d h 网络单元。由于t u 指针调整引起的相位变化会影响时钟的定时性能，因而通常不提倡采用在s d ht u 内传送的一次群信号( 2 0 4 8 m b i t s 或1 5 4 4 m b i t s ) 作为局间同步分配，而直接采用高比特率的s t m - n 信号传送同步信息。局内时钟间关系如图6 所示。局外占局外的茸他g - 8 l 褂图6 局内分配的同步网结构2 局间分配的同步网结构：类树型拓扑结构s d h 网内的所有节点都能同步。各级时钟关系如图7 所示。但低等级的时钟只能接收更高级或同一级时钟的定时，以避免形成定时信号的环路，造成同步的不稳定。此外，设计较低等级时钟时应有足够宽的捕捉范围，以便能够自动进行捕捉并锁定于基准定时信号。田7 局间分配得同步网结构2 4s d h 协议测试的意义光纤通信以其具有传输容量大、中继距离长、抗干扰能力强和性能价格比高等优点，已经在现代通信网中具有举足轻重的地位，并且成为信息传输的主要手段。当前世界各国大力发展的信息高速公路，其中个重点就是组建大容量的传输光纤网络，不断提高传输线路上的信号速率，扩宽传输频带。同时用户希望传输网能有世界范围的接口标准，从而使地球村中的每一个用户能随时随地便捷地通信。目前通信中使用的时分多路复用传输系统主要有准同步数字系列( p d h ) 和同步数字系列( s d h ) 。传统的由p d h 传输体制组建的传输网，由于其复用的方式很明显的不能满足大容量传输的要求，另外p d h 体制的地区性规范也使网络互连增加了难度，由此看出在通信网向大容量、标准化发展的今天，p d h 的传输体制已经愈来愈成为现代通信网的瓶颈，翩约了传输网向更高的速率发展。s d h 传输体制是针对p d h 的局限性进化而来的，它具有p d h 体制所无可比拟的优点，是不同于p d h 体制的全新的一代传输体制，与p d h 相比在技术体制上进行了根本的变革。s d h 协议在光纤通信中的地位日渐突出，为了今后它在实际中得到最有效的利用，s d h 协议的一致性测试势在必行。2 1第三章协议的形式化建模3 1 形式化描述方法形式化描述方法【5 】并不是新兴的事物，它已经经历了一个很长的发展时期。目前已经得到广泛应用的形式化描述方法v d m ( v i e 加ad e v e l o p m e n tm e t h o d ) ，1 9 7 1 年就已经开始应用了。h o a r e 于1 9 7 8 年首先提出了他的形式化描述语言c s p( c o m m u n i c a t i o ns e q u e n t i a lp r o c e s s ) 。z 语言从7 0 年代末已经开始开发了。事实上，第一个形式化描述语言b a c k u s - n a u r f o r m ( b n f ) 早在1 9 5 9 就已经出现了，形式化描述方法不仅可以用来描述和定义一个系统的行为和动作，而且可以用来验证和测试一个系统设计和实现是否满足一个系统功能的要求。由于不同规范、模型、验证和测试使用不同的形式化描述方法，所以导致它们有不同的精确程度。一种形式化描述方法可以简单的表示为数学模型和程序语言概念的结合：形式化描述方法= 数学模型+ 程序语言概念3 1 1 形式化描述方法的特性形式化描述方法是指在描述、设计和构建计算机系统和软件的过程中所使用的基于形式逻辑和离散数学的方法和技术。它具备以下重要的特性：1 数学模型：2 它是否可以表达“做什么”而不需要说“怎样做”；3 形式化的语法：4 它是否可以方便的应用有效的工具来进行自动化分析。3 1 2 形式化描述方法的能力形式化描述方法的描述能力可以粗略的分为以下三个级别：1 形式化描述系统的各个部分；2 不仅可以描述系统的各个部分，而且可以在此基础上进行手工的证明，这样就可以使用详细的规范描述推导出更加抽象的系统规范；3 存在算法可以通过使用计算机来自动的完成级别2 的手工证明。3 1 3 使用形式化描述方法的好处形式化描述方法在协议开发中起到的作用是多方面的。协议规范的描述是协议开发的基础。一般非形式化的描述可能导致描述的不明确和不一致。如果描述的不明确和不一致导致协议设计，协议实现出现错误，将来的修改、维护所要付出的代价就非常大。如果导致的错误没有被发现，则会影响协议的可靠和使用。形式化描述方法则要求描述的明确性，而描述的不一致性也就相对易于发现。使用形式化描述方法的好处有【27 j ：1 使用形式化描述方法所描述的协议规范是精确的；2 可以通过严格的分析来确定给定规范的正确性和一致性；3 协议的形式化规范可以作为协议验证和协议测试的基础；4 协议的形式化描述可以帮助协议验证和协议测试自动化或半自动化完成；5 协议的形式化描述可以作为一个协议的形式化文档；6 协议设计者可以形式化描述协议，保证协议设计的精确性、一致性和正确性。3 1 4 形式化描述方法的分类随着形式化描述方法在系统开发中的应用越来越广泛，形式化描述方法逐渐成为提高软件系统，特别是安全攸关系统的安全性与可靠性的重要手段。然而，在实际的通信协议的设计、开发中，选择哪一种形式化描述方法才是最适当的呢? 每一种形式化描述方法都有它的优点，对描述某些特定类型的系统可能比其它的形式化描述方法更加合适。这些形式化描述方法大致可以划分为两类【5 】，如图8 所示：1 面向属性的：是通过系统的属性来间接的描述系统；2 面向模型的：是通过对系统建模来直接描述系统；1 ) 面向状态的：描述系统的状态以及与之相关的变迁；2 ) 面向变迁的：无须参考具体的状态，而直接描述变迁。商瞰技术图8 形式化描述方法分类实际上，对形式化描述方法的分类是很难的，有的形式化描述方法可能同时属于多个类别，这主要依赖于该形式化描述方法在实际工程中如何运用。但总的来说，上述划分有助于比较各类形式化描述方法的异同。3 2 形式化模型与协议的适应性协议模型技术是协议工程的核心技术之一，它是协议工程的基础。形式描述语言总是以某种模型技术为基础，协议的正确性验证必定基于某种模型技术，协议自动化实现以及协议测试等都以某种模型技术为基础。目前，协议工程所采用的模型技术全部来自数学家以及计算机科学理论家所提出的一些数学模型( 或方法) 和自动化模型( 或程序模型) ，从事协议工程的学者也许会提出一些新的模型。常用的通信协议的形式化模型方法有有限状态机模型f s m 2 8 j ( f i n i t es t a t em a c h i n e ) ，消息序列图m s c ，p e t r i 网( p e t r in e t ：p n ) 2 9 1 ，时序逻辑( t e m p o r a ll o g i c ：t l ) 3 0 l ，通讯进程演算( c a l c u l u so f c o m m u n i c a t i n gs y s t e m s ：c c s ) 3 h 、过程语言( p r o c e d u r a ll a n g u a g e ) 【3 2 】等；常用的形式化描述语言有l o t o s l 4 1 1 、e s t e l l e 3 7 】、s d l 38 1 、z 语言口9 1 等。以上几种形式化模型语言在当前的协议工程领域得到了广泛的应用，但同时也要注意到它们都存在着不同程度的缺陷，如当进行大型的复杂协议的构造时，f s m 和p e t t i 网模型将面临状态爆炸的问题。以上各种通信协议的形式化描述方法在描述协议的过程中，其描述能力、分析能力、测试用例形式化生成能力也有各自的长处和短处，所以一种协议形式化描述方法在描述特定的协议时可能存在不足。3 2 1 协议性质协议性质，也就是全局系统性质，指一个好协议应该具有的性质，它包括四个主要方面：活动性、安全性、一致性和完整性。1 活动性( 1 i v e n e s s ) ：协议活动性是指协议运行时一些好事情会发生。这些好事情包括：预定的事件会产生，指定的协议状态会达到，应该进行的协议行动会进行等等。协议的活动性体现在终止性( t e r m i n a t i o n ) 和进展性( p r o g r e s s )两个方面，或者说，如果协议有终止性和进展性，它就有活动性。终止性指协议从任何一个状态开始运行，总能正确地达到终止状态：进展性则指协议从初始状态运行，总能正确地达到指定状态。在某些情况下，终止状态和初始状态是同的。这样，协议从初始状态开始运行总能正确的回到初始状态，并可反复运行，这就是协议的回归性( r e c u r r e n c e ) ：回归性= 终止性+ 进展性= 活动性2 安全性( s a f e t y ) ：协议安全性是指协议运行时没有坏事情出现。这些坏事情包括不可接受事件，不可迸一步向前状态、错误的行为、错误的条件、错误的环境、变量值越界等等。坏事情一般会导致两种现象：死锁( d e a d l o c k ) 或是活锁( 1 i v e l o c k ) 。死锁指协议堵塞在某一个状态而无法向前，活锁指协议做无意义的循环；3 一致性( c o n s i s t e n c y ) ：协议一致性是指协议服务行为和协议性质一致。n 层协议的用户所要求的服务以及它所能观察到服务性质与n 层协议内部机制所表现出的总体行为和性质是一致的，那么协议就有一致性。一致性包括两个方面：协议应该提供用户要求的服务和协议无需提供用户没有要求的服务；4 完备性( c o m p l e t e n e s s ) ：完备性是指协议性质完全符合协议环境的各种要求，即协议的构造考虑了用户要求、用户特点、通道性质、工作模式等各种潜在因素的影响，考虑了各种错误事件，异常情况处理：5 备注：关于协议性质还有多种说法，有的学者将协议分为一般性质和特殊性质。一般性质指那些与协议具体内容无关的性质，特殊性质指那些与协议具体内容相关的性质。安全性和活动性属于一般性质，而致性和完备性属于特殊性质。协议的正确性验证着重一般性质，而协议测试着重于特殊性质。3 2 2 协议模型的选取原则我们根据以下两个方面来选取协议模型：i 能够方便充分的表示协议元素和通道的各种性质；2 容易观察协议性质( 全局系统性质) 。达到以上两点的模型技术就是一种理想的模型技术。“方便充分的表示”意味着所采用的模型技术有足够强的表达能力和实用性，“容易观察”则意味着协议验证和测试容易实现。3 2 3 几种典型的形式化模型，描述语言1 有限状态机f s m ( f i n i t es t a t em a c h i n e ) 是最常用的协议形式化描述技术。f s m 模型包括基本f s m 、扩展f s m ”刘( 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 ) 、结构化f s m 、通信f s m ( 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 ) 。2 在状态转移图中能描述的东西，都可以用p e t r i 网p 4 j 来描述。但p e t r i 网比状态转移图的描述能力强，是逻辑上的可解释模型中描述能力最强的一种。3 m s c 又叫信号顺序图，流图，消息流图等。很早就在开始设计现场使用，但只到1 9 9 3 年才成为国际标准。4 数学家的任务之一是从现实世界中识别并定义一类目标，然后对该类目标建立一套严密的演算系统。进程( p r o c e s s ) 是计算机科学与工程中广泛使用的概念，一些数学家已成功地将它们作为演算目标建立了几种不同的进程代数( t h ea l g e b r a o f p r o c e s s ) 系统。进程代数的开拓性工作是由r m i l e r 进行的，他提案的通讯进程演算c c s ”1 ( t h ec a l c u l af o rc o m m 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 ! ”j ( t h ec o m m u n i c a t i n gs e q u e n t i a lp r o c e s s e s ) 。c s p 一经出现就被广泛地应用于计算机科学的诸多领域，如网络通信协议的形式化描述等。5 从逻辑角度来说，时序逻辑t l 口0 】是模态逻辑的扩充，以状态为可能世界，以状态的演变次序关系为可能世界间的可到达关系。时序逻辑的种类很多，随时间结构的不同，算子的选择也有差异。6 s d l ( s p e c i f i c a t i o na n dd e s e f i p t i o nl a n g u a g e ) i j ”言是由c c i t t ( i t u t ) 组织开发的电信领域的国际标准。它是一种说明与描述语言，在s d l 中，被描述的系统是由若干连接的抽象机器表示的，而抽象机器之间的通信采用异步机制。s d