四、协议的形式描述语言主要内容形式化方法协议的形式化模型协议的形式描述语言SDL北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide11、形式化方法北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide2形式化方法的引入系统行为的复杂性增大了行为描述的难度，必须借助一种语言或一种技术来准确的描述系统的行为。自然语言具有冗长、不完整、语句容易产生二义性、结构性差和没有描述标准等缺点。国际标准化组织建议用形式化方法来描述复杂的系统。形式化方法使得对通信系统的描述、实现和测试变得容易。北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide3形式化方法的特点与自然语言相比，形式化方法具有以下的特点：形式化的语法形式化的语义清楚的概念模型界面统一表示强大的表达和描述功能有助于系统的实现和完善北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide4形式化方法的最终目的为开发者提供一种分析、设计的方法作为对开发结果进行验证、测试的基础为设计和应用人员提供交流的途径作为开发文档易于今后的维护和再开发北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide52、协议的形式化模型北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide6协议的形式化模型有限状态机（FSM）Petri网时态逻辑TL通信进程演算北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide7有限状态自动机（1）有限状态自动机可定义为一个四元系统<S，i，E，T>，其中：–S：系统状态集，状态数有限；–i：系统初始状态，i∈S;–E：输入字母集；–T：转移函数集，是从SⅹE到S的映射；北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide8有限状态自动机（2）单比特奇偶检验器的有限状态自动机010偶1奇北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide9扩展有限状态自动机（1）扩展有限状态自动机定义为一个四元系统<S，i，E，T>，其中：–S：系统状态集，状态数有限；–i：系统初始状态，i∈S;–E：输入事件集；–T：转移函数，是从SⅹE到S的映射北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide10扩展有限状态自动机（2）转换函数的定义：tSj∈T，Si，Sj∈SSi–t=e/p：a；或–t=e/a；或–t=e其中：e∈E，p为谓词，表示条件；a表示动作北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide11扩展有限状态自动机（3）等待DCDCTDISreq/DRAK未连接TCONreq/CR已连接CC/TCONconf等AK等CCTDTreq/DT传输层协议机北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide12可通信的扩展有限状态自动机系统的行为通过可通信的扩展有限自动机来描述–系统由扩展的有限状态自动机组成–扩展的有限状态自动机具有与外界通信的能力：输入/输出动作北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide13Petri网Petri网的概念最早是由德国的CarlAdamPetri于1962年提出的。它是一种适合于并发、异步、分布式系统描述与分析的图形数学工具。Petri网已成为网络协议分析和设计的典型形式化模型之一。北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide14时态逻辑（TL）它涉及含有时间信息（现在、过去、将来、之前、之后等）的事件、状态及其关系的命题、谓词和演算。北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide15通信进程演算（CCS）是计算机通信系统的基本理论模型，也是许多形式化语言的基础。CCS的基本成分是事件和进程，而进程是通过顺序、选择和并行三个基本算子来定义的。P1=a.b.NILP2=a.b.P2（顺序）P1=a.(c.NIL+b.NIL)（选择）P1=Q2IQ3（并行）北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide163、协议的形式描述语言北京邮电大学计算机科学与技术学院通信技术中心卞佳丽Slide17ESTELLE为准确描述OSI协议，ISO的FDT（形式描述技术）小组于20世纪80年代初开始进行形式描述语言的开发研究。最初提出了20多种方法，大致可归结为2类：基于有限状态机语言类和基于代数方法语言类。ESTELLE（一种扩充的有限状态机语言）是前一类语言的典型代表。1989年，ISO公布了作为形式描述技术国际标准之一的ESTELLE。ESTELLE