軟件體系結(jié)構(gòu)形式化描述ppt精選課件

.,1,軟件體系結(jié)構(gòu)(4）軟件體系結(jié)構(gòu)形式化描述覃征教授,SoftwareArchitecture,.,2,內(nèi)容概要,形式化描述簡(jiǎn)介軟件體系結(jié)構(gòu)的描述軟件體系結(jié)構(gòu)形式化描述實(shí)例：WRIGHTWRIGHT應(yīng)用范例,.,3,抽象認(rèn)識(shí)事物本質(zhì)的慣用法,抽象是人類(lèi)對(duì)實(shí)際事物在針對(duì)某一特定關(guān)點(diǎn)下的簡(jiǎn)化突出我們希望認(rèn)識(shí)的各個(gè)元素允許我們對(duì)關(guān)注的結(jié)構(gòu)和行為進(jìn)行辨識(shí)和分析在構(gòu)建新的實(shí)例時(shí)可以作為藍(lán)圖,.,4,抽象實(shí)例：運(yùn)動(dòng)系統(tǒng),.,5,抽象實(shí)例：動(dòng)力系統(tǒng),忽略了施力者和受力者的實(shí)體忽略了次要的環(huán)境作用，如地面、空氣忽略了傳力媒介突出了力和運(yùn)動(dòng)狀態(tài)之間的關(guān)系,.,6,形式化的抽象,實(shí)際事物,形式化方法,.,7,內(nèi)容概要,形式化描述簡(jiǎn)介軟件體系結(jié)構(gòu)的描述軟件體系結(jié)構(gòu)形式化描述實(shí)例：WRIGHTWRIGHT應(yīng)用范例,.,8,軟件體系結(jié)構(gòu)的描述,軟件體系結(jié)構(gòu)和軟件體系結(jié)構(gòu)描述不同的兩個(gè)概念軟件體系結(jié)構(gòu)是附屬于系統(tǒng)之中。只要存在系統(tǒng)，體系結(jié)構(gòu)就存在如：每個(gè)石頭都會(huì)有重量軟件體系結(jié)構(gòu)描述是將體系結(jié)構(gòu)可視化的手段和產(chǎn)物如：表示一個(gè)石頭的重量,.,9,如何理解體系結(jié)構(gòu)描述,.,10,體系結(jié)構(gòu)描述方式,使用不同的策略和方法可對(duì)同一軟件體系結(jié)構(gòu)作不同的理解和描述如：描述一塊石頭的重量比較輕比另一塊重一些大約2公斤四斤六兩2.32Kg5.114751207磅,精確程度不同單位不同測(cè)量基準(zhǔn)不同,描述方式不同,.,11,體系結(jié)構(gòu)描述方式,體系結(jié)構(gòu)描述方式標(biāo)準(zhǔn)語(yǔ)義豐富性語(yǔ)義精確性形式化程度主要描述方式非標(biāo)準(zhǔn)的圖形符號(hào)UML模塊接口語(yǔ)言MILADL,Richness,Preciseness,Formalization,O,.,12,非標(biāo)準(zhǔn)圖形符號(hào)描述,非標(biāo)準(zhǔn)圖形符號(hào)描述用由矩形框和有向線段組合而成的圖形表達(dá)工具。其中，矩形框代表抽象構(gòu)件，有向線段代表輔助各構(gòu)件進(jìn)行通訊、控制或關(guān)聯(lián)的連接件。特點(diǎn)語(yǔ)義豐富語(yǔ)義極不精確沒(méi)有形式化基礎(chǔ)用途商業(yè)展示設(shè)計(jì)草圖,.,13,非標(biāo)準(zhǔn)圖形符號(hào)描述,軟件體系結(jié)構(gòu)的非標(biāo)準(zhǔn)圖形符號(hào)表示具有如下優(yōu)點(diǎn)：直觀形象簡(jiǎn)單易用,.,14,非標(biāo)準(zhǔn)圖形符號(hào)描述,軟件體系結(jié)構(gòu)的非標(biāo)準(zhǔn)圖形符號(hào)表示具有如下缺點(diǎn)：由于其術(shù)語(yǔ)和表達(dá)語(yǔ)義上存在著一些不規(guī)范和不精確，從而使得以矩形為基礎(chǔ)的傳統(tǒng)圖形表達(dá)方法在不同系統(tǒng)和不同文檔之間存在著許多不一致甚至矛盾。,.,15,實(shí)例,EnterpriseJavaBeansArchitecture,.,16,實(shí)例,Microsoft.NetFrameworkArchitecture,.,17,實(shí)例,DC-LMPLinkManagementProtocolSoftware用于光纖網(wǎng)物理介質(zhì)連接器的軟件,.,18,UML,基于UML技術(shù)的軟件體系結(jié)構(gòu)描述方法1996年，Rational、Catapulse公司發(fā)起workshop，倡議用UML進(jìn)行體系結(jié)構(gòu)描述和建模、特定領(lǐng)域體系結(jié)構(gòu)建模；對(duì)UML中的stereotypes、profiles等進(jìn)行擴(kuò)充，支持體系結(jié)構(gòu)的表示2004年，UML2.0發(fā)布，增強(qiáng)了通用軟件體系結(jié)構(gòu)的描述能力。本質(zhì)上UML是側(cè)重于面向?qū)ο螅∣O,ObjectOriented)軟件系統(tǒng)設(shè)計(jì)的語(yǔ)言,.,19,UML特性,特點(diǎn)語(yǔ)義極其豐富語(yǔ)義相對(duì)精確有少量的形式化基礎(chǔ)用途需求分析OO類(lèi)設(shè)計(jì)行為設(shè)計(jì)和分析代碼自動(dòng)生成,.,20,UML與RUP,UML本身只是一門(mén)語(yǔ)言，并不限定使用它的開(kāi)發(fā)過(guò)程。但UML特別適合使用在RUP(統(tǒng)一開(kāi)發(fā)工程）上。RUP定義了如何看待軟件系統(tǒng)（視圖：View）UML定義了如何從某個(gè)角度描繪軟件（圖：Diagram）,.,21,RUP4+1視圖,設(shè)計(jì)視圖,實(shí)現(xiàn)視圖,用例視圖,進(jìn)程視圖,部署視圖,系統(tǒng)綜合者-性能-可擴(kuò)展性-吞吐量,系統(tǒng)工程-系統(tǒng)拓?fù)浣Y(jié)構(gòu)-發(fā)布和安裝-通訊,最終用戶-功能性-詞匯量,程序員-軟件管理,RUPViews,分析員/測(cè)試員-動(dòng)作,.,22,RUP4+1視圖,用例圖（UseCaseView）由專門(mén)描述可被最終用戶、分析人員和測(cè)試人員看到的系統(tǒng)行為的用況組成。用例視圖實(shí)際上沒(méi)有描述軟件系統(tǒng)的組織，而是描述了形成系統(tǒng)體系結(jié)構(gòu)的動(dòng)力,.,23,RUP4+1視圖,設(shè)計(jì)視圖（DesignView）又稱邏輯視圖（LogicView），包含了類(lèi)、接口和協(xié)作，它們形成了問(wèn)題及對(duì)問(wèn)題解決方案的術(shù)語(yǔ)詞匯。這種視圖主要支持系統(tǒng)的功能需求，即系統(tǒng)提供給最終用戶的服務(wù)。,.,24,RUP4+1視圖,實(shí)現(xiàn)視圖（ImplementationView）包含了用于裝配與發(fā)布物理系統(tǒng)的構(gòu)件和文件。這種視圖主要對(duì)系統(tǒng)發(fā)布的配置管理，它由一些獨(dú)立的構(gòu)件和文件組成；這些構(gòu)件和文件可以用各種方法裝配，以產(chǎn)生運(yùn)行系統(tǒng)。,.,25,RUP4+1視圖,部署視圖（DeploymentView）包含了形成系統(tǒng)硬件拓?fù)浣Y(jié)構(gòu)的節(jié)點(diǎn)（系統(tǒng)在器上運(yùn)行）。這種視圖主要描述對(duì)組成物理系統(tǒng)部件分布、交付和安裝。,.,26,RUP4+1視圖,進(jìn)程視圖（ProcessView）包含了形成系統(tǒng)并發(fā)與同步機(jī)制的線程和進(jìn)程，該圖主要針對(duì)性能、可伸縮性和系統(tǒng)的吞吐量。,.,27,RUP視圖的實(shí)現(xiàn)方式,Deployment,Process,Design,UseCase,Implementation,RUPViews,UseCaseDiagramSequenceDiagram,ClassDiagramCompositeStructureDiagram,DeploymentDiagram,SequenceDiagramActivityDiagram,ClassDiagramObjectDiagramSequenceDiagramActivityDiagramStateDiagramArtifactDiagram,UMLDiagrams,.,28,UML圖實(shí)例,類(lèi)圖（ClassDiagram）,.,29,UML圖實(shí)例,用例圖（UseCaseDiagram）,.,30,UML圖實(shí)例,序列圖（SequenceDiagram）,.,31,UML圖實(shí)例,協(xié)作圖（CollaborationDiagram）,.,32,UML圖實(shí)例,構(gòu)件圖（ComponentDiagram）,.,33,基于OO的軟件體系結(jié)構(gòu)描述方法,OO描述方法的優(yōu)點(diǎn)：采用面向?qū)ο蠓椒?，更能反映軟件體系結(jié)構(gòu)的本質(zhì)特征。提供了多個(gè)視圖直觀形象地反映體系結(jié)構(gòu)元素所具有的功能、特征。通過(guò)類(lèi)圖、包圖等反映體系結(jié)構(gòu)的靜態(tài)特征，并通過(guò)協(xié)作圖、序列圖、部署圖等反映體系結(jié)構(gòu)的動(dòng)態(tài)特征。,.,34,基于OO的軟件體系結(jié)構(gòu)描述方法,OO描述方法的缺點(diǎn)：缺少形式化的描述方法，造成設(shè)計(jì)人員由于對(duì)軟件認(rèn)識(shí)的角度、方法不同，生成的體系結(jié)構(gòu)描述不盡相同，理解上存在的二義性。,.,35,模塊接口語(yǔ)言MIL,MIL(ModuleV=VNVT;1inp。DSADL針對(duì)分布式軟件的特征引入了并行描述機(jī)制、特殊的終結(jié)符號(hào)、條件產(chǎn)生式。,.,53,幾種ADL簡(jiǎn)介（續(xù)）,OOADL采用Z語(yǔ)言形式化描述軟件體系結(jié)構(gòu)。其中Z語(yǔ)言是基于一階邏輯（，）和集合論(，等）的一種數(shù)學(xué)語(yǔ)言。OOADL以O(shè)O范例作為核心，增加了a_kind_of”,“a_part_of”和“an_instance_of”等關(guān)鍵字來(lái)表示OO范例中的概括、聚集和實(shí)例化關(guān)系。,.,54,幾種ADL簡(jiǎn)介（續(xù)）,WRIGHT采用CSP做為形式化描述語(yǔ)言。CSP是基于字母表、跡和拒絕集的概念。從形式上，CSP進(jìn)程可以用一個(gè)3元組(A,F,D)表示，A表示字母表(Alphabet)，F(xiàn)表示失效（Failures），D表示偏差（Divergences）。進(jìn)程的字母表是進(jìn)程所參與的事件的集合。進(jìn)程的跡是進(jìn)程所允許的事件序列。,.,55,通過(guò)ADL看軟件,不同的ADL對(duì)軟件的理解不同WRIGHT將軟件理解為構(gòu)件、連接器、端口、角色，以及這些元素之間的聯(lián)系和約束。CSP的描述使其有利分析復(fù)雜行為。C2將軟件理解為構(gòu)件、端口和連接器。不過(guò)構(gòu)件有且只有Top和Bottom兩個(gè)端口。同時(shí)構(gòu)件和構(gòu)件之間僅通過(guò)Request和Notification兩種信息進(jìn)行通訊。適合描述交互式系統(tǒng)。ACME將軟件理解為具有屬性的構(gòu)件和連接器。具有大多數(shù)ADL的共性元素。善于在不同ADL之間進(jìn)行轉(zhuǎn)換。,.,56,通過(guò)ADL看軟件（續(xù)）,任何人都可以利用自己的關(guān)注點(diǎn)來(lái)看待并描述體系結(jié)構(gòu)，即可以定義自己的ADL回憶：用自己習(xí)慣的方式來(lái)描述一塊石頭的重量比較輕比另一塊重一些大約2公斤四斤六兩2.32Kg5.114751207磅,你心目中的軟件體系結(jié)構(gòu)是什么樣子？,你是如何抽象軟件，從而解決在設(shè)計(jì)和管理中的問(wèn)題的？,.,57,內(nèi)容概要,形式化描述簡(jiǎn)介軟件體系結(jié)構(gòu)的描述軟件體系結(jié)構(gòu)形式化描述實(shí)例：WRIGHTWRIGHT應(yīng)用范例,.,58,WRIGHT,WRIGHT起源AFormalApproachtoSoftwareArchitecture,RobertJ.Allen,Ph.D.Thesis,CarnegieMellonUniversity,TechnicalReportNumber:CMU-CS-97-144,May,1997.發(fā)展DynamicWRIGHT,.,59,WRIGHT應(yīng)用實(shí)例,應(yīng)用：將一個(gè)字符串讀入，修改字符串使其呈現(xiàn)大小寫(xiě)交替出現(xiàn)，然后輸出如：IlovethisgameILoVeThIsGaMe假設(shè)系統(tǒng)設(shè)計(jì)管道過(guò)濾器系統(tǒng)，它分解輸入流（使用過(guò)濾器Split）,分別處理各子流（使用過(guò)濾器Upper和Lower）,然后合并子流（使用過(guò)濾器Merge）。,本系統(tǒng)的模塊分解圖，側(cè)重于實(shí)現(xiàn),.,60,WRIGHT應(yīng)用實(shí)例,WRIGHT眼中的系統(tǒng),構(gòu)件,連接器,圖例：,角色,端口,.,61,WRIGHT應(yīng)用實(shí)例,WRIGHT語(yǔ)言描述,SystemCapitalize定義一個(gè)系統(tǒng)CapitalizeComponentSplitportIn輸入?yún)f(xié)議portLeft,Right輸出協(xié)議compspecSplit構(gòu)件規(guī)格說(shuō)明ComponentUpperportIn輸入?yún)f(xié)議portLeft,Right輸出協(xié)議compspecUpper構(gòu)件規(guī)格說(shuō)明ConnectorPipePipe連接器規(guī)格說(shuō)明Instancessplit:Split;upper:Upper;lower:Lower;merge:MergeEndCapitalize,中內(nèi)容為注釋藍(lán)色字為關(guān)鍵字,.,62,WRIGHT設(shè)計(jì)目標(biāo),支持體系結(jié)構(gòu)配置的描述體系結(jié)構(gòu)描述的最終目的是在高層抽象級(jí)上捕捉和利用一個(gè)系統(tǒng)的結(jié)構(gòu)。它必須可以定義一個(gè)系統(tǒng)中的構(gòu)件和構(gòu)件之間的交互行為。支持體系結(jié)構(gòu)風(fēng)格的描述除了描述單一系統(tǒng)的體系結(jié)構(gòu)，開(kāi)發(fā)人員必須能描述一系列類(lèi)似系統(tǒng)。這些體系結(jié)構(gòu)風(fēng)格提供了使用系統(tǒng)之間共性的方法。除此之外，在給定配置的情況下，兩種描述必須可以結(jié)合在一起，這樣我們就可以確定這兩種描述是否符合同一種給定的風(fēng)格。,.,63,WRIGHT設(shè)計(jì)目標(biāo)（續(xù)）,支持屬性分析描述行為的一個(gè)重要的目標(biāo)是使用這種描述理解系統(tǒng)的屬性。開(kāi)發(fā)人員可以使用描述去分析系統(tǒng)或者風(fēng)格，以確定系統(tǒng)是否滿足他們的要求。支持在實(shí)際問(wèn)題中的應(yīng)用如果描述的符號(hào)僅僅能應(yīng)用于有很大限制的環(huán)境中或者小系統(tǒng)中，那么這種描述將是不實(shí)用的。一種實(shí)用的符號(hào)表示可以擴(kuò)展到描述復(fù)雜的實(shí)際問(wèn)題。,.,64,基于WRIGHT的形式化描述,作為一種體系結(jié)構(gòu)描述語(yǔ)言，WRIGHT是根據(jù)構(gòu)件、連接器和配置等基本體系結(jié)構(gòu)的抽象而構(gòu)造的，并為這些元素提供了清晰的記號(hào)，把構(gòu)件形式化成計(jì)算，把連接器形式化成交互模式。下面分別介紹基于Wright的體系結(jié)構(gòu)基本元素的形式化描述。,.,65,基于WRIGHT的描述框架,構(gòu)件,接口（接口類(lèi)型、接口類(lèi)型的參數(shù)化、接口類(lèi)型約束、實(shí)例）；計(jì)算,連接器,配置,附屬,層次,風(fēng)格,擴(kuò)展風(fēng)格,行為描述,事件、進(jìn)程、并行組合,配置的拓?fù)浣Y(jié)構(gòu),定義了配置可以共享的屬性集合,定義新的風(fēng)格,Wright體系結(jié)構(gòu)形式化描述框架,.,66,基于WRIGHT的描述元素1：構(gòu)件,構(gòu)件（Component）一個(gè)構(gòu)件描述了一個(gè)本地化、獨(dú)立的計(jì)算。例如，在“管道/過(guò)濾器”系統(tǒng)中，一個(gè)典型的構(gòu)件可以讀取系統(tǒng)的所有輸入并且把每個(gè)字母轉(zhuǎn)換成大寫(xiě)字母，或者把一個(gè)輸入流分成兩個(gè)，每隔一個(gè)字符送到不同的輸出。在一個(gè)數(shù)據(jù)庫(kù)系統(tǒng)中，構(gòu)件可能包括一個(gè)訪問(wèn)庫(kù)和一個(gè)用戶所請(qǐng)求的報(bào)表客戶端。在WRIGHT中，對(duì)構(gòu)件的描述包括兩個(gè)方面：接口（Interface）和計(jì)算(Computation)。一個(gè)接口有多個(gè)端口（Port）組成。每個(gè)端口表示構(gòu)件參與的一種交互。在下例中，一個(gè)過(guò)濾器構(gòu)件（分離過(guò)濾器）可能有三個(gè)端口，一個(gè)用于輸入，另外兩個(gè)用于輸出。,.,67,基于WRIGHT的描述元素1：構(gòu)件,接口類(lèi)型（InterfaceType）接口類(lèi)型可以用于描述構(gòu)件的端口，或者一個(gè)連接器的角色。在后者中，接口表示在角色中可能用到的端口接口的約束。例如：,.,68,基于WRIGHT的描述元素1：構(gòu)件,接口類(lèi)型參數(shù)化WRIGHT允許把一個(gè)類(lèi)型描述的任意部分變成預(yù)留空間，這些預(yù)留空間將在類(lèi)型實(shí)例化是利用參數(shù)進(jìn)行填充。因此，一個(gè)端口或者角色的類(lèi)型、一種計(jì)算、一個(gè)接口的命名等等都可以參數(shù)化。,.,69,基于WRIGHT的描述元素1：構(gòu)件,接口類(lèi)型參數(shù)化（續(xù)）除了在類(lèi)型描述中預(yù)留空間之外，還有一種通過(guò)數(shù)字（Number）參數(shù)化類(lèi)型描述。例如：,ComponentSplitFilter(nout:1.)PortInput=DataInputPortOutput1.nout=DataOutputComputation=反復(fù)從端口Input讀入數(shù)據(jù)，并將數(shù)據(jù)依次寫(xiě)入端口Output1，Output2，,.,70,基于WRIGHT的描述元素1：構(gòu)件,接口類(lèi)型約束在WRIGHT風(fēng)格描述中可聲明在這個(gè)風(fēng)格中的配置都必須遵循的屬性（即約束）。例如：,實(shí)例名,類(lèi)型名,取得類(lèi)型的操作,類(lèi)型名,意為：對(duì)于所有的連接器，它們的類(lèi)型都必須是Pipe（Pipe是連接器的一個(gè)類(lèi)型）,分隔聲明和約束,.,71,基于WRIGHT的描述元素1：構(gòu)件,一個(gè)“管道/過(guò)濾”系統(tǒng)實(shí)例：,系統(tǒng)功能：讀取一個(gè)字符流，并輸出把每隔一個(gè)的字符轉(zhuǎn)換成大寫(xiě)字母的字符流。,.,72,基于WRIGHT的描述元素1：構(gòu)件,SplitFilter構(gòu)件描述,SplitFilter,PortInput,PortLeft,PortRight,.,73,基于WRIGHT的描述元素2：連接器,連接器一個(gè)連接器代表了構(gòu)件集合內(nèi)各種構(gòu)件之間的交互。例如，一個(gè)管道代表了兩個(gè)過(guò)濾器之間的一個(gè)序列流。一個(gè)過(guò)程的調(diào)用就是一種“調(diào)用-返回”模式控制的連接器。更復(fù)雜的連接還有數(shù)據(jù)庫(kù)協(xié)議，例如，2-階段提交和可靠安全網(wǎng)絡(luò)消息的過(guò)濾。WRIGHT對(duì)連接器進(jìn)行描述時(shí)，可以分為一個(gè)角色（Role）的集合和粘合（Glue）。,.,74,基于WRIGHT的描述元素2：連接器,角色（Role）每個(gè)角色指定了在交互中單個(gè)參與者的行為。例如，在一個(gè)管道中有兩個(gè)角色：數(shù)據(jù)源和接收器（Sink），同時(shí)，角色指定了交互中構(gòu)件的參與者的期望。每種角色代表了一種構(gòu)件將要做什么，例如，接收器角色代表了那個(gè)參與者所期望的行為：任何作為接收器的構(gòu)件允許讀取數(shù)據(jù)并且負(fù)責(zé)關(guān)閉連接。,.,75,基于WRIGHT的描述元素2：連接器,粘合（Glue）一個(gè)連接器的粘合描述了參與者如何工作在一起創(chuàng)建一種交互，即連接器的粘合代表了完整的行為說(shuō)明。實(shí)際上，我們把一個(gè)連接器解釋成：如果真正的構(gòu)件符合角色所指定的行為，那么構(gòu)件的不同計(jì)算(Computation)將通過(guò)粘合而結(jié)合起來(lái)。如下例所示的一個(gè)管道例子，粘合描述了來(lái)自數(shù)據(jù)源的數(shù)據(jù)如何被傳送到接收器。一個(gè)過(guò)程調(diào)用將表示調(diào)用者初始化一個(gè)調(diào)用，緊接著從過(guò)程定義器返回。連接器的粘合說(shuō)明了構(gòu)件的計(jì)算是如何組成一個(gè)更大的計(jì)算。,.,76,基于WRIGHT的描述元素2：連接器,一個(gè)連接器描述實(shí)例管道連接器,Pipe,Source,Sink,Glue,.,77,基于WRIGHT的描述元素3：配置,配置（Configuration）為了描述一個(gè)完整的系統(tǒng)體系結(jié)構(gòu)，WRIGHT把對(duì)構(gòu)件和連接器的描述結(jié)合在一起，形成配置。一個(gè)配置就是通過(guò)連接器把構(gòu)件實(shí)例結(jié)合起來(lái)的一個(gè)集合。配置包括構(gòu)件和連接器的生成，以及附屬（Attachment）即將構(gòu)件的端口和連接器的角色連接起來(lái),.,78,基于WRIGHT的描述元素3：配置,實(shí)例因?yàn)樵谝粋€(gè)系統(tǒng)中可能多次使用給定的構(gòu)件或者連接器，所以我們把先前的描述作為構(gòu)件和連接器的類(lèi)型。為了在一個(gè)配置中區(qū)分每種構(gòu)件和連接器類(lèi)型的不同實(shí)例，WRIGHT描述語(yǔ)言要求每個(gè)實(shí)例必須清晰并且具有唯一性。下例描述了一個(gè)具有實(shí)例聲明的配置。,定義構(gòu)件連接器類(lèi)型,定義構(gòu)件連接器實(shí)例,連接端口和角色,.,79,基于WRIGHT的描述元素4：附屬,附屬（Attachment）在實(shí)例聲明之后，就可以描述附屬(Attachment)了，這樣配置才算是完整的。附屬說(shuō)明了哪些構(gòu)件參與哪些交互，從而定義了配置的拓?fù)浣Y(jié)構(gòu)。附屬的聲明把體系結(jié)構(gòu)描述的每個(gè)元素結(jié)合在一起。例如，構(gòu)件執(zhí)行一種計(jì)算(Computation)，這種計(jì)算的一部分是由端口(Port)指定的交互行為。這個(gè)端口與角色(Role)聯(lián)系在一起，這說(shuō)明了端口為了合法地參與連接器所指定的交互所必須遵從的規(guī)則。如果每個(gè)由各自的端口表示的構(gòu)件遵從角色所規(guī)定的規(guī)則，那么連接器的粘合(Glue)則定義了機(jī)算是如何結(jié)合在一起形成更大的計(jì)算。實(shí)例見(jiàn)上例,.,80,基于WRIGHT的描述元素5：層次,層次WRIGHT支持層次描述，如下層次結(jié)構(gòu)（服務(wù)器有內(nèi)部結(jié)構(gòu)）：,客戶,服務(wù)器,.,81,基于WRIGHT的描述元素5：層次,與上圖對(duì)應(yīng)的層次描述，縮進(jìn)可以幫助看清層次結(jié)構(gòu)：,接下頁(yè),.,82,基于WRIGHT的描述元素5：層次,定義次級(jí)構(gòu)件實(shí)例Coordinator類(lèi)型的c和SecurityManager類(lèi)型的Security,將次級(jí)結(jié)構(gòu)的構(gòu)件和連接器連接起來(lái),定義SecurityType的端口應(yīng)該指向其內(nèi)部結(jié)構(gòu)的哪個(gè)端口（如圖）,.,83,基于WRIGHT的描述元素6：風(fēng)格,風(fēng)格WRIGHT可以用于定義體系結(jié)構(gòu)的風(fēng)格。一種風(fēng)格定義了配置可以共享的屬性集合。這些屬性可以包括一個(gè)公共的詞匯集和約束集。在WRIGHT中，通過(guò)聲明一系列構(gòu)件和連接器的類(lèi)型引入公共的詞匯集，并且使用聲明的類(lèi)型進(jìn)行實(shí)例化說(shuō)明。例如，“管道/過(guò)濾器”風(fēng)格將包括連接器類(lèi)型“Pipe”的聲明，然后，如果在“管道/過(guò)濾器”風(fēng)格中聲明一個(gè)配置，那么該配置就可以自動(dòng)使用“Pipe”類(lèi)型了。,.,84,基于WRIGHT的描述元素7：擴(kuò)展風(fēng)格,擴(kuò)展風(fēng)格定義一種新風(fēng)格的重要方法是把新風(fēng)格描述成另外一種風(fēng)格的子風(fēng)格。如果新風(fēng)格具有另外一種風(fēng)格的所有約束條件，就可以新風(fēng)格描述成該風(fēng)格的子風(fēng)格。例如，我們可以把管道風(fēng)格定義成通過(guò)管道交互的線性序列的組合。這種風(fēng)格具有“管道/過(guò)濾器”風(fēng)格的所有限制。在定義子風(fēng)格時(shí)，把父風(fēng)格的名字放在子風(fēng)格名字的后面。這樣就可以包含父風(fēng)格所定義的所有詞匯和約束了。,.,85,基于WRIGHT的描述元素8：行為,體系結(jié)構(gòu)行為描述WRIGHT采用基于CSP（通信順序進(jìn)程，CommunicatingSequentialProcesses）的記號(hào)描述構(gòu)件的行為和構(gòu)件之間的協(xié)調(diào)關(guān)系。,.,86,我們?cè)谀睦?.,87,行為描述法的要求,必須可以反映體系結(jié)構(gòu)最常見(jiàn)的交互模式如過(guò)程調(diào)用，管道，事件，共享變量等等必須可以描述復(fù)雜的交互行為如哪一方先發(fā)起什么需求，然后另一方如何響應(yīng)要求必須可以區(qū)分相似行為的細(xì)微不同例如同樣是使用共享變量，具體是否需要初始化，如果需要，由誰(shuí)來(lái)初始化等,.,88,CSP簡(jiǎn)介,CSP起源Hoare，1978解決序列化的進(jìn)程描述以及這些進(jìn)程并行執(zhí)行時(shí)的交互問(wèn)題理論成形Hoare，Brookes，Roscoe，1984以事件為基礎(chǔ)的理論模型，構(gòu)建動(dòng)態(tài)的描述結(jié)構(gòu)，并提出了進(jìn)程間通訊的一些范式和準(zhǔn)則,C.A.RHoare,1980年圖靈獎(jiǎng)獲得者,.,89,CSP在哪里,Computation=,用CSP精確描述,反復(fù)從端口Input讀入數(shù)據(jù)，并將數(shù)據(jù)依次寫(xiě)入端口Output1，Output2，,source?xoutput1!xoutput2!xComputation,.,90,CSP基本概念,事件（Event）引發(fā)其它事件或者被其它事件引發(fā)的情況，CSP中最基本的單位。事件集（Alphabet）對(duì)某一系統(tǒng)進(jìn)行某種描述時(shí)所有相關(guān)的事件名稱組成的集合。如果系統(tǒng)名為S，則事件集表示為S進(jìn)程（Process）連續(xù)交互發(fā)生的一組事件的整體。有一個(gè)特殊的進(jìn)程叫STOP，表示系統(tǒng)停機(jī)。前束（Prefixing）由指定事件觸發(fā)某一進(jìn)程的關(guān)系，表示為eP選擇行為（Alternative）在某種情況下，可以有多種進(jìn)程發(fā)生。具體哪一種發(fā)生由環(huán)境決定不確定行為（Nondeterminism）在某種情況下，可以有多種進(jìn)程發(fā)生。具體哪一種發(fā)生有進(jìn)程自身決定,.,91,CSP實(shí)例行為能被描述么？,描述自動(dòng)售貨機(jī)的行為定義系統(tǒng)名稱SVM（簡(jiǎn)單自動(dòng)售貨機(jī)）定義事件coin：投一枚硬幣choc：得到一塊巧克力定義本系統(tǒng)的事件集SVM=coin,choc系統(tǒng)簡(jiǎn)化本描述只和顧客投幣并獲取巧克力相關(guān)，因此其它的事件在此描述中均被忽略事件發(fā)生的精確時(shí)間被忽略無(wú)須區(qū)分一個(gè)對(duì)象本身觸發(fā)和外界觸發(fā)的事件,.,92,CSP表現(xiàn)SVM行為,當(dāng)顧客投一個(gè)硬幣，自動(dòng)售貨機(jī)就停止工作SVM=(coinSTOP)當(dāng)兩個(gè)顧客分別投一個(gè)硬幣后，均得到一塊巧克力，之后再投幣，自動(dòng)售貨機(jī)停止工作SVM=(coin(choc(coin(chocSTOP)當(dāng)?shù)谝粋€(gè)和第二個(gè)硬幣投下后，巧克力出來(lái)之前，不可以再投入新的硬幣；巧克力出來(lái)之后，不投入新硬幣，不會(huì)再有巧克力出來(lái)：即不可能有多于一個(gè)的硬幣被連續(xù)投入，也不可能有多于一塊的巧克力連續(xù)出來(lái)CSP前束操作符有右結(jié)合性，所以上式等價(jià)于SVM=coinchoccoinchocSTOP,事件,前綴,進(jìn)程,.,93,CSP的遞歸定義,現(xiàn)實(shí)當(dāng)中有些對(duì)象在正常情況下的行為是永不停機(jī)的，用遞歸定義來(lái)描述這種情況對(duì)于系統(tǒng)SVM進(jìn)程描述：SVM=coinchocSVM,.,94,CSP描述體系結(jié)構(gòu)行為,引入成功完成的概念CSP中的STOP僅僅意味著系統(tǒng)停機(jī)，沒(méi)有成功或者失敗的意味。在體系結(jié)構(gòu)描述中引入事件“成功完成”的概念，用表示。WRIGHT定義=STOP事件可以伴隨數(shù)據(jù)。通常e?x表示輸入一個(gè)參數(shù)；e!x表示輸出一個(gè)參數(shù)引入作用域（Scope）的概念存在于某一作用域中的進(jìn)程僅在這個(gè)作用域中有效，效果等同于多元遞歸表示引入標(biāo)簽（Lable）的概念標(biāo)簽可以限定事件或者進(jìn)程的歸屬者。其中對(duì)于某一單個(gè)事件的標(biāo)簽使用“.”，例如l.e；對(duì)于某一進(jìn)程中的所有事件使用“:”，例如l:P通常使用來(lái)表示所有通用的事件，如l:表示所有通用的事件加上l這個(gè)標(biāo)簽,.,95,CSP的優(yōu)勢(shì)和劣勢(shì),其他的可選方案Petri網(wǎng)、SDL、I/O自動(dòng)機(jī)、狀態(tài)圖等在CSP中可以區(qū)分Alternatives和Nondeterminisms即由內(nèi)部進(jìn)行的決策和外部進(jìn)行的決策是分開(kāi)的CSP中有并行進(jìn)程組合機(jī)制，可以表達(dá)一個(gè)符合多個(gè)進(jìn)程描述的進(jìn)程CSP擁有成熟的工具支持缺點(diǎn)CSP中，時(shí)間是不被考慮的CSP中，進(jìn)程之間只存在觸發(fā)的關(guān)系,.,96,CSP應(yīng)用實(shí)例,我們用WRIGHT定義一個(gè)連接器ConnectorCSConnector=Roleclient=request!xresult?yclientRoleserver=invoke?xreturn!yserverGlue=client.request!xserver.invoke?xserver.return?yclient.result!yGlueclient、server、Glue均為進(jìn)程，request、result、invoke、return為事件。X為參數(shù)client從使用者的角度來(lái)描述其行為，request和result均為client的事件。client是反復(fù)執(zhí)行還是成功終止是由用戶自己決定的，環(huán)境無(wú)法干涉server從服務(wù)提供者的角度描述其行為，invoke和return為server的事件。server是反復(fù)執(zhí)行還是成功終止是由環(huán)境（這里特指用戶）決定的glue從連接器的角度將兩個(gè)角色的行為聯(lián)系起來(lái),Nondeterminism，表示由自身進(jìn)行選擇,Alternative，表示由環(huán)境進(jìn)行選擇,.,97,CSP連接端口和角色,端口行為也使用CSP表示例如ComponentDataUser=portDataRead=readDataReaddefinitionofotherports端口定義了系統(tǒng)的實(shí)際行為。將一個(gè)構(gòu)件的某個(gè)端口和一個(gè)連接器的某個(gè)角色連接起來(lái)，實(shí)際上端口將取代角色的位置。即角色只有占位符的意義。,.,98,CSP深入,CSP具有復(fù)雜的演算和證明體系CSP模型：事件集、跡、拒絕集CSP是基于字母表、跡和拒絕集的概念。從形式上，CSP進(jìn)程可以用一個(gè)3元組(A,F,D)表示，A表示事件集Alphabet），F(xiàn)表示失效（Failures），D表示偏差（Divergences）。進(jìn)程的事件集是進(jìn)程所參與的事件的集合。進(jìn)程P的字母表通常寫(xiě)成P。進(jìn)程的失效是跡與拒絕集組成的對(duì)。每個(gè)跡表示事件的有限序列，每個(gè)拒絕集是一個(gè)事件集。進(jìn)程的跡是進(jìn)程所允許的事件序列。例如，進(jìn)程P,可以產(chǎn)生的跡是(),(a),(b),(aa),(ab),(ba),等等，跡的全集用Traces(P)表示。事件的拒絕集可以用進(jìn)程的失效對(duì)表示。失效對(duì)的第一個(gè)元素是進(jìn)程的一個(gè)跡，第二個(gè)元素是進(jìn)程在該跡上的一個(gè)拒絕集。,.,99,CSP深入（續(xù)）,一個(gè)失效是一個(gè)跡和一個(gè)事件集。對(duì)于一個(gè)給定的跡，可能存在多個(gè)拒絕集。因?yàn)榫芙^集是子集閉合的，也就是說(shuō)，如果一個(gè)構(gòu)件拒絕了一個(gè)事件集，它就可以拒絕該事件集的任何子集。另外，一個(gè)進(jìn)程可能可以分別拒絕事件的組合，但是并不是所有的組合。例如，進(jìn)程可以拒絕事件a或者事件b，但是不能同時(shí)拒絕二者。于是，進(jìn)程就有失效(),),(),a)和(),b)，但是沒(méi)有(),a,b)。然而，進(jìn)程就有失效(),a,b)，因?yàn)镾TOP選擇意味著不發(fā)生任何事件。,.,100,CSP深入（續(xù)）,并發(fā)交織（interleaving）隱藏接口并行條件超時(shí)（timeout）和中斷（interrupt）死鎖檢測(cè),.,101,WRIGHT基于CSP語(yǔ)義進(jìn)行的形式化校驗(yàn),構(gòu)件一致問(wèn)題,連接器一致問(wèn)題,風(fēng)格約束,實(shí)例聲明一致問(wèn)題,激發(fā)器一致問(wèn)題,定義1、測(cè)試2、測(cè)試3,定義2、測(cè)試5、測(cè)試6、測(cè)試7,測(cè)試4,測(cè)試8、測(cè)試9,測(cè)試1,一致問(wèn)題測(cè)試,.,102,內(nèi)容概要,形式化描述簡(jiǎn)介軟件體系結(jié)構(gòu)的描述軟件體系結(jié)構(gòu)形式化描述實(shí)例：WRIGHTWRIGHT應(yīng)用范例,.,103,WRIGHT應(yīng)用實(shí)例,實(shí)例內(nèi)容概要AEGIS系統(tǒng)說(shuō)明基于Wright的AEGIS體系結(jié)構(gòu)描述,.,104,AEGIS系統(tǒng)說(shuō)明,AEGIS武器系統(tǒng)是一個(gè)大型復(fù)雜的軟件系統(tǒng)，它可以控制美國(guó)海軍艦艇的許多防御功能.AEGIS系統(tǒng)的結(jié)構(gòu)如下圖所示，原始的體系結(jié)構(gòu)描述由七個(gè)構(gòu)件組成其中，實(shí)驗(yàn)控制模塊提供了來(lái)自傳感器和操作者的仿真輸入，“心跳”信號(hào)表示了仿真時(shí)間。跟蹤數(shù)據(jù)被送往跟蹤服務(wù)器，該服務(wù)器記錄了當(dāng)前在監(jiān)視區(qū)域內(nèi)所監(jiān)視的移動(dòng)物體(導(dǎo)彈、其他星體和潛水艇等等)。規(guī)則創(chuàng)建模塊接收描述活動(dòng)的規(guī)則信息。GeoServer模塊接收規(guī)則信息(來(lái)自規(guī)則創(chuàng)建模塊)和跟蹤信息(來(lái)自跟蹤服務(wù)器)，并根據(jù)幾何模塊判定哪一個(gè)軌跡和哪一個(gè)幾何區(qū)域相交。這些信息(與軌跡和規(guī)則信息一起)被送往規(guī)則推理模塊，在這個(gè)模塊中決定采取任何什么行動(dòng)。圖中連線代表構(gòu)件的交互，箭頭表示了信息流的方向。,.,105,AEGIS系統(tǒng)說(shuō)明,AEGIS系統(tǒng)結(jié)構(gòu)圖,.,106,使用WRIGHT描述AE