通信協(xié)議分析-4-協(xié)議形式描述語言

第四章

協(xié)議形式描述語言自然語言優(yōu)點：可讀性好缺點：不準(zhǔn)確、存在二義性；從協(xié)議描述到協(xié)議實現(xiàn)較復(fù)雜、效率低、一致性差、必須手工完成；協(xié)議正確性驗證時存在同樣問題。程序設(shè)計語言優(yōu)點：易于實現(xiàn)缺點：可讀性差；難以表達(dá)并發(fā)性、不確定性等協(xié)議性質(zhì)和協(xié)議元素性質(zhì)；過多涉及協(xié)議實現(xiàn)細(xì)節(jié)，通常受特定設(shè)備環(huán)境約束。形式描述語言(FDL)優(yōu)點：基于協(xié)議模型技術(shù)，一般無二義性；表達(dá)協(xié)議并發(fā)性、不確定性、時序性、遞歸性等能力較強；為協(xié)議驗證、實現(xiàn)、測試和綜合過程的自動化和系統(tǒng)化提供良好的數(shù)學(xué)基礎(chǔ)。在上個世紀(jì)，ISO開始研究自己的形式描述技術(shù)。ISO/TC97/SC16/WG1正式成立了FDT特別小組，下分A、B和C三個分組：A組研究協(xié)議系統(tǒng)的總體結(jié)構(gòu)概念，供B組和C組使用B組研制擴展的狀態(tài)變遷模型語言ESTELLE(ExtendedStateTransitionmodELLanguagE)C組研制描述系統(tǒng)外觀行為的時態(tài)次序語言LOTOS(LanguageOfTemporalOrderingSpecification)。ISO在最后確定了這兩個語言最后的國際標(biāo)準(zhǔn)文本:ESTELLE(ISO9074)和LOTOS(ISO8807)主要內(nèi)容4.1ESTELLE4.1.1模塊概念4.1.2模塊通信4.1.3狀態(tài)轉(zhuǎn)換描述4.1.4ESTELLE協(xié)議描述示例4.1.5ESTELLE的特點和應(yīng)用4.2LOTOS4.2.1進(jìn)程定義4.2.2行為算子4.2.3抽象數(shù)據(jù)類型4.2.4門徑4.2.5LOTOS協(xié)議描述示例4.2.6LOTOS的特點及應(yīng)用4.1ESTELLE概述ESTELLE中，一個系統(tǒng)被描述為許多相互通信的模塊分層嵌套構(gòu)成，模塊之間通過通道通信（Channel），通道與模塊之間的連接點稱為交互點（InteractionPoints）。

每個模塊內(nèi)部有一個有限狀態(tài)機，有限狀態(tài)機的每個遷移或轉(zhuǎn)換都由某些輸入所觸發(fā)，狀態(tài)遷移過程中可能產(chǎn)生輸出。4.1ESTELLE概述基本特點：ESTELLE基于擴展的有限狀態(tài)機模型使用的是Pascal語法和數(shù)據(jù)類型，容易轉(zhuǎn)換為Pascal或C代碼ESTELLE對并發(fā)、不確定性、超時、異步通信狀態(tài)轉(zhuǎn)換有較強的表達(dá)能力從ESTELLE描述中易于提取出協(xié)議FSM模型或Petri網(wǎng)模型4.1ESTELLE概述用ESTELLE描述協(xié)議的最重要工作是構(gòu)造協(xié)議的模塊結(jié)構(gòu)和通信機制：系統(tǒng)中模塊的層次構(gòu)成模塊類別通道和交互點定義交互點隊列的屬性模塊和通道之間的連接4.1ESTELLE概述4.1.1模塊概念1、模塊(modules)

ESTELLE中，系統(tǒng)由相互通信的模塊分層嵌套構(gòu)成。每一層可有多個模塊，每個模塊通過通道以異步方式和其它的模塊(父模塊、兄弟模塊、子模塊)通信。模塊定義由兩部分組成：模塊頭和模塊體。一個模塊頭可有多個模塊體與之關(guān)聯(lián)。4.1ESTELLE概述4.1.1模塊概念1、模塊(modules)

模塊頭定義包含：外部交互點和輸出變量

模塊體定義包括三個主要部分：

