1、四、協(xié)議的形式描述語(yǔ)言1Slide 1主要內(nèi)容形式化方法協(xié)議的形式化模型協(xié)議的形式描述語(yǔ)言SDL2Slide 21、形式化方法3Slide 3形式化方法的引入系統(tǒng)行為的復(fù)雜性增大了行為描述的難度，必須借助一種語(yǔ)言或一種技術(shù)來(lái)準(zhǔn)確的描述系統(tǒng)的行為。自然語(yǔ)言具有冗長(zhǎng)、不完整、語(yǔ)句容易產(chǎn)生二義性、結(jié)構(gòu)性差和沒(méi)有描述標(biāo)準(zhǔn)等缺點(diǎn)。國(guó)際標(biāo)準(zhǔn)化組織建議用形式化方法來(lái)描述復(fù)雜的系統(tǒng)。形式化方法使得對(duì)通信系統(tǒng)的描述、實(shí)現(xiàn)和測(cè)試變得容易。4Slide 4與自然語(yǔ)言相比，形式化方法具有以下的特點(diǎn)：形式化的語(yǔ)法形式化的語(yǔ)義清楚的概念模型界面統(tǒng)一表示強(qiáng)大的表達(dá)和描述功能有助于系統(tǒng)的實(shí)現(xiàn)和完善形式化方法的特點(diǎn)5Slide

2、 5形式化方法的最終目的為開(kāi)發(fā)者提供一種分析、設(shè)計(jì)的方法作為對(duì)開(kāi)發(fā)結(jié)果進(jìn)行驗(yàn)證、測(cè)試的基礎(chǔ)為設(shè)計(jì)和應(yīng)用人員提供交流的途徑作為開(kāi)發(fā)文檔易于今后的維護(hù)和再開(kāi)發(fā)6Slide 62、協(xié)議的形式化模型7Slide 7協(xié)議的形式化模型有限狀態(tài)機(jī)（FSM）Petri網(wǎng)時(shí)態(tài)邏輯TL通信進(jìn)程演算8Slide 8有限狀態(tài)自動(dòng)機(jī)可定義為一個(gè)四元系統(tǒng) ，其中：S：系統(tǒng)狀態(tài)集，狀態(tài)數(shù)有限；i：系統(tǒng)初始狀態(tài)，i S;E：輸入字母集；T：轉(zhuǎn)移函數(shù)集，是從 SE到S的映射；有限狀態(tài)自動(dòng)機(jī)（1）9有限狀態(tài)自動(dòng)機(jī)（2）單比特奇偶檢驗(yàn)器的有限狀態(tài)自動(dòng)機(jī)偶奇11Slide 90010Slide 10擴(kuò)展有限狀態(tài)自動(dòng)機(jī)（1）擴(kuò)展有限狀

3、態(tài)自動(dòng)機(jī)定義為一個(gè)四元系統(tǒng) ，其中：S：系統(tǒng)狀態(tài)集，狀態(tài)數(shù)有限；i： 系統(tǒng)初始狀態(tài)， i S;E：輸入事件集；T：轉(zhuǎn)移函數(shù)，是從SE到S的映射11擴(kuò)展有限狀態(tài)自動(dòng)機(jī)（2）轉(zhuǎn)換函數(shù)的定義：SiSj T， Si，SjSt = e / p：a；或t = e / a；或t = e其中：eE，p為謂詞，表示條件；a表示動(dòng)作Slide 11t12等AK擴(kuò)展有限狀態(tài)自動(dòng)機(jī)（3）等待DC等CCDC未連接AKTDTreq/DTCC/TCONconfTDISreq/DR已連接TCONreq/CR傳輸層協(xié)議機(jī)Slide 1213Slide 13可通信的擴(kuò)展有限狀態(tài)自動(dòng)機(jī)系統(tǒng)的行為通過(guò)可通信的擴(kuò)展有限自動(dòng)機(jī)來(lái)描述系統(tǒng)

4、由擴(kuò)展的有限狀態(tài)自動(dòng)機(jī)組成擴(kuò)展的有限狀態(tài)自動(dòng)機(jī)具有與外界通信的能力：輸入/輸出動(dòng)作14Slide 14Petri網(wǎng)Petri網(wǎng)的概念最早是由德國(guó)的Carl Adam Petri于1962年提出的。它是一種適合于并發(fā)、異步、分布式系統(tǒng)描述與分析的圖形數(shù)學(xué)工具。Petri網(wǎng)已成為網(wǎng)絡(luò)協(xié)議分析和設(shè)計(jì)的典型形式化模型之一。15Slide 15時(shí)態(tài)邏輯（TL）它涉及含有時(shí)間信息（現(xiàn)在、過(guò)去、將來(lái)、之前、之后等）的事件、狀態(tài)及其關(guān)系的命題、謂詞和演算。16P1=a.(c.NIL+b.NIL)P1=Q2 I Q3（選擇）（并行）通信進(jìn)程演算（CCS）是計(jì)算機(jī)通信系統(tǒng)的基本理論模型，也是許多形式化語(yǔ)言的基礎(chǔ)。

