陳 博，劉 翀，3，陳 輝，陳香蘭，3 ，李 曦，3

1(中國科學(xué)技術(shù)大學(xué) 軟件學(xué)院，江蘇 蘇州 215123)

2(華為信息技術(shù)有限公司，深圳 518000)

3(中國科學(xué)技術(shù)大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，合肥 230027)

1 引 言

為了更精確地認(rèn)識(shí)與改造世界，新一代的嵌入式系統(tǒng)必須將計(jì)算世界與物理世界作為一個(gè)緊密交互的整體來進(jìn)行認(rèn)識(shí)，實(shí)現(xiàn)一個(gè)集計(jì)算、通信與控制于一體的深度融合的理論體系與技術(shù)框架，即信息物理系統(tǒng)(Cyber Physical Systems，CPS).與傳統(tǒng)嵌入式系統(tǒng)(Embedded System，ES)不同，CPS充分考慮計(jì)算部件與物理環(huán)境的深度融合，通過將設(shè)備智能化連接，實(shí)現(xiàn)物理環(huán)境與計(jì)算系統(tǒng)之間的精確感知與高效協(xié)同.CPS通常被應(yīng)用在安全關(guān)鍵的場(chǎng)景中，需要對(duì)環(huán)境進(jìn)行實(shí)時(shí)監(jiān)測(cè)，計(jì)算反饋信息，最終實(shí)現(xiàn)自動(dòng)化的控制與管理，是一種具有異構(gòu)性、實(shí)時(shí)性的復(fù)雜系統(tǒng).CPS與傳統(tǒng)ES的工作方式相近，但傳統(tǒng)ES通常由簡(jiǎn)單的計(jì)算過程和物理環(huán)境兩部分組成，如燈光控制系統(tǒng)、水溫控制系統(tǒng)等，其計(jì)算部分通常執(zhí)行順序的、簡(jiǎn)單的周期性任務(wù)，并將處理結(jié)果反饋至外部的單一環(huán)境.而CPS中的計(jì)算過程通常由復(fù)雜的調(diào)度機(jī)制進(jìn)行多任務(wù)的調(diào)度執(zhí)行，實(shí)現(xiàn)對(duì)復(fù)雜外部環(huán)境的控制與管理[1].如典型的汽車電子控制系統(tǒng)由多個(gè)電子控制單元(Electronic Control Unit，ECU)及處理ECU之間通信的總線組成，其上實(shí)現(xiàn)了多種子系統(tǒng)，如牽引力控制系統(tǒng)，車身穩(wěn)定控制系統(tǒng)等.對(duì)類似系統(tǒng)進(jìn)行設(shè)計(jì)與實(shí)現(xiàn)是一個(gè)復(fù)雜的系統(tǒng)工程，而其中，如何在設(shè)計(jì)過程中保證CPS的實(shí)時(shí)性與正確性是關(guān)鍵的核心問題.

近些年，研究人員在CPS的開發(fā)方法上取得了豐碩的研究成果，但尚缺乏對(duì)這些成果進(jìn)行梳理、總結(jié)的綜述.基于此，本文將以CPS中最為關(guān)鍵的組件時(shí)間行為可組合問題為核心內(nèi)容，回顧組件化軟件開發(fā)的發(fā)展歷程，對(duì)組件行為抽象、組合操作的發(fā)展脈絡(luò)進(jìn)行梳理，并介紹近年為提升組件時(shí)間行為的可預(yù)測(cè)性、可組合性所提出的3種實(shí)時(shí)編程模型.最后，指出未來的若干研究方向.

2 組件化軟件開發(fā)方法

為了保證CPS中功能與非功能屬性的正確性，通常采用基于組件化(Component-Based Development，CBD)的開發(fā)方法對(duì)系統(tǒng)進(jìn)行建模、分析及功能的驗(yàn)證[2].圖1給出了基于軟件工程中V模型的組件化軟件的開發(fā)流程，與傳統(tǒng)軟件開發(fā)流程相同的是，開發(fā)過程都從需求分析到最終的代碼生成.而不同的是，組件化軟件的開發(fā)過程以模型為中心，首先建立需求模型，繼而逐步定義子系統(tǒng)模型，并通過不斷精化的方法對(duì)系統(tǒng)進(jìn)行開發(fā)，最終通過組合各子系統(tǒng)模型的方式對(duì)整體行為進(jìn)行描述，并通過確認(rèn)與驗(yàn)證(Validation & Verification，V&V)的方式對(duì)系統(tǒng)的功能屬性/非功能屬性進(jìn)行驗(yàn)證，最終生成具體的執(zhí)行代碼.因此，通過基于組件的開發(fā)方法對(duì)具有安全關(guān)鍵的CPS進(jìn)行實(shí)現(xiàn)將涉及到組件的時(shí)間行為抽象、時(shí)間行為精化，以及時(shí)間行為的組合與驗(yàn)證等具體技術(shù)細(xì)節(jié).本章將首先介紹組件化軟件的基本概念，然后引出組件組合的幾種方法.

圖1 基于V模型的組件化軟件開發(fā)流程

2.1 組件化軟件開發(fā)

組件是對(duì)功能單元的一種封裝，可以看作“黑盒功能抽象”，其通過接口向外部環(huán)境提供服務(wù)，也可稱為“軟件組件(software component)”，表達(dá)了組件隱藏內(nèi)部功能，同時(shí)向外提供服務(wù)的軟件形式.

在計(jì)算機(jī)的若干概念定義中，典型的定義形式如遵循Wengerzai在1987年給出的描述[3]：“當(dāng)事物滿足了某些屬性，則它就是某種類型的特定事物(something is an A if it has properties a1，a2，and a3)”.例如，當(dāng)某語言支持對(duì)象、類及繼承三種屬性時(shí)，則該語言就是面向?qū)ο笳Z言.因此，本文借鑒文獻(xiàn)[4]給出組件化軟件的普適定義1.

定義1.當(dāng)軟件架構(gòu)滿足如下屬性，則可以將該軟件定義為組件化軟件：

·是一個(gè)可以獨(dú)立進(jìn)行開發(fā)的軟件單元；

·支持與第三方軟件單元進(jìn)行組合；

·外部環(huán)境無法直接讀取組件內(nèi)部的狀態(tài)信息；

