学海网

《网络协议工程》英文课程教案
Chapter 1: Foreword before the lecture begin
Chapter 2：Computer network protocol engineering——
Chapter 3: Petri net and colored Petri net ——Concepts and
Chapter 4: FSM (Finite State Machine) ——Concepts and Extension
Chapter 5：Brief Introduction to SDL，Estelle and LOTOS
Chapter 6：Protocol Verification and Testing——Concepts and Approaches

Chapter 1: Foreword before the lecture begin
Course content：
1.1Some Requirements: 
(1)Not necessary to present but must keep silent.
(2)Questions and good suggestions are encouraged to be given out in time during lecturing hours.
(3)Self-study with the help of Internet are greatly encouraged. When you are involved into one practice project, you must investigate the related knowledge from Internet.
1.2Practice project: 
(1)Theoretical analysis on some interesting issues;
(2)Formal modeling and specification on some interesting protocols;
(3)Implementation analysis on some protocols based on open-source code on Internet.
1.3Communications
1.3.1Communications between people: Syntax and Semantic issues: Languages
Communications between computers: Syntax and Semantic issues: Protocols
1.3.2Communication networks

Chapter 6 Protocol Verification and Testing——Concepts and Approaches
Course content：
6.1Verification
验证是对协议本身的逻辑正确性进行校验的过程。
协议验证有两种途径：
协议分析：对已设计的协议进行分析和校验（非形式化设计方法产生的协议），通常说协议验证指协议分析；
协议综合：将协议设计过程和验证过程融合在一起，通过一组规则确保所设计的协议是正确，从一些基本协议模块（正确的）产生所希望的目标协议。由协议需求描述产生一个目标协议，即：力图使用一组能确保所产生的协议是正确的规则，由“协议零部件”装配出一个符合要求的目标协议。
6.1.1Protocol Analysis
协议分析包括：可达性分析（Reachability）、等价性分析（Equivalence）、不变性分析（Invariance）、符号执行（Symbol Execution）、模拟（Simulation）。
协议分析的关键是形成确定算法，从而可以借助于分析工具在计算机上自动或半自动进行。
协议分析可在任何表达形式上进行：自然语言描述的协议的非形式化文本；基于形式化描述语言的协议规范：如Estelle、LOTOS、SDL等；基于模型技术表达的协议模型：如FSM、PetriNet、CCS等；基于程序设计语言描述的协议代码：如C、Pascal等。
6.1.2可达性分析
基于FSM，试图产生和检查协议所有或部分可达状态；
可达状态：协议（机）从初始状态开始经历有限次转换之后可到达的状态；所有可达状态构成可达树（Reachability Graph）
可达性分析：主要是产生和检查可达图，判定是否存在死锁、活锁等协议错误。
可达性分析主要技术和目的：怎样找出所有可达状态，构成可达图；怎样检测死锁、活锁等协议错误；怎样解决状态爆炸问题。
6.1.3不变性分析
系统不变性：一个系统的某个性质能用一个确定的逻辑表达式描述，而且恒为真（不随系统的状态变化或执行序列而改变）
协议的不变性分析：正确地找出协议（系统）的不变性质，形成严格定义的不变性表达式，以某种方式执行协议，验证不变性表达式是否恒为真。
不变性分析途径：不变性证明系统（如：采用归纳法）、不变性监测系统。
6.1.4等价性分析
等价：某种程度上的“相同”和“无差别” ；
两个协议模型或协议规范是等价的，它们可以互换。如果一个正确，则另一个也是正确的。
协议等价性分析：利用“等价”方法简化FSM图等；证明两个协议的FSM图或CCS表达式是等价的；证明协议规范和协议的服务规范是一致的。
等价性划分：按照等价的含义和等价的强弱程度排列划分：
观察等价：状态到状态变化观察到的协议行为没有差别；
测试等价：相同测试序列所观察到的行为没有差别；
跟踪等价：执行的事件序列相同；
实现等价：一个协议的做的事情能被另一个模仿，反之亦然。
6.2Testing