5、CCS的基本成分是事件和進(jìn)程，而進(jìn)程是通過(guò)順序、選擇和并行三個(gè)基本算子來(lái)定義的。P1=a.b.NIL P2=a.b.P2 （順序）17Slide 173、協(xié)議的形式描述語(yǔ)言18Slide 18ESTELLE為準(zhǔn)確描述OSI協(xié)議，ISO的FDT（形式描述技術(shù)）小組于20世紀(jì)80年代初開(kāi)始進(jìn)行形式描述語(yǔ)言的開(kāi)發(fā)研究。最初提出了20多種方法，大致可歸結(jié)為2類：基于有限狀態(tài)機(jī)語(yǔ)言類和基于代數(shù)方法語(yǔ)言類。ESTELLE（一種擴(kuò)充的有限狀態(tài)機(jī)語(yǔ)言）是前一類語(yǔ)言的典型代表。1989年，ISO公布了作為形式描述技術(shù)國(guó)際標(biāo)準(zhǔn)之一的ESTELLE。ESTELLE是基于擴(kuò)展的有限狀態(tài)機(jī)，是一種形式化、數(shù)學(xué)化，并且與

6、具體實(shí)現(xiàn)相獨(dú)立的描述技術(shù)。它具有良好的結(jié)構(gòu)和定義，并且具有很強(qiáng)的表達(dá)能力，可以完整、一致、簡(jiǎn)練、準(zhǔn)確的描述分布、并行信息處理系統(tǒng)。ESTELLE的特點(diǎn)：基于擴(kuò)展有限狀態(tài)機(jī)，專為描述協(xié)議而設(shè)計(jì)；是Pascal語(yǔ)言的擴(kuò)充，是面向協(xié)議實(shí)現(xiàn)的FDL；模塊之間的通信方式為異步通信；對(duì)并發(fā)、不確定性、超時(shí)、異步通信狀態(tài)轉(zhuǎn)換有較強(qiáng)的表達(dá)能力，但對(duì)遞歸、共享通道、同步通信的表示不足；其所描述的協(xié)議很容易轉(zhuǎn)換為FSM、Petri網(wǎng)模型，不容易轉(zhuǎn)換成TL、 CCS模型。19Slide 19ISO的FDT（形式描述技術(shù)）小組經(jīng)過(guò)8年多時(shí)間的努力，于1988年8月完成了作為國(guó)際標(biāo)準(zhǔn)的形式描述語(yǔ)言（LOTUS,Lang

7、uage of Temporal Ordering Specification）。LOTOS的基本思想是：外部可觀察到的系統(tǒng)行為由一系列的交互作用組成，通過(guò)對(duì)這些交互作用的時(shí)間關(guān)系進(jìn)行定義，從而描述整個(gè)系統(tǒng)。LOTOS的特點(diǎn)：基于進(jìn)程代數(shù)CCS和多類代數(shù)的FDL；進(jìn)程通信為同步通信；不是面向協(xié)議實(shí)現(xiàn)的語(yǔ)言；其所描述的協(xié)議很容易轉(zhuǎn)換為CCS模型，也比較容易轉(zhuǎn)換成TL、FSM、Petri網(wǎng)模型。LOTOS的不足之處：無(wú)異步通信機(jī)制、無(wú)清晰的記錄型數(shù)據(jù)結(jié)構(gòu)的描述手段、無(wú)常量描述手段、可讀性差。LOTOS20Slide 20SDLSDL（Specification and Description La

8、nguage）是ITU-T提出的一種形式化描述語(yǔ)言，由Z.100建議定義。SDL的版本： SDL-88：是后續(xù)版本的基礎(chǔ) SDL-92：引入面向?qū)ο蟮母拍?SDL-96：對(duì)SDL-92的完善 SDL-2000：對(duì)面向?qū)ο蟮奶卣髯髁诉M(jìn)一步的擴(kuò)展；引入了其它語(yǔ)言，如ASN.1、ITU-T ODL、UML等21Slide 21SDL的特點(diǎn)可用于需求分析到具體實(shí)現(xiàn)的整個(gè)開(kāi)發(fā)過(guò)程。適應(yīng)于實(shí)時(shí)系統(tǒng)基于擴(kuò)展的有限狀態(tài)機(jī)圖形化表示方式，可視性強(qiáng)具有面向?qū)ο蟮奶卣?2Slide 224、SDL23Slide 23內(nèi)容SDL語(yǔ)言概述SDL基本概念SDL中的數(shù)據(jù)24Slide 244-1、SDL語(yǔ)言概述25Slid