上述定義首先描述了組件應(yīng)該是一個(gè)獨(dú)立開發(fā)的個(gè)體，與外部環(huán)境和其它組件具有明確的功能界限劃分.其次，組件進(jìn)行了功能隱藏，封裝了自身的行為特征，并通過接口向外提供服務(wù).接口表明了組件向外部環(huán)境所提供服務(wù)的保證(Guarantee，如服務(wù)的時(shí)間、服務(wù)的類型等)，以及組件對(duì)外部環(huán)境所產(chǎn)生行為的期望(Assumption)，同時(shí)可以與其它組件通過組合操作來實(shí)現(xiàn)系統(tǒng)的整體功能.最后，組件是一個(gè)自給自足的個(gè)體，其它組件(或外部環(huán)境)只能通過接口向其請(qǐng)求服務(wù)，并得到計(jì)算結(jié)果.外部環(huán)境也不能顯式的獲取組件的狀態(tài)信息.

其次，針對(duì)組件的定義，Szyperski給出的描述為[4]：“組件的本質(zhì)是用于組合的”，表達(dá)了對(duì)組件最本質(zhì)的概念闡述.同樣，Meijler給出組件的兩個(gè)主要設(shè)計(jì)思想[5]：重用性與可組合性，兩者息息相關(guān).其中，重用性描述了組件在多個(gè)場(chǎng)景下的可重用能力，也可以理解為抽象化的程度，表達(dá)了當(dāng)組件的功能定義過于寬泛，即其功能定義過于抽象，則在一些場(chǎng)景下將導(dǎo)致組件重用靈活性的缺失，而當(dāng)組件的功能定義過于具體，則易增加組件組合操作的復(fù)雜性.

在編程語言的實(shí)現(xiàn)層面，如JavaBeans/CORBA/COM /.Net等編程語言都通過組件對(duì)功能進(jìn)行封裝，并給出了靜態(tài)、動(dòng)態(tài)屬性的組合規(guī)則.NeXTStep語言[6]定義了復(fù)雜的組件組合操作，將多個(gè)對(duì)象封裝在某nib文件中，同樣體現(xiàn)了組件的組合過程.再如TinyOS操作系統(tǒng)[7]下的應(yīng)用開發(fā)，該操作系統(tǒng)定義了clock/LED/Timer等多種資源組件，并由調(diào)度組件(scheduler component)協(xié)調(diào)執(zhí)行上層的任務(wù)組件，其開發(fā)過程也將組件的組合過程看作是對(duì)系統(tǒng)的配置.

綜合而言，組件是一種提供功能封裝，支持組件組合操作與精化的軟件設(shè)計(jì)思想.接下來，本文將給出組件行為抽象的一般方法，并給出組件組合的操作方法.

2.2 組件的組合操作

組件的組合操作是組件之間行為組合的計(jì)算過程.為方便敘述，本文通過標(biāo)簽遷移系統(tǒng)(Label Transition System，LTS)建模組件的個(gè)體行為，再將多個(gè)模型進(jìn)行組合，形成系統(tǒng)的整體模型.借鑒文獻(xiàn)[8]的描述，分別給出了3種典型的組件組合語義，首先給出遷移系統(tǒng)的定義.

定義2.遷移系統(tǒng)TS是一個(gè)六元組，其中，S是狀態(tài)集合，S0∈S是非空的初始狀態(tài)，I是輸入事件序列，AP是狀態(tài)標(biāo)簽，L：S→φ(AP)是標(biāo)簽函數(shù)，將一組狀態(tài)與一組標(biāo)簽進(jìn)行關(guān)聯(lián)，→∈S×I×S是系統(tǒng)中從一個(gè)動(dòng)作的輸入到下一個(gè)狀態(tài)的遷移關(guān)系.

定義4.將遷移系統(tǒng)的可達(dá)性描述為：如果在遷移系統(tǒng)TS中，對(duì)于輸入符號(hào)序列δ=i1i2i3…，存在一個(gè)有限的執(zhí)行序列rδ=s0i0s1i1s2…iks′，則可以定義狀態(tài)s′是可達(dá)的.

兩個(gè)遷移系統(tǒng)的組合為TS1‖TS2，其狀態(tài)集合為笛卡爾積S1×S2.首先給出兩個(gè)TS：

TS1=〈S1，S0，1，I1，→1，AP1，L1〉TS2=〈S2，S0，2，I2，→2，AP2，L2〉

具體的組合方法與遷移系統(tǒng)的遷移條件→1·2相關(guān).依據(jù)不同語義，具體分為如下3種組合方式：

·同步組合(synchronous composition)：同步組合要求遷移系統(tǒng)僅當(dāng)TS1和TS2在有一致的輸入符號(hào)時(shí)才進(jìn)行遷移.在該語義下，如圖2所示，將TS1與TS2的同步組合表示為TS1∩TS2=TS1∩2，計(jì)算過程為：

圖2 組件的組合語義

TS1∩2=

其中：

·S1∩2=S1×S2；S0，1∩2=S0，1×S0，2；

·I1∩2=I1∪I2；AP1∩2=AP1∪AP2；

·L1∩2()=L1(S1)∪L2(S2)；

·<，i，>∈→1∩2；

并且滿足如下條件：

∈→1，∈→2；

·并發(fā)組合(parallel composition)：并發(fā)組合規(guī)則要求遷移系統(tǒng)僅當(dāng)TS1和TS2在有一致的遷移動(dòng)作時(shí)進(jìn)行遷移.如圖2中TSsr‖TSpsp，在該組合語義下，TS1與TS2的同步組合表示為：TS1‖TS2=TS1‖2，計(jì)算過程為：

TS1‖2=，其中：

·S1‖2=S1×S2；S0，1‖2=S0，1×S0，2；

·I1‖2=I1∪I2；AP1‖2=AP1∪AP2；

·L1‖2()=L1(S1)∪L2(S2)；

·<，i，>∈→1‖2；

并且滿足如下條件：

1)i∈I1∩I2，∈→1，∈→2(TS1與TS2均進(jìn)行遷移，輸入符號(hào)被雙方接收)；

2)i∈I1I2，∈→1，s2=s2′(只有TS1進(jìn)行遷移，輸入符號(hào)只有TS1接收)；

3)i∈I2I1，∈→2，s1=s1′(只有TS2進(jìn)行遷移，輸入符號(hào)只有TS2接收).

·信道組合(channel composition)：具有通信語義的遷移系統(tǒng)表示為，其中C是一組進(jìn)行數(shù)據(jù)傳輸?shù)耐ㄐ判诺?系統(tǒng)在信道組合語義下，不僅在TS1和TS2有相同輸入/輸出的情況下進(jìn)行狀態(tài)遷移，同時(shí)也在有消息發(fā)送(c!)和接收(c?)的過程時(shí)進(jìn)行遷移.則有：→∈S×(I∪C!∪C?)×S，其中，c!屬于集合{c!| c∈C}，以及c?屬于集合{c?|c∈C}，信道組合如圖2中組件a┥┝b┥┝c的組合過程.針對(duì)具有通信語義的遷移系統(tǒng)可以描述為：

