《网络协议工程》课程教案.doc

《网络协议工程》课程教案
Chapter 1: Foreword before the lecture begin
Course content：
1.1 Some 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.2 Practice 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.3 Communications
1.3.1 Communications between people: Syntax and Semantic issues: Languages
Communications between computers: Syntax and Semantic issues: Protocols
1.3.2 Communication networks

1.4 Overview on computer networks
1.4.1 Layered architecture
OSI/RM defined 7 layer: Physical Layer, Data link layer, Network layer, Transport layer, Session layer, Representation layer, Application layer
1.4.2 Typical protocols in layered network architecture
Data-link layer: from ALOHA to CSMA/CD, PPP, MPLS;
1.4.3 Some Bearers for IP transferring
(1) Circuit-switched Communication Network: typical telecom networks;
(2) Packet-Switched Communication Network: X.25, FR, ATM
1.4.4 Protocol service model between layer n and n+1

1.4.5 LAN and inter-net
1.4.6 LAN and its standardization
IEEE 802.X divided DLL into MAC layer and LLC; Ethernet MAC uses CSMA/CD, and CSMA/CD is one kind of random access mechanisms to do with a shared media; The oldest random access mechanism is ALOHA protocol; Ethernet MAC has 48-bit MAC address (physical address of NIC)
1.5 Protocol in layered computer network
The essence in the layered network architecture is protocol stack, One protocol is developed to complete a task or to provide one service, Read and implement one or more protocols by yourself

Chapter 2：Computer network protocol engineering——Concepts and overview on its methodology
Course content：
2.1 Communications and Protocols
(1) How to organize the entities in collection of communication network?
(2) How to communicate very well?
(3) What is a protocol?
2.2 Protocol engineering

2.3 Protocol engineering techniques

2.4 Layers in a communications architecture
The capabilities provided by the entities in the (N)-layer (and all layers below) at the boundary between the (N)-layer and (N+1)-layer is called the (N)-service. The (N+1)-entities access the (N)-service by (N)-service-access-points (SAP).
2.5 Service Definition
2.6 Protocol Definition
2.7 Protocol engineering activities

28 Formal methods are introduced
(1) To obtain complete and unambiguous specifications in the design stages of protocol engineering, formal methods can be used;
(2) Formal methods are those which are based on mathematics. This means there is no room for misinterpretation of the formal specifications;
(3) Formal methods are those which are based on mathematics. This means there is no room for misinterpretation of the formal specifications;
(4) A major advantage of using formal methods in protocol engineering is the ability to formally reason about the properties of a protocol, including verifying it against the services.

Chapter 3: Petri net and colored Petri net ——Concepts and applications
Course content：
3.1 Introduction to Petri网
Philosophy and History of Petri Nets: The Name of the Game; System Modeling; History of Petri Nets.
3.2 网系统的定义
网系统：六元组å=（P，T；F，K，W，M0），其中N=（P，T；F）是网，K、W、M0分别是N的容量(capacity)函数、权(weight)函数和初始标识（Initial Markings）。
网执行的分析和说明：网系统的并发性分析可以通过建模工具进行分析，也可以通过矩阵变换进行分析，如：M0=(3,2,0)， M1=(1,1,3)。
3.3 Petri网的定义
在网系统中，当K为无穷，W=1时，网系统演化为Petri网：Petri Nets=（P，T；F，M0）；对Petri网的研究主要包括网系统的以下特性：活性(Liveness)、可达性(Reachability)。
3.4 基本网系统和高级网系统
在C/E网基础上扩展的新模型、概念和分析方法。早期的网模型在理论上归结为基本网(Elementary Net)；对Petri网增加变迁的优先级、时间延迟、全程变量等概念满足实际应用建模的要求，产生了各种各样的高级网(High-Level Nets)理论。
3.5 着色Petri网(CPN)的形式化定义
A non-hierarchical CPN is a tuple CPN =（∑，P，T，A，N，C，G，E，I） satisfying the requirements below：
∑ is a finite set of non-empty types, called Color Set；
T is a finite set of transitions；
A is a finite set of arcs such that:P Ç T = P Ç A= T Ç A = F；
N is a node function, it is defined from A into（P´T）∪（T´P）；
C is a color function, it is defined from P into ∑, i. e. :C：P®∑
3.6 CPN的建模
Design/CPN工具：由美国麻省Meta软件公司与丹麦Aarhus大学合作开发的Linux下的CPN建模工具，通过X-Window图形界面，为用户提供了可视化的开发环境，可以进行CPN模型的创建、仿真和验证。
CPN建模示意：