說明部分—定義模塊所使用的通道、內(nèi)部交互點、數(shù)據(jù)類型和變量、模塊狀態(tài)、調(diào)用的過程和函數(shù)

初始化部分—定義模塊變量和狀態(tài)的初始值

轉(zhuǎn)換部分—按FSM定義模塊的狀態(tài)轉(zhuǎn)換過程，是模塊的關(guān)鍵部分4.1ESTELLE概述4.1.1模塊概念1、模塊(modules)module

模塊頭-A模塊類別 外部交互點說明; 輸出變量說明;end;body

模塊體-1for

模塊頭-A 通道說明; 內(nèi)部交互點說明; 數(shù)據(jù)類型和變量說明; 模塊狀態(tài)定義; 過程和函數(shù)定義; 模塊初始化部分; 狀態(tài)轉(zhuǎn)換部分;end;4.1ESTELLE概述4.1.1模塊概念2、模塊實例(moduleinstances)協(xié)議運行時，用ESTELLE定義的模塊可同時生成一個或多個模塊實例，并且模塊實例可以動態(tài)產(chǎn)生和消失。同一模塊的不同實例用模塊變量來標(biāo)識。父模塊實例初始化時負(fù)責(zé)子模塊實例的生成。例如：modvar mv-1:模塊頭-A; mv-2:模塊頭-A;initialize

begin

initmv-1with

模塊體-1;

initmv-2with

模塊體-2; ……

end;4.1ESTELLE概述4.1.1模塊概念3、模塊類別(moduleclass)

按模塊體定義是否包含狀態(tài)轉(zhuǎn)換部分來說，模塊分為：

非活躍模塊(inactivemodules)

模塊體內(nèi)無狀態(tài)轉(zhuǎn)換部分，初始化非活躍模塊所產(chǎn)生的模塊實例也是非活躍的。

活躍模塊(activemodules)

模塊體包括狀態(tài)轉(zhuǎn)換部分。

特征模塊(attributedmodules)

當(dāng)一個模塊頭定義有多個模塊體定義與之關(guān)聯(lián)，如果至少有一個模塊體內(nèi)包含狀態(tài)轉(zhuǎn)換部分，此種模塊叫做特征模塊。4.1ESTELLE概述4.1.1模塊概念3、模塊類別(moduleclass)按模塊的工作方式，可以分為：1）系統(tǒng)進(jìn)程模塊(systemprocess)本身可以是特征模塊，但其父模塊必須為非特征的系統(tǒng)進(jìn)程模塊，其子模塊可以是任意類別模塊。該系統(tǒng)模塊內(nèi)的各個子模塊可以并行執(zhí)行，而父模塊則優(yōu)先于子模塊執(zhí)行。4.1ESTELLE概述4.1.1模塊概念3、模塊類別(moduleclass)按模塊的工作方式，可以分為：2）系統(tǒng)活動模塊(systemactivity)本身可以是特征模塊，但父模塊必須為非特征的系統(tǒng)進(jìn)程或系統(tǒng)活動系統(tǒng)模塊內(nèi)的各個子模塊只能串行運行，具體哪個子模塊執(zhí)行則是隨機選擇的，父模塊仍然優(yōu)先于子模塊執(zhí)行。4.1ESTELLE概述4.1.1模塊概念3、模塊類別(moduleclass)

按模塊的工作方式，可以分為：

3）進(jìn)程模塊(process)必須為特征模塊，子模塊不能為系統(tǒng)進(jìn)程和系統(tǒng)活動，只能為進(jìn)程工作方式和系統(tǒng)進(jìn)程一樣4.1ESTELLE概述4.1.1模塊概念3、模塊類別(moduleclass)

按模塊的工作方式，可以分為：

4）活動模塊(Activity)必須為特征模塊，子模塊不能為系統(tǒng)進(jìn)程和系統(tǒng)活動，只能為活動工作方式和系統(tǒng)活動一樣4.1ESTELLE概述4.1.1模塊概念4、specification模塊用ESTELLE描述一個協(xié)議時，描述文本總是從關(guān)鍵詞(specification)開始。由specification開始的整個協(xié)議描述也是一個模塊，它是最高層模塊。