9、e 25SDL的應(yīng)用（1）SDL主要應(yīng)用于電信領(lǐng)域，適用于描述活性離散系統(tǒng)。活性：是指系統(tǒng)對(duì)外來(lái)的信號(hào)（輸入）是有反應(yīng)（輸出）的離散：是指系統(tǒng)與環(huán)境的信息交互不是連續(xù)的26Slide 26SDL的應(yīng)用（2）既可以用來(lái)說(shuō)明（specification ）一個(gè)系統(tǒng)應(yīng)具有的行為（behaviour）；又可以用來(lái)描述（description ）一個(gè)系統(tǒng)實(shí)際具有的行為（behaviour）。SDL可用來(lái)制作以下文檔：需求說(shuō)明ITU-T建議系統(tǒng)設(shè)計(jì)說(shuō)明系統(tǒng)設(shè)計(jì)描述系統(tǒng)測(cè)試說(shuō)明27SDL的系統(tǒng)和環(huán)境系統(tǒng)環(huán)境交互信號(hào)SDL系統(tǒng)環(huán)境信號(hào)28SDL系統(tǒng)層次關(guān)系系統(tǒng)功能塊功能塊進(jìn)程功能塊進(jìn)程進(jìn)程功能塊進(jìn)程29Sli

10、de 29SDL系統(tǒng)包含關(guān)系SDL系統(tǒng)功能塊圖進(jìn)程圖30Slide 30SDL中的主要術(shù)語(yǔ)代理（agent）系統(tǒng)（system）功能塊（block）進(jìn)程（process）信號(hào)（signal）信道（channel）狀態(tài)（state）實(shí)例（instance）過(guò)程（procedure）數(shù)據(jù)類型（sort）進(jìn)程標(biāo)識(shí)（pid）31Slide 31SDL文法概述graphical grammarabstract grammarcommon textual grammarSDL/GRSDL/PRtextualgrammar32Slide 324-2、SDL基本概念33Slide 33系統(tǒng)（1）SDL系統(tǒng)：完

11、整地描述一個(gè)真實(shí)系統(tǒng)或一個(gè)真實(shí)系統(tǒng)中相對(duì)獨(dú)立的一部分。一個(gè)系統(tǒng)可以劃分為若干個(gè)功能塊；功能塊之間以及功能塊與環(huán)境之間用信道相連。系統(tǒng)各功能塊之間以及功能塊與環(huán)境之間可以使用信號(hào)通信；信號(hào)通過(guò)信道來(lái)傳遞。系統(tǒng)的文本域：用來(lái)定義信號(hào)、信號(hào)列表、數(shù)據(jù)類型、變量等，這些定義包含在文本符內(nèi)。系統(tǒng)的交互域：描述系統(tǒng)圖中功能塊的劃分情況以及信道的設(shè)置情況。34Slide 34系統(tǒng)（2）35Slide 35功能塊（1）功能塊包括一個(gè)或多個(gè)并發(fā)的功能塊或進(jìn)程；功能塊文本域定義本功能塊內(nèi)部信號(hào)、信號(hào)列表、數(shù)據(jù)類型等內(nèi)容；功能塊的交互域描述本功能塊中功能塊或進(jìn)程的組成及交互關(guān)系；在功能塊圖的邊界上，要標(biāo)出與本功能塊

12、相連的信道標(biāo)識(shí)。36Slide 36功能塊（2）37Slide 37功能塊（3）38Slide 38進(jìn)程（1）進(jìn)程是系統(tǒng)的基本組成單位，系統(tǒng)的行為主要由進(jìn)程來(lái)描述；進(jìn)程圖中每個(gè)進(jìn)程實(shí)例都有一塊私有存儲(chǔ)空間，記錄進(jìn)程圖中定義的變量的數(shù)值及實(shí)例所處的狀態(tài)。39Slide 39進(jìn)程（2）進(jìn)程實(shí)例一旦被創(chuàng)建，就擁有了一個(gè)自己的pid，通過(guò)以下四種pid表達(dá)式可以得到進(jìn)程實(shí)例的pid：self返回本進(jìn)程實(shí)例的pid；sender返回發(fā)送最近被消耗信號(hào)的進(jìn)程實(shí)例的pid；parent返回創(chuàng)建本進(jìn)程實(shí)例的進(jìn)程實(shí)例（父進(jìn)程）的id；offspring返回最近被本進(jìn)程創(chuàng)建的進(jìn)程實(shí)例（子進(jìn)程）的 pid。40Sl

