《网络协议工程》课程教案.docx
《《网络协议工程》课程教案.docx》由会员分享，可在线阅读，更多相关《《网络协议工程》课程教案.docx（15页珍藏版）》请在冰点文库上搜索。
《网络协议工程》课程教案
《网络协议工程》课程教案
Chapter1:
Forewordbeforethelecturebegin
Coursecontent：
1.1SomeRequirements:
（1）Notnecessarytopresentbutmustkeepsilent.
（2）Questionsandgoodsuggestionsareencouragedtobegivenoutintimeduringlecturinghours.
（3）Self-studywiththehelpofInternetaregreatlyencouraged.Whenyouareinvolvedintoonepracticeproject,youmustinvestigatetherelatedknowledgefromInternet.
1.2Practiceproject:
（1）Theoreticalanalysisonsomeinterestingissues;
（2）Formalmodelingandspecificationonsomeinterestingprotocols;
（3）Implementationanalysisonsomeprotocolsbasedonopen-sourcecodeonInternet.
1.3Communications
1.3.1Communicationsbetweenpeople:
SyntaxandSemanticissues:
Languages
Communicationsbetweencomputers:
SyntaxandSemanticissues:
Protocols
1.3.2Communicationnetworks
1.4Overviewoncomputernetworks
1.4.1Layeredarchitecture
OSI/RMdefined7layer:
PhysicalLayer,Datalinklayer,Networklayer,Transportlayer,Sessionlayer,Representationlayer,Applicationlayer
1.4.2Typicalprotocolsinlayerednetworkarchitecture
Data-linklayer:
fromALOHAtoCSMA/CD,PPP,MPLS;
1.4.3SomeBearersforIPtransferring
（1）Circuit-switchedCommunicationNetwork:
typicaltelecomnetworks;
（2）Packet-SwitchedCommunicationNetwork:
X.25,FR,ATM
1.4.4Protocolservicemodelbetweenlayernandn+1
1.4.5LANandinter-net
1.4.6LANanditsstandardization
IEEE802.XdividedDLLintoMAClayerandLLC;EthernetMACusesCSMA/CD,andCSMA/CDisonekindofrandomaccessmechanismstodowithasharedmedia;TheoldestrandomaccessmechanismisALOHAprotocol;EthernetMAChas48-bitMACaddress（physicaladdressofNIC）
1.5Protocolinlayeredcomputernetwork
Theessenceinthelayerednetworkarchitectureisprotocolstack,Oneprotocolisdevelopedtocompleteataskortoprovideoneservice,Readandimplementoneormoreprotocolsbyyourself
Chapter2：
Computernetworkprotocolengineering——Conceptsandoverviewonitsmethodology
Coursecontent：
2.1CommunicationsandProtocols
（1）Howtoorganizetheentitiesincollectionofcommunicationnetwork?
（2）Howtocommunicateverywell?
（3）Whatisaprotocol?
2.2Protocolengineering
2.3Protocolengineeringtechniques
2.4Layersinacommunicationsarchitecture
Thecapabilitiesprovidedbytheentitiesinthe（N）-layer（andalllayersbelow）attheboundarybetweenthe（N）-layerand（N+1）-layeriscalledthe（N）-service.The（N+1）-entitiesaccessthe（N）-serviceby（N）-service-access-points（SAP）.
2.5ServiceDefinition
2.6ProtocolDefinition
2.7Protocolengineeringactivities
2.8Formalmethodsareintroduced
（1）Toobtaincompleteandunambiguousspecificationsinthedesignstagesofprotocolengineering,formalmethodscanbeused;
（2）Formalmethodsarethosewhicharebasedonmathematics.Thismeansthereisnoroomformisinterpretationoftheformalspecifications;
（3）Formalmethodsarethosewhicharebasedonmathematics.Thismeansthereisnoroomformisinterpretationoftheformalspecifications;
（4）Amajoradvantageofusingformalmethodsinprotocolengineeringistheabilitytoformallyreasonaboutthepropertiesofaprotocol,includingverifyingitagainsttheservices.
Chapter3:
PetrinetandcoloredPetrinet——Conceptsandapplications
Coursecontent：
3.1IntroductiontoPetri网
PhilosophyandHistoryofPetriNets:
TheNameoftheGame;SystemModeling;HistoryofPetriNets.
3.2网系统的定义
网系统：
六元组∑=（P，T；F，K，W，M0），其中N=（P，T；F）是网，K、W、M0分别是N的容量（capacity）函数、权（weight）函数和初始标识（InitialMarkings）。
网执行的分析和说明：
网系统的并发性分析可以通过建模工具进行分析，也可以通过矩阵变换进行分析，如：
M0=（3,2,0），M1=（1,1,3）。
3.3Petri网的定义
在网系统中，当K为无穷，W=1时，网系统演化为Petri网：
PetriNets=（P，T；F，M0）；对Petri网的研究主要包括网系统的以下特性：
活性（Liveness）、可达性（Reachability）。
3.4基本网系统和高级网系统
在C/E网基础上扩展的新模型、概念和分析方法。
早期的网模型在理论上归结为基本网（ElementaryNet）；对Petri网增加变迁的优先级、时间延迟、全程变量等概念满足实际应用建模的要求，产生了各种各样的高级网（High-LevelNets）理论。
3.5着色Petri网（CPN）的形式化定义
Anon-hierarchicalCPNisatupleCPN=（∑，P，T，A，N，C，G，E，I）satisfyingtherequirementsbelow：
∑isafinitesetofnon-emptytypes,calledColorSet；
Tisafinitesetoftransitions；
Aisafinitesetofarcssuchthat:
P⋂T=P⋂A=T⋂A=Φ；
Nisanodefunction,itisdefinedfromAinto（P⨯T）∪（T⨯P）；
Cisacolorfunction,itisdefinedfromPinto∑,i.e.:
C：
P→∑
3.6CPN的建模
Design/CPN工具：
由美国麻省Meta软件公司与丹麦Aarhus大学合作开发的Linux下的CPN建模工具，通过X-Window图形界面，为用户提供了可视化的开发环境，可以进行CPN模型的创建、仿真和验证。
CPN建模示意：
Chapter4:
FSM（FiniteStateMachine）——ConceptsandExtension
Coursecontent：
4.1IntroductiontoFSM
FSMwasintroducedtomeetrequirementsofscientificresearchandengineering;FSM,asamathematicalmodelingmethodology,canbeusedtodescribephysicalphenomenaaswellasabstractconcepts;FSMisn’tlimitedtoonescientificfield,instead,itcanbeapplieduniversally;WhenFSMisusedtodescribeonecomplicatedsystem,thesystematicmodelareabstractedasa“black-box”,whoseinputandoutputareonlyobservable.
4.2FSMdefinition
AnFSMcanbedefinedasa5-tupleM=（I,O,S,δ,λ）
I:
thefinitenon-emptysetofinputsymbol
O:
thefinitenon-emptysetofoutputsymbol
S:
thefinitenon-emptysetofstate
δ:
SXI→S,thestatetransitionfunction
λ:
SXI→O,theoutputfunction
4.3HowtodesignFSM
Designstrategy：
Synchronousorasynchronous；
SynchronousFSM：
Clock-controlmechanismisintroduced,inputeventwillbeeffectivewhenthenextclockcomes
AsynchronousFSM：
noclock-controlmechanism,inputeventwillleadtostatechange
MealyorMoore
DFSMorNFSM
Encoding
FSM的优点：
简单性、可预测性、易于实现、易于测试
4.4进程代数
进程代数：
将计算机科学与工程中的进程作为演算目标建立的代数系统；
CCS算子：
CCS的理论比较深奥，但用于协议工程，有关定义和代数变换法则非常直观明了；三个基本算子（顺序、选择、并行）定义一个进程。
4.5基于进程代数的模型和方法
CCS和CSP是进程代数方法的代表，是描述通信和并发的演算系统.它们均以进程为计算单位，进程的基本组成是原子性动作.所谓原子性，是指动作不可再分，且动作执行是瞬时的.在两个演算系统中，进程间交互以双方握手（handshake）来完成，是一种同步通信方式.同时，CCS和CSP都是既有模型又有演算.当然，CCS和CSP之间也有不同.CCS用同步树（synchronizationtree）表示进程，或称为状态转移图；而CSP用失败集（failureset）表示进程.在CCS中，使用操作语义（互模拟语义）解释进程（的等价性）；而在CSP中，则使用指称语义（失败语义）解释进程（的等价性）.
Chapter5BriefIntroductiontoSDL，EstelleandLOTOS
Coursecontent：
5.1形式化方法
形式化方法的最终目的是：
为开发者提供一种分析的方法；作为对开发结果进行验证的基础；为设计人员和应用人员提供交流途径；作为开发文档能在将来再开发时使用。
理想的形式化方法应该既能描述系统的行为特征，又能进行操作。
在系统需求分析和设计阶段，它应该是一种描述语言，在系统实现阶段它应该是一种编程语言。
5.2SDL
SpecificationandDescriptionLanguage（功能规格和描述语言）是ITU-T（CCITT）标准语言,定义在Z.100中
SDL是CCITT为描述远程通信而定义的一种形式描述技术，基于EFSM的。
其数据部分采用抽象数据类型描述，程序变量和数据结构用CCITT定义的程序设计语言CHILL来表示
SDLDefinition：
Specificationanddescriptionlanguage（SDL）isanobject-oriented,formallanguagedefinedbyTheInternationalTelecommunicationUnion-TelecommunicationsStandardizationSector（ITU-T）asrecommendationZ.100.
Thelanguageisintendedforthespecificationofcomplex,even-driven,real-time,andinteractiveapplicationsinvolvingmanyconcurrentactivitiesthatcommunicateusingdiscretesignals
Structure：
SDLcomprisesfourmainhierarchicallevels:
System、Blocks、Processes、Procedures
5.3Estelle
一种基于扩展FSM的形式化描述技术，它可以把系统描述为具有层次结构的一些相互通信的模块（Modules）：
系统被看作由许多相互通信的模块分层嵌套而构成；系统的每一级可有多个模块；每个模块可通过通道以异步方式和其他模块（父模块、兄弟模块、子模块）通信；这些模块的行为（Behaviors）用可相互通信的非决定型（Nondeterministic）扩展有限状态机EFSM来描述。
Estelle采用了PASCAL程序设计语言的子集描述EFSM中的数据部分，特别是各种交互参数的定义.
5.4LOTOS
LOTOS:
LanguageofTemporalOrderingSpecification）--通过定义事件的时序关系来描述系统。
适应协议工程、分布处理和并行处理要求而产生，一个系统被看着多个相互作用的子进程组成的进程。
LOTOS的基本描述对象是并发进程，进程的行为用它与外部环境之间的交互动作序列来描述。
LOTOS主要基于R.Miler的通信系统演算CCS，另外用一种抽象数据结构的代数表示法ACTONE来描述系统的数据部分。
LOTOS两个组成部分：
基于进程代数CCS：
有所扩展，描述进程的行为和相互作用，用行为算子组成行为表达式，描述多个协议事件和行为。
基于抽象数据类型ACTONE，描述数据结构和值表达式，描述基于分布，并发，消息驱动的系统，描述的协议容易转换成CCS模型，时态逻辑模型，FSM模型，Petri模型。
5.5LOTOS将一个系统看做多个相互作用的子进程组成的进程，每个子进程又是由多个子进程构成。
由此可见，LOTOS描述一个系统的方法是一种由高层向低层逐级定义进程的方法。
5.6形式描述语言的比较
由于不同的模型具有不同的语义基础，适用于不同的对象，在实际中，我们应根据目的的不同，选择不同的模型。
Estelle是pascal语言的扩充，用Estelle描述的协议容易转换成pascal或c代码。
因此，它是一种面向协议实现的FDL。
若以实现为目标，则应选择Estelle进行描述，通过使用过程语言pascal，可较详细地描述协议细节。
用Estelle描述的协议易于提取FSM模型和Petri模型，对并发、不确定性、超时、异步通讯状态转换有较强的表达能力，但对递归、共享通道、同步通讯、协议性质的表示缺少有力的手段，不容易提取转变成TL和CSS模型，并且由于在描述阶段涉及过多的协议细节，这样势必给形式描述的抽象程度带来影响。
LOTOS能提供较好抽象程度的形式描述，侧重于通过定义系统外部可见行为中事件的次序关系来描述系统，而不关心协议实体的内部变化，可区别内部事件和外部事件，较有利于判断死锁，可描述非确定性系统，同时包含一套严谨的数学公理化系统，因而使得该语言具有较高的抽象程度，有利于对协议的各种性质进行分析验证。
若以验证为目标，则可以选择LOTOS来描述。
其弱点在于缺乏状态概念，不易直接通过编译器自动生成实现代码，往往需要形式描述风格变换。
SDL是一种基于扩展状态变换图和抽象数据类型的混合技术，主要用于描述电信系统和开发控制软件，已被电信公司广泛用于描述电子分组交换系统。
但也可以用它来描述协议，比较适用于描述用扩展有限状态机进行模拟的系统，尤其是交互式实时系统。
其不足表现在：
语义需重新定义，缺乏分析技术，实现不具有独立性。
Chapter6ProtocolVerificationandTesting——ConceptsandApproaches
Coursecontent：
6.1Verification
验证是对协议本身的逻辑正确性进行校验的过程。
协议验证有两种途径：
协议分析：
对已设计的协议进行分析和校验（非形式化设计方法产生的协议），通常说协议验证指协议分析；
协议综合：
将协议设计过程和验证过程融合在一起，通过一组规则确保所设计的协议是正确，从一些基本协议模块（正确的）产生所希望的目标协议。
由协议需求描述产生一个目标协议，即：
力图使用一组能确保所产生的协议是正确的规则，由“协议零部件”装配出一个符合要求的目标协议。
6.1.1ProtocolAnalysis
协议分析包括：
可达性分析（Reachability）、等价性分析（Equivalence）、不变性分析（Invariance）、符号执行（SymbolExecution）、模拟（Simulation）。
协议分析的关键是形成确定算法，从而可以借助于分析工具在计算机上自动或半自动进行。
协议分析可在任何表达形式上进行：
自然语言描述的协议的非形式化文本；基于形式化描述语言的协议规范：
如Estelle、LOTOS、SDL等；基于模型技术表达的协议模型：
如FSM、PetriNet、CCS等；基于程序设计语言描述的协议代码：
如C、Pascal等。
6.1.2可达性分析
基于FSM，试图产生和检查协议所有或部分可达状态；
可达状态：
协议（机）从初始状态开始经历有限次转换之后可到达的状态；所有可达状态构成可达树（ReachabilityGraph）
可达性分析：
主要是产生和检查可达图，判定是否存在死锁、活锁等协议错误。
可达性分析主要技术和目的：
怎样找出所有可达状态，构成可达图；怎样检测死锁、活锁等协议错误；怎样解决状态爆炸问题。
6.1.3不变性分析
系统不变性：
一个系统的某个性质能用一个确定的逻辑表达式描述，而且恒为真（不随系统的状态变化或执行序列而改变）
协议的不变性分析：
正确地找出协议（系统）的不变性质，形成严格定义的不变性表达式，以某种方式执行协议，验证不变性表达式是否恒为真。
不变性分析途径：
不变性证明系统（如：
采用归纳法）、不变性监测系统。
6.1.4等价性分析
等价：
某种程度上的“相同”和“无差别”；
两个协议模型或协议规范是等价的，它们可以互换。
如果一个正确，则另一个也是正确的。
协议等价性分析：
利用“等价”方法简化FSM图等；证明两个协议的FSM图或CCS表达式是等价的；证明协议规范和协议的服务规范是一致的。
等价性划分：
按照等价的含义和等价的强弱程度排列划分：
观察等价：
状态到状态变化观察到的协议行为没有差别；
测试等价：
相同测试序列所观察到的行为没有差别；
跟踪等价：
执行的事件序列相同；
实现等价：
一个协议的做的事情能被另一个模仿，反之亦然。
6.2Testing
测试是试图通过实验的方法找出错误的过程。
在测试过程中既要模拟被测试方正常工作的情况，也要模拟异常使用的情况；既要模拟被测试方单独运行的情况，也要模拟若干个被测试方互相通信的情况。
由于无法对一个系统进行无穷尽的测试，所以测试并不能保证被测试方的完全正确性。
协议测试的基本出发点——只能证明“存在错误”，而不能证明“不存在错误”
6.2.1ProtocolTesting
协议测试理论是协议工程学的一个重要分支。
研究协议测试理论的原因在于一个标准化的协议并不能确保该
升级会员 