specification模塊可以是非活躍模塊(不給出模塊類別)，也可以是系統(tǒng)模塊(systemprocess或systemactivity)。4.1ESTELLE概述4.1.1模塊概念5、模塊嵌套規(guī)則(modulenestingrules)系統(tǒng)模塊(System)的父模塊必須為非特征模塊系統(tǒng)模塊的子模塊必須為特征模塊同一級可有多個系統(tǒng)模塊非系統(tǒng)模塊的子模塊不能為系統(tǒng)模塊systemprocess的子模塊可以是process或activity，systemactivity的子模塊必須為activityprocess的子模塊必須為process，activity的子模塊必須為activity非活躍模塊頭定義可以不指明“模塊類別”(a)(b)(c)(d)4.1ESTELLE概述4.1.2模塊通信1、通道(channels)通道定義包括三部分：通道名、通信角色和各個通信角色對通道的交互信息。一般，一個通道只有兩個通信角色(一端一個)，每個角色向通道發(fā)出什么交互信息(即報文名、服務(wù)原語名等),以及各個交互所附帶的參數(shù)都必須在通道定義中給出。例如TSAP定義為通道：

Channeltsap-type(user,provider)

byuser: t-connection-req(source:address-type,…); t-data-req(user-data:user-data-type,…); ……

byprovider: t-connection-ind(source:address-type,…); t-data-ind(user-data:user-data-type,…); ……4.1ESTELLE概述4.1.2模塊通信2、交互點(interactionpoints，ip)一個通道定義二個通信角色，這不意味著只能有兩個模塊使用一個通道。多個模塊可扮演同一個通信角色使用同一個通道。一個模塊必須定義一個交互點之后才能將它自己與一個通道聯(lián)系起來。如果一個模塊要使用父模塊定義的通道，它必須在模塊頭定義中給出交互點定義，這種交互點叫做外部交互點。如果一個模塊要使用它自己定義的通道，那么它必須在模塊定義中給出交互點定義，這種交互點叫做內(nèi)部交互點。4.1ESTELLE概述4.1.2模塊通信3、交互點綁定(ipbinding)一個獨立的交互點無通信能力，只有當(dāng)兩個以上的交互點綁定(binding)在一起時，一個交互點的輸入事件才能作為輸出事件傳遞到另一個交互點。connect語句和attach語句將交互點綁定在一起；disconnect語句和detach語句解除ip的綁定。4.1ESTELLE概述4.1.2模塊通信3、交互點綁定(ipbinding)connect格式：connectip-1toip-2disconnect格式：disconnectip-1或ip-2attach格式：attacheiptochild-eipdetach格式：detacheip或child-eip4.1ESTELLE概述4.1.2模塊通信4、聯(lián)接端點(connection

endpoints)多個ip利用多條connect語句和attach語句串行綁定在一起可形成一條聯(lián)接(connection)。聯(lián)接兩端的ip叫做聯(lián)接端點。聯(lián)接的主要特征：進(jìn)入一個聯(lián)接端點的輸入事件將自動傳遞到另一端的聯(lián)接端點的隊列中，中間ip的隊列隱藏起來。下圖是由四個模塊W,X,Y,Z嵌套形成的系統(tǒng)：4.1.2模塊通信4、聯(lián)接端點(connection

endpoints)四個ip形成一條聯(lián)接，a和d為聯(lián)接端點。從a輸入的信息進(jìn)入d的隊列，從d輸入的信息進(jìn)入a的隊列。如果在Y中發(fā)出detachc，那么聯(lián)接端點改為a和c。如果在X中發(fā)出detachb，那么聯(lián)接端點改為a和b，c和d變?yōu)榉墙壎╥p。如果在W中發(fā)出disconnecta，那么由b,c和d形成的聯(lián)接無通信能力。channelCH(user,provider);byuser:……byprovider:……ipa:CH(user)individualqueue;ipb:CH(provider)individualqueue;ipc:CH(provider)individualqueue;ipd:CH(provider)individualqueue;4.1ESTELLE概述4.1ESTELLE概述4.1.2模塊通信5、ip隊列定義ip時必須指明ip的隊列性質(zhì)：commonqueueindividualqueue多個模塊使用同一個通道時，它們可使用自己的單獨隊列，也可以共享隊列。如果定義在通道同一端的ip隊列為commonqueue，那么定義這些ip的模塊使用共享隊列。4.1.2模塊通信5、ip隊列a的輸入事件進(jìn)入d的單獨隊列，f的輸入事件進(jìn)入c的單獨隊列，d和e的輸入事件進(jìn)入a和b的共享隊列，b和c的輸入事件進(jìn)入e和f的共享隊列。4.1ESTELLE概述4.1ESTELLE概述4.1.2模塊通信6、輸入和輸出