Chapter 4: FSM (Finite State Machine) ——Concepts and Extension
Course content：
4.1 Introduction to FSM
FSM was introduced to meet requirements of scientific research and engineering; FSM, as a mathematical modeling methodology, can be used to describe physical phenomena as well as abstract concepts; FSM isn’t limited to one scientific field, instead, it can be applied universally; When FSM is used to describe one complicated system, the systematic model are abstracted as a “black-box”, whose input and output are only observable.
4.2 FSM definition
An FSM can be defined as a 5-tuple M = (I, O, S, δ,λ)
I: the finite non-empty set of input symbol
O: the finite non-empty set of output symbol
S: the finite non-empty set of state
δ: S X I → S, the state transition function
λ: S X I → O, the output function
4.3 How to design FSM
Design strategy：Synchronous or asynchronous；
Synchronous FSM：Clock-control mechanism is introduced, input event will be effective when the next clock comes
Asynchronous FSM：no clock-control mechanism, input event will lead to state change
Mealy or Moore
DFSM or NFSM
Encoding
FSM的优点：简单性、可预测性、易于实现、易于测试
4.4 进程代数
进程代数：将计算机科学与工程中的进程作为演算目标建立的代数系统；
CCS算子：CCS的理论比较深奥，但用于协议工程，有关定义和代数变换法则非常直观明了；三个基本算子（顺序、选择、并行）定义一个进程。
4.5 基于进程代数的模型和方法
CCS和CSP是进程代数方法的代表，是描述通信和并发的演算系统.它们均以进程为计算单位，进程的基本组成是原子性动作.所谓原子性，是指动作不可再分，且动作执行是瞬时的.在两个演算系统中，进程间交互以双方握手(handshake)来完成，是一种同步通信方式.同时，CCS和CSP都是既有模型又有演算.当然，CCS和CSP之间也有不同.CCS用同步树(synchronization tree)表示进程，或称为状态转移图；而CSP用失败集(failure set)表示进程.在CCS中，使用操作语义(互模拟语义)解释进程(的等价性)；而在CSP中，则使用指称语义(失败语义)解释进程(的等价性).