13、ide 40進(jìn)程（3）進(jìn)程中可以定義過(guò)程，過(guò)程圖可被包含在進(jìn)程圖中，也可單獨(dú)定義。在進(jìn)程圖中用過(guò)程符來(lái)說(shuō)明定義關(guān)系。如果在進(jìn)程圖中包含了過(guò)程符，則在SDL描述中必然有具有相同過(guò)程名的過(guò)程圖存在。過(guò)程只能由包含該過(guò)程的進(jìn)程的實(shí)例來(lái)調(diào)用，如果該進(jìn)程以外的代理實(shí)例要調(diào)用該過(guò)程，就必須把該過(guò)程聲明為遠(yuǎn)端過(guò)程（remote procedure）。41proc1狀態(tài)機(jī)圖進(jìn)程（4）use process 定義變量等42Slide 42過(guò)程（1）過(guò)程是進(jìn)程的一部分過(guò)程不存在過(guò)程實(shí)例，它可由包含該過(guò)程的進(jìn)程集的所有實(shí)例來(lái)調(diào)用過(guò)程用過(guò)程圖來(lái)定義過(guò)程中還可以定義過(guò)程過(guò)程可以帶參數(shù)，參數(shù)類型有三種：in/out，in

14、，out；過(guò)程還可以定義成返回型過(guò)程，返回值類型定義跟在形參定義后面過(guò)程可以有狀態(tài)，但過(guò)程沒(méi)有獨(dú)立的輸入隊(duì)列43Slide 43過(guò)程（2）procedure Proc1in/out x integer, in y integer- rslt char定義變量、定時(shí)器等過(guò)程圖形域use 44Slide 44過(guò)程（3）過(guò)程圖形域是過(guò)程的主體內(nèi)容，與狀態(tài)機(jī)圖形域基本相同，但有以下不同：起始符不同，過(guò)程起始符定義為：狀態(tài)機(jī)圖可以沒(méi)有終止符，而過(guò)程圖必須有至少一個(gè)返回符，返回符定義為：帶表達(dá)式的返回符僅用于要求返回值的過(guò)程，表達(dá)式的值即為本次過(guò)程調(diào)用的返回值45Slide 45通信SDL系統(tǒng)的通信手段包

15、括系統(tǒng)與環(huán)境之間或系統(tǒng)中的各代理之間交互信號(hào)遠(yuǎn)程過(guò)程調(diào)用使用遠(yuǎn)端變量46Slide 46信道（1）信道是用在代理與代理之間或代理與系統(tǒng)環(huán)境或信關(guān)之間傳遞信號(hào)的通道。信道分為單向和雙向兩種，在每個(gè)方向上需列出在該方向上傳遞的所有信號(hào)，這些信號(hào)用方括號(hào)（ ）括起來(lái)，標(biāo)在信道的箭頭處。信道分為：延遲信道：表示信號(hào)從源端到目的端要經(jīng)過(guò)一定延遲，延遲時(shí)間是不確定的，但信道上的信號(hào)仍是有序的非延遲信道：表示信號(hào)從源端發(fā)出后直接到達(dá)目的地，沒(méi)有延遲47Slide 47信道（2）延遲信道（單向）延遲信道（雙向）非延遲信道（單向）非延遲信道（雙向）48Slide 48信號(hào)（1）信號(hào)是SDL系統(tǒng)中代理之間通信的基

16、本單位信號(hào)必須在信道中傳輸要利用信號(hào)來(lái)通信，必須：信號(hào)定義：在相關(guān)代理圖的文本域中定義信號(hào)；信號(hào)與信道關(guān)聯(lián)：在信道的信號(hào)列表域中列出信號(hào)，說(shuō)明信號(hào)可以在哪些信道中傳遞信號(hào)可以定義參數(shù)，定義過(guò)的信號(hào)可以用來(lái)定義信號(hào)列表。信號(hào)列表的定義也在文本符中定義。在信道上列出信號(hào)和/或信號(hào)列表時(shí)，信號(hào)列表標(biāo)識(shí)符要用圓括號(hào)括起來(lái)，以區(qū)別于信號(hào)49Slide 49信號(hào)（2）定義舉例signal call_hkof,call_hkon,dial_number(integer);signal called_hkof,called_hkon;Signal timeout(char,integer);signallis

17、t call_input=call_hkof,call_hkon,dial_number,timeout;signallist called_input=called_hkof,called_hkon,timeout;50Slide 50信號(hào)（3）51Slide 51狀態(tài)機(jī)開(kāi)始域（1）每個(gè)狀態(tài)機(jī)有且僅有一個(gè)開(kāi)始域開(kāi)始域由開(kāi)始符下接遷移過(guò)程組成開(kāi)始符遷移過(guò)程：遷移過(guò)程由一系列動(dòng)作組成，如輸出信號(hào)、變量賦值、調(diào)用過(guò)程、創(chuàng)建實(shí)例等。52Slide 52狀態(tài)機(jī)開(kāi)始域（2）開(kāi)始域的一般情況最簡(jiǎn)單的開(kāi)始域是從開(kāi)始符直接進(jìn)入狀態(tài)in i_ s ta te53Slide 53狀態(tài)機(jī)狀態(tài)（1）一個(gè)狀態(tài)機(jī)包含若干

