【正文】 南京郵電大學(xué) 第 3 章 協(xié)議形式化描述技術(shù) （ 1概述及 FSM） 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 2 內(nèi)容提要 概述 1 FSM 2 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 3 形式化描述技術(shù)： Why? ?通信系統(tǒng)行為的復(fù)雜性增大了行為描述的難度，人們必須借助一種語言或一種技術(shù)來準(zhǔn)確地描述系統(tǒng)行為。 ?在過去，人們習(xí)慣使用自然語言進(jìn)行協(xié)議描述（用自然語言寫協(xié)議的規(guī)格說明或規(guī)范） ?優(yōu)點(diǎn)是：方便、易懂 ?致命缺點(diǎn)是：不嚴(yán)格、不精確、結(jié)構(gòu)不好、沒有描述標(biāo)準(zhǔn)和有二義性 ?且很難進(jìn)行協(xié)議實(shí)現(xiàn)、測試的自動(dòng)化和協(xié)議驗(yàn)證。 ?不同的人對(duì)協(xié)議描述的理解不一樣導(dǎo)致不同的協(xié)議實(shí)現(xiàn)之間不能實(shí)現(xiàn)互連，甚至還會(huì)得出錯(cuò)誤的協(xié)議。 ?解決辦法：形式化技術(shù) FDTs (Formal Description Techniques) 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 4 FDTs： Aims ?采用形式描述技術(shù)的目的是： ?為開發(fā)者提供一種分析的方法； ?作為對(duì)開發(fā)結(jié)果驗(yàn)證的基礎(chǔ)； ?為設(shè)計(jì)人員和應(yīng)用人員提供交流途徑； ?作為開發(fā)文檔能在將來再開發(fā)時(shí)使用。 ?理想的形式描述技術(shù)應(yīng)該既能描述系統(tǒng)的行為特征，又能進(jìn)行操作： ?在系統(tǒng)需求分析和設(shè)計(jì)階段，它應(yīng)該是一種描述語言 ?在系統(tǒng)實(shí)現(xiàn)階段它應(yīng)該是一種編程語言。 ?形式描述技術(shù)是將協(xié)議工程各階段在技術(shù)上銜接起來的紐帶，因此它對(duì)協(xié)議工程的發(fā)展起決定性作用。 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 5 FDTs：特性 ?用于協(xié)議的 FDT一般應(yīng)具有如下重要特性： ?完整的語法和語義定義 ?體系結(jié)構(gòu)、服務(wù)和協(xié)議的可表達(dá)性 ?協(xié)議重要特性 (如，無死鎖 )的可分析性 ?支持復(fù)雜協(xié)議的管理 (如，構(gòu)造能力 ) ?支持逐步求精的方法 ?支持實(shí)現(xiàn)獨(dú)立性 (包括并發(fā)性、非確定性和適當(dāng)?shù)某橄髾C(jī)制 ) ?支持協(xié)議生命期的各環(huán)節(jié)，包括驗(yàn)證、實(shí)現(xiàn)和測試 ?支持自動(dòng)或半自動(dòng)設(shè)計(jì)、驗(yàn)證、實(shí)現(xiàn)和維護(hù)方法 ?應(yīng)能準(zhǔn)確地描述進(jìn)程交互的各種原語 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 6 FDTs: Classification ?形式描述模型 (FDM) ?狀態(tài)變遷模型 ?有限狀態(tài)機(jī) FSM(Finite State Machine) ?擴(kuò)展的有限狀態(tài)機(jī) EFSM(Extended FSM)模型 ?通信有限狀態(tài)機(jī) CFSM(Communicating FSM)模型 ? Carl Adam Petri的 Petri網(wǎng) (PetriNet) ?時(shí)態(tài)邏輯 TL(Temporal Logic) ?進(jìn)程代數(shù) (Algebra of Process) ? ： 通信系統(tǒng)演算 CCS (Calculus of Communication System)（進(jìn)程代數(shù)據(jù)的基礎(chǔ)） ? Hoare： 通信順序進(jìn)程 CSP (Communicating Sequential Processes)（以 CCS為基礎(chǔ)） 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 7 FDTs: Classification (Cont.) ?形式描述語言 (FDL) ?ISO制定的 Estelle和 LOTOS ?CCITT制定的 SDL ?ISO的 (抽象語法記法 ) ?對(duì)象管理組織 OMG制定的統(tǒng)一建模語言 UML ?ISO的 抽象測試集描述語言的 TTCN ?高級(jí)程序設(shè)計(jì)語言，如 Pascal, C, PL/1 ?便于協(xié)議的實(shí)現(xiàn) ?大多數(shù)比較復(fù)雜、分析起來比較困難，且不支持非確定性的描述。 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 8 模型 vs. 語言 ?模型 ?含義一：對(duì)象或系統(tǒng)的抽象 ? OSI/RM：網(wǎng)絡(luò)系統(tǒng)的抽象模型 ?含義二：描述對(duì)象或系統(tǒng)的方法或技術(shù) ? FSM ? PetriNet 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 9 Functions vs. Computation ?Functions specify only a relation between two sets of variables (input and output) ?Computations describe how the output Variables can be derived from the value of the input variables. 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 10 Model of Computation ?A MoC is a framework in which to express what sequence of actions must be taken to plete a putation ?An instance of a model of putation is a representation of a function under a particular interpretation of its constituents ?Not necessarily a bijection (in fact almost never!) ?Examples: Finite State Machine, Turing Machine, differential equation 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 11 模型 vs. 語言（續(xù)） ?形式語言 ?具有嚴(yán)格的語法和語義 ?可以精確、完全地表述協(xié)議的功能、性能及行為等 ?以一種或多種數(shù)學(xué)方法或形式模型為基礎(chǔ) ? SDL： 基于擴(kuò)展的 FSM和抽象數(shù)據(jù)類型 ? Eetelle：基于擴(kuò)展的 FSM，是 Pascal語言的擴(kuò)充 ? LOTOS：基于通信系統(tǒng)演算（ CCS）和抽象數(shù)據(jù)類型語言 ACT ONE 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 12 模型 vs. 語言（續(xù)） ?模型與語言的差別不是很明顯。不同文獻(xiàn)有不同的說法。 ?將模型與語言分開 ?一些文獻(xiàn)中的模型在另一些文獻(xiàn)中成為語言或相反 ?將模型與語言不分，統(tǒng)稱為形式化描述技術(shù) ?事實(shí)上，模型也可以看成是一種形式語言 ?文法：描述語言的語法結(jié)構(gòu)的形式規(guī)則（即語法規(guī)則） ?Turing 機(jī) (無限自動(dòng)機(jī) )的能力相當(dāng)于 0型文法 ?有限自動(dòng)機(jī)相當(dāng)于正規(guī)文法（ 3型文法） ?模型是語言的一個(gè)實(shí)例 (Instance)（語義），例如 C語言編譯器是 C語言的模型 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 13 Models Of Computation and languages ?Need to distinguish between model and language ?Language needs to ? be expressive enough for application domain (write things once…) ?have semantics in desired MOC ?MOC needs to ? be powerful enough for application domain ?have appropriate synthesis and validation algorithms 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 14 FDTs: 小結(jié) ?實(shí)際應(yīng)用時(shí)，往往是將多種形式描述技術(shù)混合起來使用。 ?例如：將協(xié)議中的主要狀態(tài)用變遷用圖形表示 (有限狀態(tài)機(jī)或 Petri網(wǎng) )，而協(xié)議的其他細(xì)節(jié)則用高級(jí)語言描述。這樣使得協(xié)議的描述和驗(yàn)證都比較方便。 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 15 內(nèi)容提要 概述 1 FSM 2 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 16 Finite State Machines (FSMs) 一、概 述 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 17 Finite State Machines (FSMs) input events outputs current state next state state transition function ?Finite state machines consist of: ?Output Events ?Input Events (or Signals, or Messages) ?Transition Functions STATE ?States NEXT STATE CURRENT STATE INPUT EVENTS OUTPUTS Transition Function 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 18 Finite State Machine States input events outputs current state next state state transition function ? Current State ? State which determines the current behavior of the machine ? Next State ? State which will machine have after processing an input event. Next State can be same as current ? Start State ? State in which machine will be when created 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 19 FSM Transitions input events outputs current state next state state transition function ? Triggered by input events the FSM moves from one state to other based on the Transition Function ? Transition Function produces the Output and Next State depending on Current State and Input Event ? While in particular state FSM is not active. It is waiting for an input to perform next activity 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 20 Finite State Machines (FSMs) 二、形式化定義 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 21 FSM: Formal Definition ?FSM is 5tuple: FSM = (S, s0, I, ?, F), where ?S = {s0, s1, …, s n}: 有限狀態(tài)集合。在任一確定時(shí)刻，F(xiàn)SM只能處于一個(gè)確定的狀態(tài) si。 ?I = {a0, a1, …, a m}: 有限輸入字符集合。在任一確定的時(shí)刻， FSM只能接收一個(gè)確定的輸入 aj。 ?? ： S ? I ? S是狀態(tài)轉(zhuǎn)換函數(shù)，如果在某一確定的時(shí)刻，F(xiàn)SM處于某一狀態(tài) si ? S, 并接收一個(gè)輸入字符 aj? I，那么下一時(shí)刻將處于一個(gè)確定的狀態(tài) s180。 = ?(si , aj) ? S。在這里規(guī)定， s = ?(s , ?)， 即對(duì)任何狀態(tài) s，當(dāng)讀入空字符 ?時(shí)，有很狀態(tài)機(jī)不發(fā)生任何狀態(tài)轉(zhuǎn)移。 ?s0 ? S是初始狀態(tài)， FSM由此狀態(tài)開始接收輸入 ?F ? S是一個(gè)終態(tài)集（可空）， FSM到達(dá)終態(tài)后不再接收輸入 ?確定有限狀態(tài)機(jī)也稱為 DFA（確定有限自動(dòng)機(jī)） 第 3章 協(xié)議形式化描述技術(shù) (1－概述及 FSM) 22 Non determinis