TS1=〈S1，S0，1，I1，C，→1，AP1，L1〉TS2=〈S2，S0，2，I2，C，→2，AP2，L2〉

其組合模型為TS1┥┝TS2為：

TS1┥┝2=

其中：

·S1┥┝2=S1×S2；S0，1┥┝2=S0，1×S0，2；

·I1┥┝2=I1∪I2；AP1┥┝2=AP1∪AP2；

·L1┥┝2()=L1(S1)∪L2(S2)；

·<，i，>∈→1┥┝2；

同時(shí)需要滿足如下條件：

1)i∈I1，→1(S2=S2′)；

2)i∈I2，→2(S1=S1′)；

3)∈→1，∈→2′，其中i=ε，

或：

4)∈→1，∈→2′，其中i=ε

本文羅列了上述3種典型的組件組合操作方法，通過3種不同語義對(duì)組件的行為進(jìn)行組合.這也是基于組件化軟件開發(fā)的基礎(chǔ).

2.3 組件的可組合性

對(duì)組件行為進(jìn)行抽象并給出抽象后組件的組合方法，可以對(duì)系統(tǒng)的整體行為進(jìn)行描述.在此基礎(chǔ)上，需要給出判定規(guī)則描述何種條件下組件是可組合的.當(dāng)前，相關(guān)研究小組相繼提出一些形式化方法用于建模系統(tǒng)的交互行為，并驗(yàn)證組件的可組合性.典型的，Lynch提出I/O自動(dòng)機(jī)模型[9]，通過建模組件的接口行為來分析交互過程.接口自動(dòng)機(jī)是另一種顯示表達(dá)組件接口時(shí)序行為的形式化模型[10]，對(duì)外部環(huán)境行為進(jìn)行定義，在一定程度上可以被看做接口模型，而IO自動(dòng)機(jī)類比看作是組件模型.繼而，Alur與Lynch等將時(shí)間語義加入到自動(dòng)機(jī)模型中，提出了時(shí)間自動(dòng)機(jī)[11]、時(shí)間I/O自動(dòng)機(jī)等模型.

·一組狀態(tài)集合，也可以表示為StS；

·一組簽名(動(dòng)作)sig(A)，也可以表示為ΣS；

·step(A)?states(A)×acts(sig(A))×states(A)，描述對(duì)于給定的某個(gè)狀態(tài)a，對(duì)于輸入事件π，系統(tǒng)將產(chǎn)生遷移(a，π，a′) ，也可以表示為→S.

對(duì)于具有可兼容性的自動(dòng)機(jī)Ai：i∈I，其構(gòu)成組合后的自動(dòng)機(jī)A=∏i∈IAi為：

states(A)=∏i∈Istates(Ai)；start(A)=∏i∈Istart(Ai)；

sig(A)=∏i∈Isig(Ai)；part(A)=∪i∈Ipart(Ai)；

I/O自動(dòng)機(jī)的可組合性描述為：在組件具有兼容性的前提下，組合后形成的整體模型中，組件的原有屬性保持不變.在組合時(shí)，可通過組件的笛卡爾積(product)進(jìn)行計(jì)算.

·VP是一組狀態(tài)集合；

·τP?VP×AP×VP是一組遷移過程.

定義9.接口自動(dòng)機(jī)P和Q是可兼容的，當(dāng)條件成立：

定義10.接口自動(dòng)機(jī)P和Q的笛卡爾積(product)為P?Q：

·VP?Q=VP×VQ

接口自動(dòng)機(jī)的組件P和Q在可兼容的前提下，當(dāng)如下條件滿足時(shí)，則組件是可組合的：對(duì)于P?Q，存在一個(gè)合法的環(huán)境E使得illegal(P，Q)×VE在(P?Q)?E系統(tǒng)中，非法狀態(tài)illegal(P，Q)不可達(dá)的.

3 組件的時(shí)間行為建模與驗(yàn)證

前面給出了基于遷移系統(tǒng)的組件組合操作方法用于建模系統(tǒng)的整體行為.在此基礎(chǔ)上，需要給出組件行為可組合性的形式化定義，以此指導(dǎo)對(duì)組件可組合性的驗(yàn)證.本節(jié)將對(duì)組件行為可組合的形式化定義進(jìn)行闡述與歸納.

3.1 時(shí)間行為的可組合

可組合性是組件化軟件重要的性質(zhì)之一，描述了組件之間行為的兼容能力.傳統(tǒng)的CBD方法更多關(guān)注組件接口值域的可組合性，描述了兩個(gè)組件在組合時(shí)，需要滿足兩個(gè)組件接口的值域要求.如圖3的例子中，組件P1的輸入值x和y，同時(shí)對(duì)其輸入進(jìn)行約束，要求當(dāng)x=0時(shí)，y值也需要等于0，以此產(chǎn)生z值.而在x不等于0時(shí)，則對(duì)y值無限制.本文給出兩個(gè)組件的組合行為P1||P2，為了滿足整體的輸入條件，組合后給出的約束條件為x≠0，以此保證z值的正確輸出.組合過程也可以看作是對(duì)值約束行為的一種精化.

圖3 約束行為的組合

針對(duì)組件的可組合性，Baldovin在其博士論文中從兩個(gè)角度給出了較為普適的定義[17].其一描述了組件的個(gè)體功能在組合后的保持性，定義為組件的組合性(compositionality)，是一種基于自底向上(bottom-up)的視角對(duì)組件化軟件的解決方案.其二描述了組件在組合后的整體行為是否能夠滿足系統(tǒng)的功能要求，描述為組件的可組合性(composability)，可以看作是一種自頂向下(top-down)的解決方案.該定義給出了組件化軟件可組合的通用性描述，具有普適性.但針對(duì)CPS中組件的可組合性，考量的不僅僅是功能屬性，更重要的是系統(tǒng)的非功能屬性(時(shí)間行為，功耗等).需要在非功能屬性上給出更為細(xì)粒度的定義，描述特定屬性的可組合性.Edward Lee在文獻(xiàn)中提出可組合性具有層次化、異構(gòu)性的特征[18]，其關(guān)注于信息物理系統(tǒng)中多種計(jì)算模型(Model of Computation，MOC)的組合，如數(shù)據(jù)流模型/進(jìn)程代數(shù)模型/同步反應(yīng)模型等模型組合.其研究小組設(shè)計(jì)并實(shí)現(xiàn)了仿真建模工具Ptolemy，針對(duì)每種模型給出其行為類型系統(tǒng)用以驗(yàn)證各模型之間的可組合性.Kopetz在文獻(xiàn)中定義組件的可組合性是其行為的可保持性[19]，即，在組件組合前后，組件的個(gè)體功能保持不變.基于該定義，Kopetz給出了系統(tǒng)中架構(gòu)可組合的形式化描述：“子系統(tǒng)(sub-system)所具有的屬性，在系統(tǒng)組合之后，該屬性仍然得到保持，則系統(tǒng)的架構(gòu)是可組合的”.本文在表1中羅列了幾個(gè)典型的組件時(shí)間行為可組合的定義.