when語句從ip讀入一個事件，而output語句往ip輸出一個事件。格式為：

whenip.m(arguments)

outputip.m(arguments)這里m(arguments)必須是channel定義中指明的交互事件。when語句從ip的隊列(FIFO)讀出事件，該事件是聯(lián)接的另一端output語句所輸出的事件。

由于FIFO隊列的原因，輸出和輸入不是同時發(fā)生的，因此模塊間通信是異步的。4.1ESTELLE概述4.1.3狀態(tài)轉(zhuǎn)換的描述1、描述語句

whenip.m

fromA

toB

providedE

delay(E1,E2)

priorityE

anyvardo

trans4.1ESTELLE概述4.1.3狀態(tài)轉(zhuǎn)換的描述2、轉(zhuǎn)換的選擇與執(zhí)行

轉(zhuǎn)換可分成三種狀態(tài):enabled:when，from和provided語句滿足，該轉(zhuǎn)換變成enabled狀態(tài)。fireable:delay和priority語句滿足，那么一個enabled轉(zhuǎn)換變成fireable狀態(tài)。如果無delay和priority語句，那么enabled狀態(tài)和fireable狀態(tài)相同。offered:對于某個模塊實例來說，它和它的子模塊中可能存在多個fireable轉(zhuǎn)換，模塊將選擇一個或多個轉(zhuǎn)換交付執(zhí)行，被交付執(zhí)行的轉(zhuǎn)換叫做offered轉(zhuǎn)換。模塊怎樣選擇fireable轉(zhuǎn)換取決于模塊本身類別和子模塊的結(jié)構(gòu)。選擇按4.1.1所述的原則先父后子，process并行，activity串行。4.1ESTELLE概述4.1.4AB協(xié)議的ESTELLE描述本節(jié)所描述的整個AB協(xié)議系統(tǒng)(類別為systemprocess)如下圖。4.1ESTELLE概述4.1.4AB協(xié)議的ESTELLE描述AB協(xié)議的模塊：用戶模塊AB協(xié)議模塊數(shù)據(jù)傳輸子模塊網(wǎng)絡(luò)模塊specification模塊，系統(tǒng)模塊單位時間大小定義常量定義超時重發(fā)間隔類型定義通道定義模塊頭定義交互點定義，包括通道，角色以及隊列說明模塊體定義，其中Network和User為外部模塊，用關(guān)鍵詞external標(biāo)識。模塊體說明部分，包括了：數(shù)據(jù)類型與變量；狀態(tài)與狀態(tài)集。模塊體說明部分，包括了：函數(shù)與過程等。模塊體初始化部分模塊體轉(zhuǎn)換部分4.1ESTELLE概述4.1.5ESTELLE的特點與應(yīng)用方法基于有限狀態(tài)機(FSM)模型。模塊實例可通過初始化語句動態(tài)產(chǎn)生。如果協(xié)議實現(xiàn)后模塊實例對應(yīng)于一個進(jìn)程或任務(wù)，那么網(wǎng)絡(luò)進(jìn)程或任務(wù)也是動態(tài)產(chǎn)生的。模塊通信為異步通信。是pascal語言的擴充，用ESTELLE描述的協(xié)議容易轉(zhuǎn)換成pascal或c代碼。因此，它是一種面向協(xié)議實現(xiàn)的FDL。對并發(fā)、不確定性、超時、異步通信狀態(tài)轉(zhuǎn)換有較強的表達(dá)能力，但對遞歸、共享通道(廣播通道)、同步通信、協(xié)議性質(zhì)(如不變性等)的表示缺少有力的手段。用ESTELLE描述的協(xié)議易于提取FSM模型和Petri網(wǎng)模型，但不容易提取轉(zhuǎn)變成CCS模型。4.1ESTELLE概述用ESTELLE描述一個協(xié)議，首先也是最重要的工作就是構(gòu)造協(xié)議的模塊結(jié)構(gòu)和通信機制。需要考慮：系統(tǒng)由多少層模塊構(gòu)成？每個模塊應(yīng)該是什么類別(類別決定了工作方式)？定義多少通道和交互點？交互點隊列屬于哪種？它們綁定成什么樣聯(lián)接？如果應(yīng)該定義為systemprocess類別的模塊定義systemactivity，則難以表示協(xié)議的并發(fā)性。4.2LOTOS概述基本思想：

