《网络协议工程》课程教案Word文档格式.docx
- 文档编号:6505790
- 上传时间:2023-05-06
- 格式:DOCX
- 页数:15
- 大小:163.39KB
《网络协议工程》课程教案Word文档格式.docx
《《网络协议工程》课程教案Word文档格式.docx》由会员分享,可在线阅读,更多相关《《网络协议工程》课程教案Word文档格式.docx(15页珍藏版)》请在冰点文库上搜索。
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
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
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
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
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
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
协议测试理论是协议工程学的一个重要分支。
研究协议测试理论的原因在于一个标准化的协议并不能确保该
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 网络协议工程 网络 协议 工程 课程 教案