表1 典型的組件可組合形式化定義

另一個(gè)重要的研究工作是賓夕法尼亞大學(xué)Insup Lee小組的相關(guān)工作[20-22].主要關(guān)注實(shí)時(shí)嵌入式系統(tǒng)的層次化可調(diào)度、可組合的問題.在該工作中描述組件具有層次化的特性，系統(tǒng)可以看作分區(qū)(partitioned)的架構(gòu).因此，該模型下的可組合問題演變?yōu)椋菏紫冉€(gè)體組件的時(shí)間行為模型，然后通過全局調(diào)度器對(duì)組件之間的時(shí)間需求進(jìn)行可組合(可滿足)驗(yàn)證.基于此，通過增量式(incremental)的開發(fā)方法進(jìn)行具體實(shí)現(xiàn).清華大學(xué)的王博對(duì)嵌入式可組合軟件進(jìn)行了闡述[23]，描述可組合具有廣義和狹義的概念，并分析嵌入式可組合軟件應(yīng)具備的特征.其次，為了從執(zhí)行語義上對(duì)時(shí)間行為的可組合性進(jìn)行分析，Henzinger等人基于邏輯執(zhí)行時(shí)間編程模型(Logical Execution Time，LET)[24]定義了Giotto編程語言，并給出了針對(duì)分布式系統(tǒng)的、具有時(shí)間行為可組合性的編程方法.在開發(fā)過程中，將分布式節(jié)點(diǎn)看做資源提供者(Supplier)，并通過功能的集成(Integrator)對(duì)系統(tǒng)進(jìn)行設(shè)計(jì)實(shí)現(xiàn).其針對(duì)分布式環(huán)境下時(shí)間行為的可組合性，給出兩方面描述：1)接口兼容性(interface compatible)：描述了在分布式環(huán)境下，分配至某節(jié)點(diǎn)的功能模塊Ps，h可以在其提供者S的時(shí)間接口Ts，h內(nèi)執(zhí)行完成；2)時(shí)間安全性(time-safety)：滿足如下條件時(shí)，功能模塊Ps，h是安全的：①讀取某任務(wù)輸出端口的時(shí)間點(diǎn)(或總線消息)不早于任務(wù)計(jì)算的時(shí)間(或傳輸)；②寫入任務(wù)端口的時(shí)間點(diǎn)(或傳輸)不晚于任務(wù)開始執(zhí)行的時(shí)間.

近些年，工業(yè)界同樣受惠于模型驅(qū)動(dòng)開發(fā)的方法優(yōu)勢(shì).典型的如針對(duì)汽車電子系統(tǒng)進(jìn)行建模開發(fā)的EAST-ADL方法，其基于Autosar架構(gòu)建立整車的需求模型[25]，并逐步分解為子系統(tǒng)需求，并通過sysML語言對(duì)各子系統(tǒng)進(jìn)行模型的設(shè)計(jì)與實(shí)現(xiàn).再如早期針對(duì)航空領(lǐng)域進(jìn)行模型定義的AADL建模語言[26]，其從建模工具到分析工具都逐漸變得成熟，若干工作已經(jīng)將其應(yīng)用于無線通信或機(jī)器人等領(lǐng)域.在AADL中定義組件/包/子系統(tǒng)等系統(tǒng)元素，并通過連接器等方式對(duì)系統(tǒng)進(jìn)行組合行為的配置.Bardaro等人[27]給出了基于AADL對(duì)ROS機(jī)器人進(jìn)行實(shí)現(xiàn)的開發(fā)方法.Li等人[28]給出AADL轉(zhuǎn)換為時(shí)間自動(dòng)機(jī)的方法，并給出規(guī)則用于驗(yàn)證模型的可組合性.

3.2 組件模型

當(dāng)前，已有相關(guān)研究提出多種組件模型來對(duì)系統(tǒng)行為進(jìn)行建模及分析.本小節(jié)分別概述幾種典型的系統(tǒng)模型，包括，基本組件模型、組件之間的交互行為BIP模型、接口事件模型及框架模型等.

3.2.1 基本組件模型

Kopetz給出分布式實(shí)時(shí)系統(tǒng)中組件的概念性描述[29]，根據(jù)不同場(chǎng)景，將組件分為閉合組件(close component)與開放組件(open component).通過接口與外部進(jìn)行通信，具體定義了4種接口：服務(wù)提供、服務(wù)請(qǐng)求、配置計(jì)劃以及診斷與管理接口.同時(shí)定義任務(wù)、狀態(tài)、報(bào)文、節(jié)點(diǎn)以及簇等基本系統(tǒng)元素，并通過Linking Interface[30]描述其可組合性.Joseph Sifakis研究小組的相關(guān)工作[31-33]定義了系統(tǒng)的抽象模型BIP(Behavior Interaction Priority，BIP)，具體為：行為模型(Behavioral Model)：組件個(gè)體的行為，不因環(huán)境的上下文而改變，提供給環(huán)境的保證(guarantee)及對(duì)環(huán)境的期望(assumption).交互模型(Interaction Model)：組件之間的通信行為，具體描述了系統(tǒng)在架構(gòu)上的約束，通?？捎梢唤M連接器(Connector)及相關(guān)屬性進(jìn)行建模；優(yōu)先級(jí)(Priority)：用于建模交互行為中的優(yōu)先關(guān)系.該模型較好的從頂層給出系統(tǒng)行為語義，抽象了系統(tǒng)的結(jié)構(gòu)與行為.在該描述下，組件的基本概念定義為：

定義11.原子組件(Atomic Component)包含如下元素[32]：