外部可觀察到的系統(tǒng)行為由一系列交互作用組成，通過對這些交互作用的時間關(guān)系進(jìn)行定義，從而描述整個系統(tǒng)。4.2LOTOS概述LOTOS,(LanguageOfTemporalOrderingSpecifications),時序規(guī)范語言。

基于CCSISO標(biāo)準(zhǔn)化

可用于:通信協(xié)議、分布式時序并發(fā)系統(tǒng)

適用于:動態(tài)系統(tǒng)性能分析4.2LOTOS概述4.2.1進(jìn)程LOTOS將系統(tǒng)看做多個相互作用的子進(jìn)程組成的進(jìn)程，進(jìn)程與其他進(jìn)程交互(Interact)，與其交互的進(jìn)程構(gòu)成了它的環(huán)境（Environment）。進(jìn)程間的交互通過用于協(xié)同的基本單元建立，將這些用于協(xié)同的基本單元稱為事件（Events）進(jìn)程可能參與的所有事件的集合稱為該進(jìn)程的字母表（Alphabet）協(xié)同事件的發(fā)生點（兩個進(jìn)程的同步通信點）稱為門徑（Gates）4.2LOTOS概述4.2.1進(jìn)程Pacdebfg從外部環(huán)境看，進(jìn)程是一個黑盒4.2LOTOS概述4.2.2門徑門徑是協(xié)同事件的發(fā)生點，是兩個進(jìn)程的同步通信點，門徑的定義包括對多個通信變量的定義和輸入輸出參數(shù)的定義。

例如在ISO/OSI模型中，各層協(xié)議的服務(wù)訪問點就是一個門徑，TSAP的門徑定義如下：

t-addr:t-addr-sort

t-cep-id:tcep-id-sort

…

TCONreq|TCONind…4.2LOTOS概述4.2.2門徑進(jìn)程從門徑變量中輸入時用“?”操作符進(jìn)程向門徑變量中發(fā)送時用“！”操作符輸入輸出操作必須采用g?x:t和g!y的形式進(jìn)程也允許將同一個門徑內(nèi)對多個變量的讀寫組合操作，例如：Tsap?t-addr?tcep-id!TCONreq4.2LOTOS概述4.2.2門徑門徑的使用規(guī)則：各個進(jìn)程向門徑輸入或輸出數(shù)據(jù)的類型和順序必須與門徑定義一致兩個進(jìn)程通過同一個門徑變量可進(jìn)行“數(shù)值匹配”、“數(shù)值傳遞”、“數(shù)值生成”三種交互作用交互方式進(jìn)程A進(jìn)程B同步條件結(jié)果數(shù)值匹配g!E1g!E2數(shù)值相等（E1=E2）同步數(shù)值傳遞g!Eg?x:tE為t類型x=E數(shù)值生成g?x:tg?y:u類型一致(t=u)x=y4.2LOTOS概述4.2.2門徑門徑的使用規(guī)則：一個進(jìn)程對門徑進(jìn)行讀時，可進(jìn)行條件接收。例如a?xa:integer[xa<3]多個進(jìn)程可對同一門徑進(jìn)行輸入輸出操作，但協(xié)同事件在哪一對進(jìn)程間發(fā)生是不確定的4.2LOTOS概述4.2.2門徑