18、種狀態(tài)狀態(tài)符狀態(tài)符下面可以連接的圖形節(jié)點(diǎn)輸入符優(yōu)先輸入符連續(xù)信號(hào)符保存符54Slide 54狀態(tài)機(jī)狀態(tài)（2）狀態(tài)符與其它圖形符號(hào)的連接關(guān)系圖s155Slide 55狀態(tài)機(jī)狀態(tài)（3）狀態(tài)列表的四種情況單個(gè)狀態(tài)名s1msg56Slide 56狀態(tài)機(jī)狀態(tài)（4）多個(gè)狀態(tài)名：表示在這幾個(gè)狀態(tài)下，同一事件引起的過(guò)程遷移是相同的s1，s2msg57Slide 57狀態(tài)機(jī)狀態(tài)（5）*：表示某一事件在本狀態(tài)機(jī)所有狀態(tài)下引起的遷移過(guò)程是相同的*msg58Slide 58狀態(tài)機(jī)狀態(tài)（6）*（狀態(tài)列表1）：表示某一事件在本狀態(tài)機(jī)除狀態(tài)列表1中列出的狀態(tài)以外的所有狀態(tài)下引起的遷移過(guò)程是相同的*(s1，s2)msg59狀

19、態(tài)機(jī)狀態(tài)（7）下一狀態(tài)：狀態(tài)機(jī)經(jīng)過(guò)遷移過(guò)程后進(jìn)入下一狀態(tài)s1s2s1-s1s160Slide 60狀態(tài)機(jī)觸發(fā)事件（1）觸發(fā)事件是激發(fā)狀態(tài)機(jī)從當(dāng)前狀態(tài)遷移到下一狀態(tài)的事件。觸發(fā)事件包括：輸入、優(yōu)先輸入、連續(xù)信號(hào)狀態(tài)機(jī)消耗一條信號(hào)后，用sender函數(shù)可得到發(fā)送該信號(hào)的代理實(shí)例的pid；但如果該信號(hào)來(lái)自環(huán)境，則sender函數(shù)返回的值將不同于系統(tǒng)內(nèi)的任何一個(gè)pid值。61Slide 61觸發(fā)事件輸入（1）輸入表示狀態(tài)機(jī)接收并消耗信號(hào)一個(gè)狀態(tài)機(jī)對(duì)應(yīng)一個(gè)輸入隊(duì)列狀態(tài)機(jī)輸入隊(duì)列按先進(jìn)先出的原則排序輸入用輸入符表示輸入符內(nèi)可以包含多條信號(hào)，表示在本狀態(tài)下，輸入這幾條信號(hào)引起的遷移過(guò)程是一樣的62觸發(fā)事件輸

20、入（2）msgmsg1，msg2T63觸發(fā)事件輸入（3）多信號(hào)輸入引起同一遷移過(guò)程msg2msg1*64觸發(fā)事件輸入（4）信號(hào)可以帶參數(shù)，對(duì)于帶參數(shù)的信號(hào)輸入，在輸入符中，除給出信號(hào)標(biāo)識(shí)外，還需給出具有相應(yīng)數(shù)據(jù)類型的變量名來(lái)接收參數(shù)值msg(x,y,z)msg(,z)msg(x)65Slide 65觸發(fā)事件輸入（5）帶使能條件的輸入msg1xmax66觸發(fā)事件輸入（6）自發(fā)輸入noneoddnoneeven67Slide 67觸發(fā)事件優(yōu)先輸入（1）優(yōu)先輸入可以使信號(hào)在某狀態(tài)下一旦輸入就立即處理優(yōu)先輸入用優(yōu)先輸入符表示優(yōu)先輸入符優(yōu)先輸入符下不接使能條件符68觸發(fā)事件優(yōu)先輸入（2）S1sig1si