·一組端口p={p1，p2，…，pn}，端口的名字描述與其它組件的同步事件行為；

·S={s1，s2，…，sn}是組件的狀態(tài)集合；

·本地的數(shù)據(jù)變量V；

·執(zhí)行原子操作的遷移過程(s1，p，gp，fp，s2).

圖4是一個(gè)原子組件結(jié)構(gòu)，包括兩個(gè)端口in和out，變量x，y，和狀態(tài)empty以及full.在狀態(tài)empty中，接收到同步事件empty后，當(dāng)守衛(wèi)條件0

圖4 原子組件的結(jié)構(gòu)

3.2.2 接口事件模型

為了建模組件接口的多種行為，Thiele等人[34]給出一種抽象-自適應(yīng)接口(adaptive interface)模型用于描述組件的接口行為，同時(shí)，給出了支持組件獨(dú)立設(shè)計(jì)、增量式開發(fā)的組合規(guī)則.文中將接口行為劃分為4種類型(周期、偶發(fā)、抖動(dòng)及突發(fā)的)：

假設(shè)組件A與B存在交互(A?B)，組件A輸出周期為T1(抖動(dòng)為J1)的周期性事件，組件B的輸入事件為最小到達(dá)間隔時(shí)間為T2的偶發(fā)性事件，兩個(gè)組件的輸出輸入行為在時(shí)間語義上不一致.如圖5所示，文獻(xiàn)中通過“構(gòu)造”事件的相關(guān)行為來對(duì)接口事件的可組合性進(jìn)行建模及分析.如上述示例中，通過T2=T1-J1構(gòu)造兩者之間關(guān)系.

圖5 接口事件之間的轉(zhuǎn)換關(guān)系

Richter等人[35]也給出接口模型用于描述組件的接口行為.具體將組件抽象為(X，Y，T，ψ)，其中X為輸入行為，Y為輸出行為，T是計(jì)算函數(shù)，Y=T(X)，ψ(X)是對(duì)輸入行為的約束.則兩個(gè)接口G與H進(jìn)行組合時(shí)，當(dāng)滿足如下條件時(shí)，接口是可組合的：

上述關(guān)系描述了當(dāng)兩個(gè)組件在組合時(shí)，接口的保證(Guarantee)可以滿足另一組件接口的假設(shè)(Assumption)，則接口是可組合的，該文工作從接口事件行為的角度進(jìn)行建模，給出接口可組合的通用規(guī)則.

3.2.3 系統(tǒng)框架模型

最為典型的系統(tǒng)模型如liu在文獻(xiàn)中給出的實(shí)時(shí)系統(tǒng)模型[36]，系統(tǒng)由任務(wù)模型task，資源模型resource，以及調(diào)度模型scheduler組成.具體將系統(tǒng)建模為：通過調(diào)度器的調(diào)度方法在資源上對(duì)任務(wù)進(jìn)行執(zhí)行.基于此基礎(chǔ)，文獻(xiàn)[37]給出了一個(gè)分布式實(shí)時(shí)系統(tǒng)下的系統(tǒng)模型，具體包括如下元素：任務(wù)task，調(diào)度策略scheduler，計(jì)時(shí)定時(shí)器timer及用于任務(wù)間通信的信道channel，給出了組件可組合的規(guī)則定義，并通過UPPAAL工具[38]進(jìn)行建模及驗(yàn)證.文中定義：當(dāng)所有實(shí)時(shí)任務(wù)是可調(diào)度的，則組件是可組合的.基于時(shí)間計(jì)算樹邏輯(Timed Computation Tree Logical，TCTL)給出了可組合性的驗(yàn)證查詢語句：

E<> Task.executing

3.3 時(shí)間行為確定的編程模型

編程模型描述了程序執(zhí)行的行為抽象.在傳統(tǒng)的基于進(jìn)程/線程理論的編程模型中，進(jìn)程作為系統(tǒng)調(diào)度的執(zhí)行單元，通過協(xié)調(diào)線程流完成任務(wù)的執(zhí)行.進(jìn)程/線程模型從多任務(wù)的角度描述任務(wù)的并發(fā)行為，可以高效的對(duì)多任務(wù)系統(tǒng)進(jìn)行調(diào)度.但固有的優(yōu)先級(jí)搶占等機(jī)制，使得正在執(zhí)行的任務(wù)易被搶占導(dǎo)致執(zhí)行時(shí)間變得不確定(輸入、輸出行為的抖動(dòng)).因此，在進(jìn)程/線程的編程范式下，CPS中組件的任務(wù)執(zhí)行行為變得不確定，對(duì)組件的時(shí)間行為可組合判定變得困難.

為了使任務(wù)的時(shí)間行為變的確定，相關(guān)研究提出了不同的編程范式以提高系統(tǒng)響應(yīng)時(shí)間的可預(yù)測(cè)性[39].典型的編程模型有物理執(zhí)行時(shí)間模型(Physical Execution Time，PET)、有界執(zhí)行時(shí)間模型(Bounded Execution Time，BET)、零執(zhí)行時(shí)間模型(Zero Execution Time，ZET)以及邏輯執(zhí)行時(shí)間模型(Logical Execution Time，LET)等，從不同執(zhí)行行為角度對(duì)時(shí)間屬性進(jìn)行限定.

3.3.1 物理執(zhí)行時(shí)間模型

PET模型被應(yīng)用于早期簡(jiǎn)單的控制系統(tǒng)中，如單或多處理器架構(gòu)的控制系統(tǒng).類似系統(tǒng)的計(jì)算時(shí)間通常為常量并有準(zhǔn)確的I/O處理時(shí)延，由較低級(jí)的編程語言進(jìn)行實(shí)現(xiàn)，該類系統(tǒng)不具備并發(fā)性即多組件的協(xié)作能力.如圖6所示，任務(wù)在時(shí)間段[0，1]之間完成數(shù)據(jù)輸入，在之后的8個(gè)時(shí)間段完成任務(wù)的計(jì)算，并在時(shí)間段[9，10]完成任務(wù)結(jié)果的輸出.

圖 6 編程模型的邏輯語義及任務(wù)的真實(shí)調(diào)度執(zhí)行情況

PET模型適用于任務(wù)的執(zhí)行時(shí)間可確定的計(jì)算平臺(tái)，比如周期性任務(wù)執(zhí)行，其計(jì)算時(shí)間可確定，因此輸入輸出時(shí)間容易計(jì)算，并能夠獲得較高的吞吐量.但較為明顯的缺點(diǎn)是缺少可組合性，即當(dāng)系統(tǒng)復(fù)雜性逐步增加時(shí)，如何集成化的開發(fā)整體系統(tǒng)變得困難，甚至在早期多個(gè)PET組件之間通信過程的傳輸時(shí)間、延遲時(shí)間等都較難計(jì)算.