Chapter 5 Brief Introduction to SDL，Estelle and LOTOS
Course content：
5.1 形式化方法
形式化方法的最终目的是：为开发者提供一种分析的方法；作为对开发结果进行验证的基础；为设计人员和应用人员提供交流途径；作为开发文档能在将来再开发时使用。
理想的形式化方法应该既能描述系统的行为特征，又能进行操作。
在系统需求分析和设计阶段，它应该是一种描述语言，在系统实现阶段它应该是一种编程语言。
5.2 SDL
Specification and Description Language(功能规格和描述语言) 是ITU-T（CCITT） 标准语言,定义在Z.100中
SDL是CCITT为描述远程通信而定义的一种形式描述技术，基于EFSM的。其数据部分采用抽象数据类型描述，程序变量和数据结构用CCITT定义的程序设计语言CHILL来表示
SDL Definition：Specification and description language (SDL) is an object-oriented, formal language defined by The International Telecommunication Union-Telecommunications Standardization Sector (ITU-T) as recommendation Z.100.
The language is intended for the specification of complex, even-driven, real-time, and interactive applications involving many concurrent activities that communicate using discrete signals
Structure：SDL comprises four main hierarchical levels: System、Blocks、Processes、Procedures
5.3 Estelle
一种基于扩展FSM的形式化描述技术，它可以把系统描述为具有层次结构的一些相互通信的模块(Modules)：系统被看作由许多相互通信的模块分层嵌套而构成；系统的每一级可有多个模块；每个模块可通过通道以异步方式和其他模块（父模块、兄弟模块、子模块）通信；这些模块的行为(Behaviors)用可相互通信的非决定型(Nondeterministic)扩展有限状态机EFSM来描述。
Estelle采用了PASCAL程序设计语言的子集描述EFSM中的数据部分，特别是各种交互参数的定义.
5.4 LOTOS
LOTOS: Language of Temporal Ordering Specification)--通过定义事件的时序关系来描述系统。适应协议工程、分布处理和并行处理要求而产生，一个系统被看着多个相互作用的子进程组成的进程。
LOTOS的基本描述对象是并发进程，进程的行为用它与外部环境之间的交互动作序列来描述。LOTOS主要基于R. Miler的通信系统演算CCS，另外用一种抽象数据结构的代数表示法ACT ONE来描述系统的数据部分。
LOTOS两个组成部分：
基于进程代数CCS：有所扩展，描述进程的行为和相互作用，用行为算子组成行为表达式，描述多个协议事件和行为。
基于抽象数据类型ACT ONE，描述数据结构和值表达式，描述基于分布，并发，消息驱动的系统，描述的协议容易转换成CCS模型，时态逻辑模型，FSM模型，Petri模型。
5.5 LOTOS将一个系统看做多个相互作用的子进程组成的进程，每个子进程又是由多个子进程构成。由此可见，LOTOS描述一个系统的方法是一种由高层向低层逐级定义进程的方法。
5.6 形式描述语言的比较

由于不同的模型具有不同的语义基础，适用于不同的对象，在实际中，我们应根据目的的不同，选择不同的模型。
Estelle是pascal语言的扩充，用Estelle描述的协议容易转换成pascal或c代码。因此，它是一种面向协议实现的FDL。若以实现为目标，则应选择Estelle进行描述，通过使用过程语言pascal，可较详细地描述协议细节。用Estelle描述的协议易于提取FSM模型和Petri模型，对并发、不确定性、超时、异步通讯状态转换有较强的表达能力，但对递归、共享通道、同步通讯、协议性质的表示缺少有力的手段，不容易提取转变成TL和CSS模型，并且由于在描述阶段涉及过多的协议细节，这样势必给形式描述的抽象程度带来影响。
LOTOS能提供较好抽象程度的形式描述，侧重于通过定义系统外部可见行为中事件的次序关系来描述系统，而不关心协议实体的内部变化，可区别内部事件和外部事件，较有利于判断死锁，可描述非确定性系统，同时包含一套严谨的数学公理化系统，因而使得该语言具有较高的抽象程度，有利于对协议的各种性质进行分析验证。若以验证为目标，则可以选择LOTOS来描述。其弱点在于缺乏状态概念，不易直接通过编译器自动生成实现代码，往往需要形式描述风格变换。
SDL是一种基于扩展状态变换图和抽象数据类型的混合技术，主要用于描述电信系统和开发控制软件，已被电信公司广泛用于描述电子分组交换系统但也可以用它来描述协议，比较适用于描述用扩展有限状态机进行模拟的系统，尤其是交互式实时系统。其不足表现在：语义需重新定义，缺乏分析技术，实现不具有独立性。