21、g269Slide 69觸發(fā)事件連續(xù)信號(hào)（1）通過(guò)計(jì)算布爾表達(dá)式的值來(lái)觸發(fā)狀態(tài)機(jī)ymax70觸發(fā)事件連續(xù)信號(hào)（2）帶優(yōu)先級(jí)的連續(xù)信號(hào)：當(dāng)多個(gè)連續(xù)信號(hào)的布爾表達(dá)式計(jì)算結(jié)果為“真”時(shí)，取優(yōu)先級(jí)最高者作為觸發(fā)信號(hào)x3;priority 1y8; priority 271Slide 71狀態(tài)機(jī)保存（1）保存可以將提前到達(dá)輸入隊(duì)列的有效信號(hào)保存下來(lái)保存用保存符來(lái)表示被保存下來(lái)的信號(hào)在下一狀態(tài)中將優(yōu)先得到處理，但前提是下一狀態(tài)的輸入符中包含了該信號(hào)如果在新的狀態(tài)下，被保存的信號(hào)沒(méi)有出現(xiàn)在該狀態(tài)的輸入符中，則該信號(hào)將被丟棄。72狀態(tài)機(jī)保存（2）S1sig2sigbS2sig1S2sig3sigcS3sig1

22、sigaS4信號(hào)到達(dá)順序：1）sig1, sig2, sig3；2）sig2, sig3, sig1Slide 7273Slide 73遷移過(guò)程概述（1）狀態(tài)機(jī)所要完成的動(dòng)作集中在遷移過(guò)程中這些動(dòng)作包括：任務(wù)輸出信號(hào)設(shè)置定時(shí)器復(fù)位定時(shí)器輸出變量值創(chuàng)建代理實(shí)例調(diào)用過(guò)程調(diào)用遠(yuǎn)端過(guò)程等74Slide 74遷移過(guò)程概述（2）遷移過(guò)程結(jié)束于以下幾種情況： 到達(dá)狀態(tài) 僅適用于從開(kāi)始域進(jìn)入的遷移過(guò)程； 到達(dá)下一狀態(tài) 完成狀態(tài)轉(zhuǎn)移； 到達(dá)分支域 產(chǎn)生多個(gè)分支，每個(gè)分支將開(kāi)始一個(gè)新的遷移過(guò)程； 到達(dá)終止符 進(jìn)程實(shí)例到此終止（stop）； 合并到另一個(gè)遷移過(guò)程中 合并點(diǎn)以下的操作對(duì)兩個(gè)遷移過(guò)程是相同的； 遇出連接

23、符 后續(xù)動(dòng)作將在具有相同連接名的入連接符開(kāi)始的遷移過(guò)程中繼續(xù)； 到達(dá)返回符 適用于過(guò)程返回的情況75Slide 75遷移過(guò)程輸出（1）輸出的作用是通過(guò)信道把信號(hào)發(fā)送到另一代理實(shí)例輸出操作是代理之間通信的基礎(chǔ)輸出符定義：輸出信號(hào)可以是一個(gè)或多個(gè)帶參數(shù)的信號(hào)在輸出符中需要給出實(shí)際參數(shù)值76遷移過(guò)程輸出（2）輸出舉例to status1s3p1_pid:=senders2 to p1_pidstatus2Slide 7677Slide 77遷移過(guò)程輸出（3）to status1s3status2s1 to p378Slide 78遷移過(guò)程輸出（4）via status1s3status2s1 via

24、 c2via c179Slide 79遷移過(guò)程輸出（5）P1P2P3S1,S2S5,S6S1,S7C1C2S3,S4在進(jìn)程P2中，以下輸出是允許的：S1 to P3S1 via C1S7 via C2S2via C2在進(jìn)程P2中，以下輸出是不允許的：因?yàn)樾盘?hào)S1可通過(guò)兩條信道C1和C2發(fā)送出去S180Slide 80遷移過(guò)程輸出（6）信號(hào)中參數(shù)的使用 聲明信號(hào)時(shí),按順序給出各參數(shù)的數(shù)據(jù)類型signal s1(integer,boolean,octet); 輸出信號(hào)時(shí),為每個(gè)參數(shù)賦值s1(var_send_int,var_send_bool,var_send_octet); 輸入信號(hào)時(shí), 使用同

25、類型變量來(lái)接收各參數(shù)值s1(var_rece_int,var_rece_bool,var_rece_octet); 定義信號(hào)列表時(shí),信號(hào)名后不需要帶參數(shù)signallist sig_list=s1,s2,s3; 保存信號(hào)時(shí),信號(hào)名后不需要帶參數(shù)s1,s2,s381Slide 81遷移過(guò)程創(chuàng)建代理實(shí)例代理實(shí)例的創(chuàng)建分為兩種： 靜態(tài)創(chuàng)建 動(dòng)態(tài)創(chuàng)建實(shí)例創(chuàng)建符代理實(shí)例被創(chuàng)建后，該實(shí)例的self和parent就被賦好了值。創(chuàng)建是否成功的判斷82caller(0,128)S1C1manager(1,1)callercaller_pid:=offspringcaller_pid=NULLfalseS1 to