3.3.2 有界執(zhí)行時(shí)間模型

隨著底層硬件架構(gòu)處理能力的增強(qiáng)，針對(duì)實(shí)時(shí)嵌入式系統(tǒng)的多任務(wù)應(yīng)用隨之增多.同時(shí)，需要準(zhǔn)確的度量多任務(wù)環(huán)境下任務(wù)的執(zhí)行時(shí)間以保證任務(wù)計(jì)算結(jié)果可以在截止時(shí)間之前完成輸出.有界執(zhí)行時(shí)間BET模型從多任務(wù)的場(chǎng)景出發(fā)，定義有界執(zhí)行時(shí)間為其任務(wù)的執(zhí)行周期，因此在實(shí)現(xiàn)中，能夠保證任務(wù)的“輸入-計(jì)算-輸出”能夠在有界執(zhí)行時(shí)間BET之內(nèi)完成，即能夠保證多任務(wù)系統(tǒng)的正確性及實(shí)時(shí)性.如圖6中任務(wù)的執(zhí)行片段，任務(wù)的周期為10個(gè)時(shí)間單元，在時(shí)間段[0，1]過程中，由于有高優(yōu)先級(jí)任務(wù)在運(yùn)行，則任務(wù)等待至[1，2]期間進(jìn)行任務(wù)的輸入，之后在[3，4]時(shí)間段執(zhí)行任務(wù)的計(jì)算，在[5，7]被其他任務(wù)搶占，并繼而在[6，8]期間完成任務(wù)的計(jì)算并輸出，同樣，在時(shí)間段[10，20]期間進(jìn)行了另一個(gè)周期的任務(wù)執(zhí)行.

有界執(zhí)行時(shí)間模型可以保證任務(wù)執(zhí)行的實(shí)時(shí)性，典型的如基于傳統(tǒng)的RM/EDF調(diào)度方法，并利用WCET分析工具進(jìn)行多任務(wù)的可調(diào)度性分析，以判定是否滿足時(shí)限要求.但從執(zhí)行過程來看，該模型仍然缺乏可組合性.

3.3.3 邏輯零執(zhí)行時(shí)間模型

為了增強(qiáng)組件的可組合性，相關(guān)研究試圖關(guān)注組件的輸入與輸出行為，為了加強(qiáng)并保證組件是輸入確定的(input-determined)，即：對(duì)于給定的任務(wù)輸入序列，可以確保有相同的計(jì)算結(jié)果的輸出(結(jié)果與時(shí)間)，某種程度上也將該類系統(tǒng)稱為“同步反應(yīng)式系統(tǒng)(Synchronous Reactive Systems)”.模型基于“同步假設(shè)(Synchronous Assumption)”，其中同步描述任務(wù)的輸入與輸出是同步的，任務(wù)的輸入-計(jì)算-輸出時(shí)間在模型角度可看作零時(shí)間.

該模型下，可以有效的保證系統(tǒng)的輸入輸出的實(shí)時(shí)性，在一定程度上對(duì)系統(tǒng)的可組合性進(jìn)行了基礎(chǔ)性的保證.但該模型從“同步假設(shè)”的角度出發(fā)，在實(shí)際操作中，任務(wù)的輸入/計(jì)算/輸出時(shí)間不能保證在零時(shí)刻內(nèi)完成，因此，需要通過語言結(jié)構(gòu)、編譯器支持進(jìn)行同步假設(shè)的實(shí)現(xiàn).在簡(jiǎn)單的任務(wù)環(huán)境下，可以正確的實(shí)現(xiàn)模型的語義，但在復(fù)雜的環(huán)境下的一些技術(shù)問題，如分布式環(huán)境下的通信行為、節(jié)點(diǎn)時(shí)鐘同步等，都給ZET模型的應(yīng)用帶來難度.

3.3.4 邏輯執(zhí)行時(shí)間模型

實(shí)時(shí)控制系統(tǒng)與物理系統(tǒng)相交互，其I/O行為尤為重要.同樣，出于考量系統(tǒng)I/O行為的時(shí)間屬性的目的，學(xué)術(shù)界提出邏輯執(zhí)行時(shí)間模型LET對(duì)任務(wù)的時(shí)間屬性進(jìn)行抽象.其中任務(wù)的輸入與輸出是在特定的時(shí)間點(diǎn)進(jìn)行完成.如圖6示例中，任務(wù)在[1，2][11，12]時(shí)間段進(jìn)行數(shù)據(jù)的輸入，在[2，8][12，18]間進(jìn)行任務(wù)的執(zhí)行，并在[8，9][18，19]時(shí)間段進(jìn)行任務(wù)的輸出.與其它編程模型最大的區(qū)別在于，LET編程模型中任務(wù)的輸入輸出是有時(shí)間要求的、是確定的.即使任務(wù)過早的計(jì)算完成也并未執(zhí)行數(shù)據(jù)的輸出，而是等待輸出時(shí)間點(diǎn)到達(dá)后再進(jìn)行輸出.LET模型通過時(shí)間的確定，強(qiáng)化了輸入輸出行為的可組合性.

3.4 組件的精化

如前所述，一些增加時(shí)間語義的典型形式化方法(如時(shí)間自動(dòng)機(jī)、時(shí)間Petri網(wǎng)、Event-B等[40])均已被應(yīng)用于CPS的建模與精化.本節(jié)將對(duì)精化部分進(jìn)行闡述.

組件化開發(fā)方法中的精化(Refinement)過程描述了系統(tǒng)的需求規(guī)約(specification)與系統(tǒng)實(shí)現(xiàn)(implementation)之間的轉(zhuǎn)換過程.在對(duì)兩個(gè)模型之間是否存在精化關(guān)系進(jìn)行判定時(shí)，典型的如使用替代模擬(alternating simulation)的方法[41]進(jìn)行檢查.該方法中，在對(duì)輸入有條件限制的情況下，如果最終實(shí)現(xiàn)模型允許輸入的集合是規(guī)約需求中所定義集合的子集，則實(shí)現(xiàn)模型將被用于較小的環(huán)境或范圍中.可描述為，組件P精化了組件Q，則Q的輸入可以被P所模擬，而對(duì)于P的輸出可以被Q所模擬，保證了精化后的組件可以在更多的外部環(huán)境中使用.