Chapter 6 Protocol Verification and Testing——Concepts and Approaches
Course content：
6.1 Verification
验证是对协议本身的逻辑正确性进行校验的过程。
协议验证有两种途径：
协议分析：对已设计的协议进行分析和校验（非形式化设计方法产生的协议），通常说协议验证指协议分析；
协议综合：将协议设计过程和验证过程融合在一起，通过一组规则确保所设计的协议是正确，从一些基本协议模块（正确的）产生所希望的目标协议。由协议需求描述产生一个目标协议，即：力图使用一组能确保所产生的协议是正确的规则，由“协议零部件”装配出一个符合要求的目标协议。
6.1.1 Protocol 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.2 Testing
测试是试图通过实验的方法找出错误的过程。
在测试过程中既要模拟被测试方正常工作的情况，也要模拟异常使用的情况；既要模拟被测试方单独运行的情况，也要模拟若干个被测试方互相通信的情况。
由于无法对一个系统进行无穷尽的测试，所以测试并不能保证被测试方的完全正确性。
协议测试的基本出发点— — 只能证明“存在错误”，而不能证明“不存在错误”
6.2.1 Protocol Testing
协议测试理论是协议工程学的一个重要分支。
研究协议测试理论的原因在于一个标准化的协议并不能确保该协议的实现之间能够成功的进行通信。
由于协议标准目前基本上是使用自然语言描述的，实现者对于协议的不同理解会导致不同的协议实现，甚至有时会是错误的实现。
需要一种有效的方法来对协议实现进行判别，这就是“协议测试”。
6.2.2 从测试到协议测试
协议测试被人为地分成三种类型：一致性测试(Conformance Testing)、互操作性测试(Interoperability Testing)、性能测试(Performance Testing)。
协议测试理论包含了协议测试的整个过程，其主要研究内容以下几个方面：
测试方法：研究在被测系统提供不同的可访问程度时，组成测试系统的多个测试器相对于被测系统的配置方法。
测试生成：主要关注于如何从协议标准的描述中获得协议测试所需要的测试集。
测试集描述：其目的是寻找一种合适的语言或公式，从而能以简洁、通用和结构化的方式表达测试集。
测试执行：协议测试过程中关键阶段，它将解释测试例的涵义并作出最终的测试判决。
6.2.3 一致性测试过程

6.3 Tree and Tabular Combined Notation
TTCN-3 is the standardised (black-box) test specification and test implementation language，最初这种语言是为明确指定测试指令序列而开发的，它与内部实现没有关系：By the European Telecommunications Standards Institute (ETSI) from 1999 to 2001. Based on the experiences from previous TTCN versions.
6.4 TTCN概念与相关定义
TTCN被定义成为一个由静态说明部分和动态行为部分组成的整体。静态说明部分用于协议的静态信息描述。如协议数据单元PDU和抽象服务原语ASP、控制观察点PCO、定时器、测试集变量和测试例变量的描述。 ---> Data
动态行为描述部分提供了与消息的接受和发送相关的操作和操作符。 ---> Behaviour
TTCN的层次结构：TTCN采用树表结合的方法，即适用于机器识别，也便于人类阅读；TTCN清楚地反映测试集的层次结构，完整地表示了测试组，测试例及测试步。
6.5 协议一致性测试框架组成
ASPs：IUT和UT之间通过抽象服务元语（Abstract Service Primitives简称ASPs）进行通信。

PDUs：从概念角度，IUT和LT通过协议数据单元（Protocol Data Units简称PDUs）交换数据；
两者的联系：从实际角度，PDUs采用ASPs对基本服务动作进行编码，即PDUs不是直接进行交互，而是CTMF允许根据PDUs的编码进行交互，即在一个抽象的测试中使用PDUs进行交换，所以ASPs与PDUs不再加以区分。
TCP：测试协调过程（Test Coordination Procedures）来协调LT和UT的动作，这在LT和UT是两个独立的过程时十分必要 。
测试方法分类：在CTMF中测试方法可分为局部的、分布的、协调的和远程的测试几种。它们的主要不同是对LT和UT的协调以及对它们的控制与观察程度不同。