一個進(jìn)程所利用的門徑必須出現(xiàn)在進(jìn)程定義的gate-list中，兩個進(jìn)程要組合時需要說明兩個進(jìn)程的協(xié)同事件（門徑），必要時可隱藏門徑4.2LOTOS概述4.2.2門徑Max2Max2in1in2midoutin3processMax3[in1,in2,in3,out]:=hidemidin(Max2[in1,in2,mid]|[mid]|Max2[mid,in3,out])where…Endproc(*Max3*)4.2LOTOS概述4.2.3進(jìn)程定義processprocess-id[gate-list](parameter-list):noexit:=<behaviour-expression>endprocprocess和endproc－關(guān)鍵詞，表示進(jìn)程定義的開始和結(jié)束。process-id－進(jìn)程名gate-list－門徑表parameter-list－參數(shù)表behaviour-express－描述進(jìn)程行為的表達(dá)式noexit－表示進(jìn)程為非終止進(jìn)程的關(guān)鍵詞exit－說明進(jìn)程為終止進(jìn)程的關(guān)鍵詞。4.2LOTOS概述4.2.3進(jìn)程定義ProcessMax3[in1,in2,in3,out]hidemidin(Max2[in1,in2,mid]|[mid]|Max2[mid,in3,out])whereProcessMax2[a,b,c]:=a;b;c;stopb;c;a;stop[]endprocendproc行為表達(dá)式進(jìn)程定義進(jìn)程定義行為表達(dá)式4.2LOTOS概述4.2.4行為算子1、前綴(prefix)

前綴(用符號“;”)描述進(jìn)程順序執(zhí)行事件的行為，對應(yīng)于CCS的"."算子。例如:a;B：進(jìn)程執(zhí)行事件a之后，執(zhí)行行為表達(dá)式B。g?x:t;B：進(jìn)程執(zhí)行事件g?x:t之后，執(zhí)行行為表達(dá)式B。這里g?x:t為一個輸入事件，表示從門徑g輸入一個事件(數(shù)據(jù))，將它放入類型為t的變量x中。g!E;B：E為數(shù)值表達(dá)式，進(jìn)程執(zhí)行事件g!E之后，執(zhí)行行為表達(dá)式B。g!E為輸出事件，表示將數(shù)值表達(dá)式E之值輸出到作用點g。4.2LOTOS概述4.2.4行為算子2、選擇(choice)

選擇(用符號“[]”)描述進(jìn)程從多個行為表達(dá)式中選擇一個去執(zhí)行的行為，它對應(yīng)于CCS的"+"算子。例如:

B1[]B2

：選擇

B1或

B2

執(zhí)行。4.2LOTOS概述4.2.4行為算子3、并行(parallelism)

并行算子描述進(jìn)程并行執(zhí)行多個行為表達(dá)式的情況，它對應(yīng)于CCS的"|"算子。LOTOS的并行算子有三種形式:B1|[a1,…,an]|B2

：B1

和B2

通過門徑a1,…,an

并行。B1||B2

：B1和B2通過它們的所有事件并行，這是前種形式的特例。B1|||B2

：B1和B2獨立并行。這是CCS并行算子變種P1，即B1和B2之間無交互作用，但和它們的環(huán)境(即父進(jìn)程)有交互作用。一般情況下，Bl和B2相同。4.2LOTOS概述4.2.4行為算子4、串行(sequentiality)串行算子(用符號“>>”)描述進(jìn)程執(zhí)行一個行為表達(dá)式之后"使能"另一個行為表達(dá)式的行為，它是CCS順序算子變種S1和S2。例如:

B1>>B2

：如果B1成功結(jié)束則使能B2。4.2LOTOS概述4.2.4行為算子5、作廢(disruption)

作廢算子(用符號“|>”表示)描述進(jìn)程在后個行為表達(dá)式的事件發(fā)生時停止并且作廢前個行為表達(dá)式的行為。例如:

B1|>B2

：執(zhí)行B1時如果B2有事件發(fā)生，作廢B1，執(zhí)行B24.2LOTOS概述4.2.4行為算子6、隱藏(hide)隱藏算子描述進(jìn)程執(zhí)行并行算子時隱藏內(nèi)部協(xié)同事件的行為，它和CCS在利用擴展規(guī)則時限制協(xié)同事件的效果相同。隱藏算子的形式為:

hideainB：a為內(nèi)部事件，B行為表達(dá)式4.2LOTOS概述4.2.4行為算子7、看守(guard)看守表達(dá)式描述一個行為表達(dá)式是否執(zhí)行的條件，其形式為：