26、 caller_pidSlide 82true83Slide 83遷移過(guò)程任務(wù)（1）任務(wù)執(zhí)行與變量有關(guān)的動(dòng)作，如給變量賦值、計(jì)算表達(dá)式等任務(wù)符一個(gè)任務(wù)符中可以包含多條語(yǔ)句，語(yǔ)句之間用分號(hào)（；）隔開(kāi)；在任務(wù)符中的語(yǔ)句可以有下列幾種： 賦值語(yǔ)句 IF語(yǔ)句 分支語(yǔ)句 組合語(yǔ)句 設(shè)置語(yǔ)句（設(shè)置定時(shí)器） 復(fù)位語(yǔ)句（復(fù)位定時(shí)器）84x:=9;Flag:=true;y:=119.5賦值語(yǔ)句decision (a) (100) m:=n;else m:=n+1IF語(yǔ)句a:=b+1;if (b7) b:=1;else b:=b+1組合語(yǔ)句85Slide 85遷移過(guò)程任務(wù)（2）任務(wù)符中還可以包含非形式化文本，非形

27、式化文本是用單引號(hào)括起來(lái)的字符串非形式化文本被視為注釋內(nèi)容，不會(huì)被執(zhí)行在下列場(chǎng)合下可使用非形式化文本： 在開(kāi)發(fā)過(guò)程中，當(dāng)部分功能描述還未細(xì)化時(shí)，可用非形式化文本來(lái)說(shuō)明這部分功能； 系統(tǒng)中需要說(shuō)明一些對(duì)硬件的操作時(shí)，可用非形式化文本來(lái)說(shuō)明； 當(dāng)SDL文檔不需要詳細(xì)描述時(shí)，可用非形式化文本做簡(jiǎn)要說(shuō)明； 當(dāng)SDL文檔主要用來(lái)供人閱讀理解時(shí)，可用非形式化文本來(lái)說(shuō)明 在SDL圖中嵌入編程語(yǔ)言語(yǔ)句86Slide 86遷移過(guò)程過(guò)程調(diào)用（1）允許有任務(wù)的地方都可使用過(guò)程調(diào)用過(guò)程調(diào)用就是執(zhí)行一遍過(guò)程描述的功能過(guò)程與任務(wù)的區(qū)別 過(guò)程可以有狀態(tài)，過(guò)程使用調(diào)用該過(guò)程的代理實(shí)例的輸入隊(duì)列 過(guò)程中可以發(fā)送信號(hào)，過(guò)程發(fā)出的

28、信號(hào)相當(dāng)于調(diào)用該過(guò)程的代理實(shí)例發(fā)出的信號(hào)過(guò)程的調(diào)用x:=call 87process caller1(18)setdataSlide 87遷移過(guò)程過(guò)程調(diào)用（2）過(guò)程調(diào)用方法步驟1在包含該過(guò)程的進(jìn)程中聲明該過(guò)程88procedure setdata1(1)fpar in/out number integer;number:=128Slide 88遷移過(guò)程過(guò)程調(diào)用（3）步驟2 描述該過(guò)程的功能89process caller8 (18)idles1(send_data)setdata(set_number)s2(set_number) to p1State_nSlide 89遷移過(guò)程過(guò)程調(diào)用（4）

29、步驟3 調(diào)用該過(guò)程90Slide 90遷移過(guò)程分支操作分支操作用來(lái)結(jié)束一個(gè)遷移過(guò)程，然后根據(jù)表達(dá)式的值產(chǎn)生多個(gè)新的不同遷移過(guò)程分支符：分支符有一個(gè)入口，兩個(gè)或多個(gè)出口可以為表達(dá)式、非形式文本或any“any”表示將隨機(jī)產(chǎn)生分支。這種分支操作可用來(lái)描述一些不確定或不可靠的情況91具有多個(gè)出口的分支操作x+ybafalsetrue1else具有兩個(gè)出口的分支操作any92Slide 92遷移過(guò)程連接連接的功能是把屬于同一遷移過(guò)程的兩部分連接起來(lái)連接符93processp18(18)s1setupSetup_ack to p21Slide 9394processp112(18)1set(T)Setu