定義12.替代模擬(alternating simulation)[41]：對(duì)于系統(tǒng)的需求規(guī)約S=(StS，S0，Σ，→S)精化了規(guī)約T=(StT，T0，Σ，→T)，可以表示為S?T，且存在二項(xiàng)關(guān)系R?StS×StT，并有(s0，t0)，并且存在狀態(tài)集合(s，t)∈R，并且滿足如下的條件：

定義13.精化關(guān)系[41]：當(dāng)規(guī)約P和Q之間存在關(guān)系P?Q時(shí)，表明兩者具有精化關(guān)系.

為了說明精化過程的具體實(shí)現(xiàn)，如圖7示例，machine-2在兩個(gè)方面對(duì)machine-1進(jìn)行精化實(shí)現(xiàn).其一，machine-1中從狀態(tài)s2遷移至s1的條件為tea!，在machine-2的具體實(shí)現(xiàn)中，舍棄了對(duì)tea!事件的處理，即，精化后的實(shí)現(xiàn)模型具有更少的行為輸出；其二，在狀態(tài)S2上進(jìn)行了不變量的緊致操作，將y≤6變?yōu)閥≤5.通過可達(dá)性分析得出，在輸入動(dòng)作上，machine-2可以模擬machine-1，而在輸出動(dòng)作上則具有相反的特征.

圖7 糖果機(jī)示例的一種精化關(guān)系實(shí)現(xiàn)

另一種精化檢查的方法是通過前向或后向模擬[42]來建立具體模型和抽象模型之間的關(guān)系.如果能夠推導(dǎo)出精化后具體模型中狀態(tài)與抽象模型中狀態(tài)存在一定的二元關(guān)系，事件也存在一定的二元關(guān)系，則可以稱兩者之間是存在精化關(guān)系的.形式化描述為如下：

r∈T?S

其中，r是二元關(guān)系，具體模型中狀態(tài)及事件集合為T，抽象模型中狀態(tài)及事件的集合為S.

模型檢查中典型的難點(diǎn)是狀態(tài)爆炸問題，在對(duì)精化關(guān)系進(jìn)行檢查時(shí)，更多采用組合精化的方法以避免狀態(tài)爆炸問題.其含義為，為了檢查組件的組合行為Q1‖Q2‖…‖Qn精化P1‖P2‖…‖Pn，只需要分別驗(yàn)證Q1精化了P1，Q2，精化了P2…Qn精化了Pn即可.也就是將組合后的精化檢驗(yàn)分解成多個(gè)獨(dú)立的精化檢驗(yàn)過程，減少空間的搜索.如下為基本模式：

4 面臨的挑戰(zhàn)與研究展望

組件的時(shí)間行為可組合問題已經(jīng)得到了廣泛的關(guān)注并取得了一系列研究成果，但仍然存在一些具有挑戰(zhàn)性的問題亟待進(jìn)一步解決.從組件化軟件開發(fā)的角度來看，首先需要建立頂層的時(shí)間行為需求模型，并將需求模型逐步轉(zhuǎn)化為底層的具體實(shí)現(xiàn).因此，如何建立上層的時(shí)間需求模型，上層的需求模型(如端到端的時(shí)間約束)如何逐步分解、轉(zhuǎn)化為實(shí)現(xiàn)層的任務(wù)級(jí)時(shí)間約束(任務(wù)的周期、截止時(shí)間等)，并在分解為各組件之后，如何分析、驗(yàn)證多個(gè)組件(子系統(tǒng))之間的時(shí)間行為是可組合的，仍然是CPS開發(fā)過程中的核心問題.具體的，相關(guān)的挑戰(zhàn)如下：

1)組件時(shí)間行為可組合的形式化定義

組件可組合性相關(guān)研究的基礎(chǔ)在于對(duì)可組合性的形式化定義，從而可以明確需要具備可組合性的屬性、含義以及度量方法等.只有在此基礎(chǔ)上，才能有針對(duì)性的提高組件的可組合性.在現(xiàn)有的組件可組合的形式化定義中，最為基本的定義是從組件的行為角度出發(fā)，描述組件在組合之后，如果各組件原有的行為不受影響，則組件是可組合的.該廣義的定義指導(dǎo)了最初的組件化軟件的設(shè)計(jì)及組合操作的實(shí)現(xiàn).但針對(duì)于具有安全攸關(guān)的CPS(無人駕駛、智能制造等)，其行為變得復(fù)雜，類似系統(tǒng)中組件行為的可組合需要保證任務(wù)調(diào)度、執(zhí)行時(shí)間、執(zhí)行順序等行為在組合前后的一致性.因此，與傳統(tǒng)的組件化軟件的可組合定義相比，如何更為進(jìn)一步明確的給出組件在時(shí)間行為可組合的形式化定義，是亟待解決的核心關(guān)鍵點(diǎn).

2)組件的時(shí)間行為可組合驗(yàn)證

在組件化開發(fā)框架中，需要通過形式化的方法和工具對(duì)組件的可組合性進(jìn)行驗(yàn)證(verification).在現(xiàn)有的工作中，典型的形式化分析工具，如時(shí)間自動(dòng)機(jī)、Petri網(wǎng)、B語言、Z語言等已被廣泛應(yīng)用.同時(shí)也有相應(yīng)工具的擴(kuò)展，如時(shí)間接口自動(dòng)機(jī)、時(shí)間petri網(wǎng)等，都從不同的角度對(duì)系統(tǒng)行為進(jìn)行建模.然而在已有的工作中，相應(yīng)的形式化方法仍然不夠完備.典型的如自動(dòng)機(jī)理論中的狀態(tài)爆炸問題，雖然可以通過層次化的思想對(duì)問題進(jìn)行解決，但在具體的工業(yè)應(yīng)用領(lǐng)域場(chǎng)景下，仍然存在語義轉(zhuǎn)換的復(fù)雜性、一致性等問題.因此，如何選擇適合的形式化工具(自動(dòng)機(jī)/Petri網(wǎng)/B語言等)對(duì)組件內(nèi)部的時(shí)間行為進(jìn)行建模，繼而對(duì)系統(tǒng)整體的時(shí)間行為進(jìn)行驗(yàn)證.也是系統(tǒng)中時(shí)間行為可組合問題的主要挑戰(zhàn).

3)運(yùn)行時(shí)系統(tǒng)在組件時(shí)間可組合性上的支持

