計算機科學2007Vol. 34No. 2實時構件合成的語義研究*)黃靖盧炎生徐麗萍(華中科技大學計算機科學與技術學院武 漢430074)摘要實時構件合成是實時應用系統(tǒng)中軟件合成的基礎,是實現軟件復用思想的軟件生產活動,其語義研究從實時構件的反射式語義模型、實時構件合成的適配性驗證和合咸構件的語義規(guī)約機制三個方面展開,規(guī)約為實時構件合成中的分析理論。關鍵詞實時構件 ,構件合成，構件語義The Semantical Research on Real-time Component CompositionHUANG Jing LU Yan Sheng XU Li-Ping(School of Computer Science & Technology, Huazhong University of Science & Technology, Wuhan 430074)Abstract The software composition in the real-time application system bases on the real-time component composition,which is productive activity of software for realizing the software reuse. In its semantic researches there are three as-pects: reflective semantic model of real-time component, adaptive estimation of real- time component composition andsemantic specification of compositive component, which can be deducted as the analytics of real-time component compo-sition.Keywords Realtime component, Component composition, Component semantics理論。1引言當前，軟構件(Software Component)技術日益成為軟件2實時構件的 反射式語義模型工程領域消除“軟件危機”、提高軟件開發(fā)效率和質量的主流實時構件的反射式語義模型(Real time Component Re-技術?；跇嫾能浖铣?2 ,則是應用該技術實踐軟件fletive Semnantic Model, RCRSM)是構件合成分析理論的基復用思想的軟件生產活動,構件合成是軟件合成的實現途徑。礎,是一種語義分析模型,為基于構件的軟件合成進行驗證服應用實時構件(Real-time Component)的組裝合成活動,也由務,即在軟構件合成的實際運作之前或進行當中,應用形式化此成為了- -種快速高效開發(fā)實時應用軟件的可行性方案。然的方法,來判斷各待合成的軟構件間的可適配性等相關合成而在實時領域軟件合成的實際工程中，下面這些問題是值得問題。它有效地規(guī)約了實時構件的功能屬性和時間約束特我們首先關注和考慮的:征,將構件語義分為外部連接接口和構件內部行為兩部分,并1)以往的構件及構件模型很好地規(guī)約了構件自身所應有以構件方法(method)作為最小構件語義規(guī)約單元，其模型可的功能屬性,但是缺乏對實時環(huán)境中實時構件所額外附有的簡單表述為:時間約束特征的語義描述機制,因而難以形成比較完整的實實時構件反射式語義模型::= (實時構件的語義模型,實時構件語義信息,作為其配置文件在構件實際合成之前進行時構件語義模型的元數據,實時構件反射語義);語義分析,避免不必要的合成失敗。實時構件的語義模型:: = (實時構件的外部接口連接規(guī)2)如何根據構件庫中實時構件的語義配置信息,事先分約 ,實時構件的內部行為語義規(guī)約)。析與判斷待合成的實時構件間是否具有語義上的適配性,即關于RCRSM模型的詳細介紹，可參考文[3]。語義上不適配的構件在實際工程中不可能合成，因而沒有必3實時構件合 成的適配性驗證要從構件庫中提取。3)由于實時構件自身的變化或演化,需要判別其在語義實時構件合成的適配性驗證,是在實時構件反射式語義上能否保持原有的適配性不變。模型RCRSM的基礎上,應用形式化方法,分析待合成的軟構4)工程中,構件合成之后所形成的大粒度實時構件所具件間是否滿足可適配性的問題。同時,此驗證方法構成了軟有的語義配置信息該如何規(guī)約推導,且其時間約束特征如何件合成的分析理論,服務于今后的構件演化[4]。獲取與驗證?；Z義模型RCRSM,軟構針對這些問題我們從實時構件的反射式語義模型[5]、實件間中國煤化工部接口間的一-致性問題。時構件合成的適配性驗證和合成構件的語義規(guī)約機制三個方這是YHC N M H G來與外界進行通信和交互面進行實時構件合成的語義研究,規(guī)約實時構件合成的分析的， 即一切構件服務提供功能或構件服務請求行為都是通過* )本文得到國防預研基金項目(10104010201)資助。黃靖博士研究生,主要 研究方向為軟件工程、分布式計算技術;盧炎生教授、博士生導師,主要研究方向為軟件工程、分布式計算技術、特種數據庫等;徐麗萍副教授， 主要研究方向為軟件工程分布式計算技術等。●10軟構件自身的外部接口來呈現的,因而對待合成的軟構件間即進程STEP1 = parameter- counter, 其字母表aSTEP1是否滿足可適配性的驗證,也就是對軟構件間外部接口-致={ parameter - counter };性的分析。step2. 對實時構件B的語義規(guī)約執(zhí)行參數導入隊列事件又由實時構件反射式語義模型RCRSM可知,構件的外parameter- counter,計算其外部連接接口中構件服務請求方部接口是以構件方法描述體為基本語義規(guī)約單位的，而實時法methodg_。的輸人參數個數Num. In ParameterB_ 。'和構件的方法描述體rtM包含方法的簽名signature(rtM)、方輸出參數個數Num Out Parametr. n' ,并得到輸人參數隊法的斷言predicate(rtM)、方法的實時約束特征feature( rtM)列Que - In Parameterg_ n'和輸出參數隊列Que Out Pa-等3個邏輯組成單元。那么,我們對軟構件間外部接口一致性的分析將以驗證構件方法描述體的適配性為基礎,并依次即進程STEP2 = parameter- counter, 其字母表aSTEP2從其3個邏輯組成單元展開。parameter- counter };為方便論述,我們先做如下假設。設有待合成的兩個實step3. if (Num In ParameterA_ .ou' = Num In - Parame-時構件,分別為構件A和構件B。在各自依據RCRSM模型terB_ m')and (Num Out ParameterA On' = Num _Out Pa-的規(guī)約描述中,構件A的服務提供端口AL Out 的第i個方法rametenB_ n')表示為methodA ou'(其中i為自然數) ,構件B的服務請求端then continue step4;口B.In的第j個方法表示為methodg. 。'(其中j為自然.else SKIP.數)。那么構件A與構件B能否通過構件A的服務提供端口即進程STEP3=step3事件,其字母表aSTEP3= { step3中的第i個方法methoda au' 和構件B的服務請求端口中的事件);第j個方法methode_ n'進行合成，在接下來的幾個小節(jié)中將step4.設自然數k=0; .分別討論其驗證過程,并介紹構件合成的有關定理及推論。while k的維數,并依次將實時特征名稱name和實時特征供方法method, _an' 的執(zhí)行前提pre .condition ou';并執(zhí)行斷言requirement導人各自的隊列結構。斷言結果事件predicate. post condition, 獲取其外部連接接定義9實時特征 名稱字母表aNAME,表示所有實時特口中構件服務提供方法methodh On' 的執(zhí)行結果post- .con-征名稱name的集合。ditiona .on'.以實時構件A與實時構件B的合成為例，下面給出FA即進程STEP1 = predicate pre condition I predicatepost_ condition,其字 母表aSTEP1= { predicate- pre- condi-stepl.對實時構件A的語義規(guī)約執(zhí)行實時特征描述導入tion, predicate- post .condition };隊列事件rtfeature .counter, 計算其外部連接接口中構件服step2.對實時構件B的語義規(guī)約執(zhí)行斷言前提事件務提供方法method_ ou' 實時特征描述體二元組);Sb' = Sa~Sb' ,那么有Componentwitim^→OrmAou十實時約束特征適配性的實時構件A和B,能夠通過進程6nmsBoi→ComponentwmimB→v ;同理, 3Sb°∈SB,其中SB為OnpMoui、OraM時實現語義規(guī)約上的連接及互操作。即證。實時構件B語義規(guī)約進程中所有跡的集合,使得6sor=推論2滿足外部接口語義規(guī)約可連接性的兩兩實時構[SB],且3Sc∈SC,其中sC為實時構件C語義規(guī)約進程中件,可實現構件合成。所有跡的集合,使得OaedCo = Sco ,因為6rMburw =6ucCon ,所以證明:由定理1及推論1可知,實時構件間的外部接口語跡Sb2能與跡Se連接,即(Sb-^(J>);Sc= Sb-^Sc,那么有義規(guī)約具有可連接性,則在構件語義規(guī)約層實時構件能通過Componentelim*- →OreyBou→GrMCMh - +Componentatimc→V.其外部接口中的某些端口,與其它軟構件系統(tǒng)所構成的外界那么,實時構件A和B.B和C能夠通過各自的進程GouM^a環(huán)境實現互連互通、交互協(xié)作。先設有三個實時構件A、B、和6rm ,Grmbu和OmMCo實現語義規(guī)約上的連接及互操作。C,實時構件A與實時構件B滿足外部接口語義規(guī)約可連接當Sb'= Sbr時，有(Sa^<~ >);(Sb' ~<>);Sc= (Sa^性,實時構件B與實時構件C滿足外部接口語義規(guī)約可連接);( Sb-<~ ));Sc- Sa^ Sb'"Sc,即進程通訊滿足Compo-性,即實時構件A存在服務提供端口A Out,其第i個方法nentelima^- + onmMou→6rrBav→ComponenteirimeB - + 6.xvBou→methods oi'(i 為自然數)與實時構件B服務請求端口B In中的第j個方法methoda. r'(j 為自然數)滿足構件方法簽由此,實時構件A的行為進程能與實時構件C的行為進名、斷言和實時約束特征的適配性;實時構件B存在服務提程,經由實時構件B相互通信與協(xié)作,形成一個較大規(guī)模的供端口B _Out,其第w個方法methode on"(w 為自然數)與行為進程組合成了一個新的合成軟構件系統(tǒng),從而實現了構實時構件C服務請求端口C In中的第h個方法methode_ n^件的合成。即證。(h為自然數)滿足構件方法簽名、斷言和實時約束特征的適定理2在合成軟構件系統(tǒng)中,將其中一個實時構件剝配性;根據RCRSM模型的規(guī)約方法，另設實時構件A服務離,并更換.上一個新的實時構件后,系統(tǒng)能仍能維系原有的功請求端口規(guī)約進程描述為P.^= (6ruAth DGaoMAke口.能特征 和時間屬性,則稱該實時構件具有可替換性,同時該實OonAin ),服務提供端口規(guī)約進程描述為Pou^= (.rerom時構件與新的實時構件能相互替換?？?...um),內部行為語義規(guī)約進程描述為證明:設實時構件A通過其服務提供端口或服務請求端P.m^= (6.mM^M ;6M2 ;.. ;6roMAm ),其中k,n,m為自然數,則實口method I ,method.2* ,. methoda'(i為自然數)與余留軟時構件A的語義規(guī)約進程描述為Comonentminm^=P.^;構件系統(tǒng)環(huán)境Env相互連接及互操作,其端口對應的通信和PamA ;Pom^ ;同理設實時構件B服務請求端口規(guī)約進程描述操作進程為OrMN ,G6mM^2 ,..‘,那么根據推論1、推論2,為P.B = (anmMEl D6uxnH 0-.Dam),服務提供端口規(guī)約如果3實時構件B,其服務提供端口或服務請求端口進程描述為P.nB= (abB D6oxtBon2...w),內部行method:' ,method,? ,.. ,methods'(i為自然數)對應的通信和為語義規(guī)約進程描述為PomB = (6oM8l ;6sMm ;.5),其操作進程為GreMB ,6ouP ,..、6rau"*，使得6rouAM = GrmMBI ,6rxvA2中l(wèi),q,r為自然數,則實時構件B的語義規(guī)約進程描述為=6rn ,... = 6rxM“* ,則實時構件B與實時構件A能相Component bian B=PB;PB;Pu*;同理設實時構件C服務互替換，且仍能維系原有合成軟構件系統(tǒng)的功能特征和時間請求端口規(guī)約進程描述為P.c = (GreurCn D6mMCn口..屬性。即證.口orxcx),服務提供端口規(guī)約進程描述為Pouc= (6murCoum推論3滿足構件可替換性的構件,可以實現構件的演Do...orxCoru),內部行為語義規(guī)約進程描述為化進程。Pom°= (6um° ;6rmMC ;.*),其中t,u.g為自然數,則實證明:設實時構件A可被實時構件B替換更新,并由時構件C的語義規(guī)約進程描述為ComponentealimnC- Puc;RCRSM模型的規(guī)約方法,設實時構件A服務請求端口規(guī)約P.m°;Puc.進程描述為P.^ = (ormrl DormMAin2 0..omMAt ),服務提供這樣端口方法methodA_ on' 的語義規(guī)約描述體所對應的端口規(guī)約進程描述為Pou^ = (6roMAoml D6r-Morue 口.進程體為omMom ,端方法methode_ n'的語義規(guī)約描述體D6rM Ao),內部行為語義規(guī)約進程描述為Pom^= (6m^';所對應的進程體為6noruv ,端口方法methods_ on" 的語義規(guī)6ouMA ;.*.*),其中k,n,m為自然數,實時構件A的語義約描述體所對應的進程體為6xMBbor ,端口方法methodc_ n"規(guī)約進程描述為Componentnale^ =P.^ ;Pm ;Pon^ ;設實時的語義規(guī)約描述體所對應的進程體為Gurcm.由于實時構件構件 B服務請求端口規(guī)約進程描述為Pa=(weO_6..mA和B.B和C滿足外部接口語義規(guī)約可連接性，即端口方法...x),服務提供端口規(guī)約進程描述為Pu=methodA .Cn' 與端口方法methodB.。' 具有語義規(guī)約層的可(GrM Boul口6ru Ron2...6.M Ro),內部行為語義規(guī)約進程描連接性,則GuMoo =rr ;端口方法methods_ on"與端口方述為 PamB = (6rmBl ;0rm ;-0*),其中l(wèi),q,r為自然數，法methodc_m“具有語義規(guī)約層的可連接性,則OmBou=實時構件B的語義規(guī)約進程描述為Componentr wumnB=PmB;GncC*.又由于實時構件A的語義規(guī)約進程描述為Compo- P."P.m*. 根據定理2,由于實時構件A可被實時構件Bnentwim^= Pn^;Pm^ ;Pou^ ,實時構件B的語義規(guī)約進程描替換更新,有述為Componentlm"=P.B ;Pam ";PouB ,實時構件C的語義| 中國煤化工咖,... =mlhn,k規(guī)約進程描述為Componenteumc=PmC;PmC;PoC,則CHCNMH(.....o...3Sa∈SA,其中SA為實時構件A語義規(guī)約進程中所有跡的集合使得GouMo =[Sa]o,且3Sb'∈SB,其中SB為實GrMBoun,n=q、即Pou^=Pon";時構件B語義規(guī)約進程中所有跡的集合,使得6Mmwi= Sb, .③(6rmMmAI ,6rM^2 ,.. ,6rmMAm )∩(6mMB1 ,6mM2 ,. ,0rmM^")=因為oni=6axr制,所以跡Sa能與跡Sb'連接，即(Sa~ (GrmM^ ,Gor. ,..");即Pn^∩Pm=Pom^;倆方數據且替換后的系統(tǒng)能仍能維系原有的功能特征和時間屬性,則實時構件B的內部行為語義蘊含實時構件A的內部行(6rsmA1 ,6rsMA2 ,.. ,6rxMm),其中k,n,m為自然數,則實時構件為語義,實時構件B是實時構件A的演化構件。即證。A的語義規(guī)約進程描述為Componentelime^= P^;Pom^;在推論3的證明中,實時構件B體現了實時構件A的自Pou^;又設實時子構件B服務請求端口規(guī)約進程描述為P.B身演化，即構件外部連接接口不變,內部行為發(fā)生改變,升級=(6u En ,6rMHm ,.. ,6rMHN ),服務提供端口規(guī)約進程描述為為新的更有競爭力的版本,其演化進程可語義規(guī)約描述為:Pou B=(6rarBoxl ,6r.NBon ,.. ,6xbm) ,內部行為語義規(guī)約進程Pam^- +Pom。描述為PB= (6rxMB1 ,6x* ,...),其中l(wèi),q,r為自然4實時合 成構件的語義規(guī)約機制數,則實時構件B的語義規(guī)約進程描述為ComponentelinB=P.m";Pn";Pou";并設實時合成構件符號表示為A+ B,其合實時合成構件是由若干反射式實時構件經過合成組裝而成如圖1所示。成的大粒度構件,且該構件仍是反射式實時構件,即其語義規(guī)約描述機制依然遵循實時構件的反射式語義模型RCRSM，支持實時合成構件的行為反射及演化進程。由此可見,反射式實時構件是一種迭代構件,可以最終組建實時軟件系統(tǒng)。A本節(jié)則重點研究實時合成構件的語義規(guī)約描述方法,使其結合前面幾節(jié)中的知識,形成較為規(guī)整的軟件合成語義規(guī)約分圖1實時構件A與B的合成示意圖析理論,供實際工程應用借鑒。依據實時構件的反射式語義模型::= (實時構件的語義那么有實時子構件A服務請求端口語義規(guī)約中方法描模型,實時構件語義模型的元數據,實時構件反射語義) ,我述體rtM對應的原子進程集合為S^= {GrauAtn ,6srAh ,.們對實時合成構件的語義規(guī)約表達同樣是以該構件中帶時間Orastink },服務提供端口語義規(guī)約中方法描述體rtM對應的原約束特征的方法描述體rtM為基本規(guī)約單位,并在構件子進程集合為Sout^ = (ormMAou ,6ruMon2 ,. ,omAo },內部行CSPI5]行為語義上對應于一個個的原子進程6rur，同時這些原為語義規(guī)約中方法描述體rtM對應的原子進程集合為Sam^子進程也就成為了實時合成構件反射與和演化操作的元數據= (oroMAl ,oroM^ ,..o..);實時子構件B服務請求端口語(metadata) ,并且實時合成構件的語義規(guī)約同樣是由該構件義規(guī)約中方法描述體rtM對應的原子進程集合為SB=的外部接口連接規(guī)約和內部行為語義規(guī)約所組成。然而作為