[cond]B：cond為條件表達(dá)式或謂詞，B為行為表達(dá)式。cond為真，執(zhí)行B。4.2LOTOS概述4.2.4行為算子8、終止(termination)表示進(jìn)程的終止有兩個關(guān)鍵詞：exit和stop

exit：成功結(jié)束

stop：停止進(jìn)程活動4.2LOTOS概述4.2.4行為算子9、內(nèi)部事件一個進(jìn)程的內(nèi)部事件用"I"表示。例如:

I;a;A[]I;b;B4.2LOTOS概述4.2.4行為算子a;P

順序，事件a后執(zhí)行Pa!x;P

門徑a輸出x后執(zhí)行Pa?x:int;P

門徑a輸入int類型變量x后執(zhí)行PP[]Q[]R

P、Q、R隨機/競爭選擇[cond]P[]

看守cond使能P，通常結(jié)合選擇P[a,b](formal_pars):=…;P[b,a](expr{pars})

進(jìn)程聲明，含門徑重命名和參數(shù)操作4.2LOTOS概述4.2.4行為算子P[a,b]||Q[b,c]

P和Q無條件并行P[a,b,c]|[a,b,c]|Q[a,b,c]

P和Q通過門徑[a,b,c]并行P[a,b]|[a]|Q[b,c]

P和Q通過門徑[a]并行a!x;P|[a]|a?y:int;Q

傳值并行，參數(shù)y的值為xa!x;P|[a]|a!y;Q

數(shù)值匹配并行，若x=y則可執(zhí)行a?x;P|[a]|a?y;Q

數(shù)值協(xié)商并行，任意輸入拷貝到x和y4.2LOTOS概述4.2.4行為算子10、雙緩沖通道的例子下圖中，進(jìn)程two-slot-buffer[i,o]為兩個單緩沖進(jìn)程buffer[i,m]和buffer[m，o]并行組合而成，事件m為它們協(xié)同事件。bufferbuffertwo-slot-bufferimo4.2LOTOS概述4.2.4行為算子10、雙緩沖通道的例子則系統(tǒng)的LOTOS定義如下： processtwo-slot-buffer[i,o]:= hideminbuffer[i,m]|[m]|buffer[m,o] where processbuffer[input,output]:= input;output;buffer[input,output] endproc endproc4.2LOTOS概述4.2.4行為算子10、雙緩沖通道的例子上述LOTOS定義可以化為CCS表達(dá)式。將two-slot-buffer記作P；buffer[i,m]記作A；buffer[m,o]記作B。則雙緩沖通道的CCS表達(dá)式為：

P=A|B\m (1) A=i.m.A (2) B=m.o.B (3)將上述CCS表達(dá)式進(jìn)行化簡可以得到：

P=i.Q (4)

Q=o.P+i.o.Q (5)4.2LOTOS概述4.2.4行為算子10、雙緩沖通道的例子利用(4)和(5)，反過來可以用LOTOS表示成嵌套的進(jìn)程定義：

processtwo-slot-buffer[i,o]:= i;Q[i,o] endproc processQ[i,o]:= o;two-slot-buffer[i,o] []i;o;Q[i,o] endproc4.2LOTOS概述4.2.5抽象數(shù)據(jù)類型(ACT.1)與程序設(shè)計語言無關(guān)的數(shù)據(jù)類型叫做抽象數(shù)據(jù)類型，是描述具體的數(shù)據(jù)類型(由不同程序設(shè)計語言實現(xiàn)的)的數(shù)學(xué)模型。抽象數(shù)據(jù)類型由數(shù)據(jù)目標(biāo)或載體集合和與之相關(guān)的操作定義以及操作性質(zhì)說明形成。數(shù)學(xué)上，一種抽象數(shù)據(jù)類型就是一種代數(shù)。例如： typenat-numberis sorts nat opns 0:nat succ:natnat endtype4.2LOTOS概述4.2.5抽象數(shù)據(jù)類型(ACT.1)一個定義可以引用另外一個定義，其目的有兩個：對一個己有的類型進(jìn)行擴充將幾個定義合成一個新定義例如：

typeen