組件的可組合性是一個(gè)關(guān)鍵的、核心的軟件工程理論問題.其中，可組合性問題也涉及到計(jì)算機(jī)軟硬件架構(gòu)多方面的技術(shù)定義與實(shí)現(xiàn).比如改造或重構(gòu)現(xiàn)有底層架構(gòu)使其增加時(shí)間語義，優(yōu)化現(xiàn)有實(shí)時(shí)調(diào)度方法(RM/EDF等)，甚至在編程語言中增加時(shí)間屬性等調(diào)整，類似對(duì)系統(tǒng)架構(gòu)進(jìn)行的優(yōu)化，均影響到組件執(zhí)行的時(shí)間屬性，甚至提升組件時(shí)間行為的可組合性.現(xiàn)今，相關(guān)工作給出若干方案，但仍然缺少完整的、具有時(shí)間語義的軟硬件架構(gòu)的支撐.

應(yīng)對(duì)上述挑戰(zhàn)，信息物理系統(tǒng)下組件化軟件的可組合性問題研究可以從以下幾個(gè)方面進(jìn)行展開：

1)系統(tǒng)中時(shí)間行為可組合定義

已有的組件時(shí)間可組合的形式化定義均從組件組合行為的本質(zhì)出發(fā)，描述當(dāng)組件之間的時(shí)間行為彼此不干擾時(shí)，則組件是時(shí)間可組合的.然而對(duì)于安全攸關(guān)的信息物理系統(tǒng)而言，任務(wù)的執(zhí)行時(shí)間和任務(wù)執(zhí)行的順序關(guān)系均影響著系統(tǒng)的正確性.因此，對(duì)系統(tǒng)中組件的時(shí)間和順序行為進(jìn)行建模及分析，能夠準(zhǔn)確刻畫系統(tǒng)的時(shí)間行為，保證系統(tǒng)的正確性.比如在MARTE/CCSL建模語言中[43-45]，通過邏輯時(shí)鐘建模了系統(tǒng)的時(shí)序行為，并驗(yàn)證多個(gè)層次上的時(shí)序行為的可組合性.但從該角度出發(fā)，如何從需求模型逐步精化到實(shí)現(xiàn)模型，仍然需要大量工作的開展.

2)具有精化與組合語義的形式化驗(yàn)證

在模型驅(qū)動(dòng)開發(fā)過程中，首先建立需求規(guī)約模型(specification)，并據(jù)此需求模型對(duì)系統(tǒng)進(jìn)行逐步精化.在精化過程中，可以對(duì)復(fù)雜系統(tǒng)進(jìn)行分解(decomposition)[46].并在后續(xù)開發(fā)過程中，再將分解后的子系統(tǒng)進(jìn)行組合，并驗(yàn)證多個(gè)子系統(tǒng)組合后的行為是否與最初的規(guī)約一致.現(xiàn)有的形式化方法中，自動(dòng)機(jī)、Petri理論均被廣泛應(yīng)用于上述過程的建模，但相應(yīng)方法也有各自缺陷，如狀態(tài)爆炸[47]、多次轉(zhuǎn)換導(dǎo)致轉(zhuǎn)換效率下降等問題.同樣，類似B語言/Event-B語言等具有事件精化及組合本質(zhì)的形式化方法可以有效對(duì)系統(tǒng)行為進(jìn)行建模，建模語言本質(zhì)上的精化特質(zhì)更適合將上層的需求模型逐步轉(zhuǎn)化為系統(tǒng)實(shí)現(xiàn)模型.

3)支持任務(wù)時(shí)序行為可組合的運(yùn)行時(shí)系統(tǒng)

運(yùn)行時(shí)系統(tǒng)應(yīng)該能夠支持設(shè)計(jì)時(shí)的時(shí)序語義.同樣，實(shí)現(xiàn)具有時(shí)間可組合的信息物理系統(tǒng)涉及到計(jì)算機(jī)整體架構(gòu)的各個(gè)層面(包括如，需求建模層—語言層—操作系統(tǒng)層—體系結(jié)構(gòu)層)，需要保證從設(shè)計(jì)時(shí)到運(yùn)行時(shí)的各個(gè)層次中時(shí)序行為的一致性.較為典型的工作，如文獻(xiàn)[48]重構(gòu)了操作系統(tǒng)內(nèi)核，將系統(tǒng)進(jìn)行了層次化(應(yīng)用/內(nèi)核/硬件平臺(tái))劃分，并提出層次之間應(yīng)彼此不干擾(Zero-disturbance)，以及操作系統(tǒng)應(yīng)該具有穩(wěn)定的時(shí)間行為(Steady timing behaviour)兩個(gè)設(shè)計(jì)準(zhǔn)則，并據(jù)此準(zhǔn)則實(shí)現(xiàn)了具有時(shí)間可組合的操作系統(tǒng)原型TiCOS(Time Composability OS).為了緩解現(xiàn)有調(diào)度方法導(dǎo)致組件時(shí)間行為的異常、以及面對(duì)減小輸入/輸出行為的抖動(dòng)的需求，項(xiàng)目組在前期面對(duì)相關(guān)挑戰(zhàn)進(jìn)行了若干嘗試，基于LET模型，提出了具有時(shí)間可預(yù)測(cè)的操作系統(tǒng)原型[49]及驗(yàn)證方法[50]，并基于FPGA實(shí)現(xiàn)了支持時(shí)間語義的硬件操作系統(tǒng)[51]，相關(guān)實(shí)驗(yàn)數(shù)據(jù)表明了方案有效降低任務(wù)輸入/輸出時(shí)間的抖動(dòng)，實(shí)時(shí)性能優(yōu)于傳統(tǒng)的體系結(jié)構(gòu)，也有效提升了系統(tǒng)中組件時(shí)間行為的可組合性.

5 結(jié) 論

組件的可組合性是組件化軟件的核心理論.尤其在針對(duì)復(fù)雜的信息物理系統(tǒng)的設(shè)計(jì)過程中，系統(tǒng)非功能屬性(時(shí)間、執(zhí)行順序[52]、功耗等)的可組合性顯得尤為重要.本文總結(jié)時(shí)間行為可組合的若干工作，重點(diǎn)闡述了可組合的形式化定義，以及為了提高組件時(shí)間行為可組合性所提出的幾種主流編程模型.在后續(xù)的工作中，將基于已有的理論基礎(chǔ)，繼續(xù)在可預(yù)測(cè)、可組合系統(tǒng)的設(shè)計(jì)及驗(yàn)證等方面進(jìn)行探索與嘗試，如編譯器中時(shí)間屬性的支持，以及提出更有價(jià)值的系統(tǒng)可組合框架等.