30、p to p3wait_ackSlide 9495遷移過(guò)程合并遷移過(guò)程s1Tsignal1reset(T)signal3s2signal2reset(T)signal4set(T)s396Slide 96定時(shí)器操作（1）定時(shí)器用來(lái)設(shè)置等待某事件發(fā)生的時(shí)間定時(shí)器的操作 設(shè)置定時(shí)器：在系統(tǒng)中啟動(dòng)一個(gè)定時(shí)器 復(fù)位定時(shí)器：停止計(jì)時(shí)定時(shí)器的應(yīng)用方法 聲明定時(shí)器：定時(shí)器可以帶參數(shù)，參數(shù)主要用來(lái)區(qū)別不同的監(jiān)視對(duì)象:timer wait_sig_time(user_id):=wait_duration;如果定時(shí)器每次設(shè)置的時(shí)間都一樣，可以在定義時(shí)給其賦值:timer T,T1=60.0; 定時(shí)器設(shè)置:set(

31、now+var_duration,T) set(T1) 復(fù)位定時(shí)器:reset(T); reset(T1); reset(T2(1)97定時(shí)器操作（2）定時(shí)器超時(shí)用包含定時(shí)器名的輸入符來(lái)表示，對(duì)于帶參數(shù)的定時(shí)器，需用具有相同數(shù)據(jù)類型的變量來(lái)接收參數(shù)值TT2（X）T198Slide 984-3、SDL中的數(shù)據(jù)99Slide 99內(nèi)容概述數(shù)據(jù)的定義數(shù)據(jù)的使用100Slide 100SDL中的數(shù)據(jù)概述數(shù)據(jù)類（Data Type）:數(shù)據(jù)類型（Sort）+ 操作（Operation）數(shù)據(jù)類型：數(shù)據(jù)項(xiàng)或元素的集合數(shù)據(jù)類型元素：數(shù)值（value）、對(duì)象（object）、進(jìn)程標(biāo)識(shí)（pid）布爾數(shù)據(jù)項(xiàng)： 布爾數(shù)

32、據(jù)類型包含兩個(gè)元素：false，true 支持的操作：=，/=，not，and，or，xor，=101數(shù)據(jù)定義數(shù)據(jù)類（data type）定義預(yù)定義數(shù)據(jù)類結(jié)構(gòu)（struct）選擇（choice）通過(guò)特殊化（specialization）定義新數(shù)據(jù)類同義類（Syntype）定義同義詞（Synonym）定義Slide 101定義新數(shù)據(jù)類通過(guò)使用預(yù)定義生成器定義新數(shù)據(jù)類串（String）數(shù)組（Array）通過(guò)使用數(shù)據(jù)類構(gòu)造器定義新數(shù)據(jù)類字面量（literals）102Slide 102預(yù)定義數(shù)據(jù)類（1）SDL中預(yù)定義的數(shù)據(jù)類包括：Boolean：布爾型Character：字符型Charstring：

33、字符串型Integer：整型Natural：自然數(shù)型Real：實(shí)數(shù)型Pid：進(jìn)程標(biāo)識(shí)型Duration：時(shí)長(zhǎng)類型103Slide 103預(yù)定義數(shù)據(jù)類（2）Boolean類= : Boolean, Boolean - Boolean 蘊(yùn)涵操作：如果第一個(gè)操作數(shù)為true，第二個(gè)操作數(shù)為false，則操作結(jié)果為false；否則操作結(jié)果為true。既：true = true = truetrue = false = falsefalse = true = truefalse = false = true104Slide 104預(yù)定義數(shù)據(jù)類（3）Character類num : Character -

34、Integer;num（A）=65chr : Integer- Characterchr(65)=“A”105Slide 105預(yù)定義數(shù)據(jù)類（4）Charstring類first:Charstring-character;first(hello)=hmkstring:Character-charstring;length:Charstring-integer;length(Hello)=5;last:Charstring-character;last(hello)=o106Slide 106預(yù)定義數(shù)據(jù)類（4）Real類float : Integer-Real;float(100)=100.0f

35、ix:Real-floatfix(138.6)=138107newtype S1元素類為整型string(Integer, Empty)endnewtype;Empty代表空串Slide 107預(yù)定義生成器串（String）S1是一個(gè)由Integer 構(gòu)成的串108newtype A1為CharacterArray(Character, Integer)endnewtype;元素類型為IntegerSlide 108預(yù)定義生成器數(shù)組（Array）A1是一個(gè)通過(guò)字符值來(lái)索引的數(shù)組數(shù)據(jù)類的索引類型109Slide 109數(shù)據(jù)類構(gòu)造器字面量（Literals）newtype colorsLitera

36、ls red, yellow, blue, greenendnewtype;使用Literals定義的數(shù)據(jù)類支持以下操作：賦值操作、比較操作、first、last、succ、pred、numdcl color colors；數(shù)據(jù)類構(gòu)造器通過(guò)列舉或構(gòu)造數(shù)據(jù)類型中元素的方法來(lái)描述數(shù)據(jù)類型的內(nèi)容。110Slide 110數(shù)據(jù)類構(gòu)造器結(jié)構(gòu)（Struct）例：newtype Person StructName Charstring;Age Integer;Address Charstring;PhoneNumber Charstring;endnewtypedcl p1 Person;111Slide 111數(shù)據(jù)類構(gòu)造器選擇（Choice）例：newtype C1 choicea Integer;b Charstring;c Boolean;endnewtype;dcl var C1;var!a=5;112定義新的數(shù)據(jù)類特殊化（Specialization）newtype this_struct structa Integer;b Character;endnewtype;newt