唐運(yùn)璇 李奎

摘 要：基于構(gòu)件的軟件開(kāi)發(fā)是當(dāng)前軟件開(kāi)發(fā)的主流泛型。如何形式化地刻畫構(gòu)件的組裝過(guò)程是業(yè)界關(guān)注的重要問(wèn)題之一。本論文對(duì)Petri網(wǎng)進(jìn)行擴(kuò)展，作為演化活動(dòng)的表示基礎(chǔ)。在此基礎(chǔ)上分析了構(gòu)件的動(dòng)態(tài)性質(zhì)與結(jié)構(gòu)性質(zhì)，給出了組裝的原理、組裝的方式與組裝的框架，對(duì)復(fù)合組裝的行為與框架性質(zhì)進(jìn)行分析。

關(guān)鍵詞：Petri網(wǎng)；構(gòu)件性質(zhì)；構(gòu)件組裝

1 構(gòu)件的Petri網(wǎng)表示及性質(zhì)

1.1 擴(kuò)展Petri網(wǎng)表示構(gòu)件

形式化構(gòu)件定義由兩個(gè)部分組成，輸入輸出規(guī)約，把構(gòu)件封裝為一個(gè)邊界單入口單出口的接口規(guī)約，其次是由構(gòu)件內(nèi)部組成，內(nèi)部包括構(gòu)件的功能化屬性和參數(shù)化屬性，參數(shù)化屬性是內(nèi)部組成間的聯(lián)系機(jī)制，功能化發(fā)生是實(shí)現(xiàn)內(nèi)部間交互式行為的動(dòng)作部件，這些部件間的相互關(guān)系組成了一個(gè)構(gòu)件內(nèi)部實(shí)體，通過(guò)規(guī)約相互依賴、相互生存、相互作用，從而在接口處產(chǎn)生一組操作序列，引發(fā)構(gòu)件行為并感染其他相連接的構(gòu)件。

定義1 構(gòu)件C由一個(gè)4元組組成，是Petri網(wǎng)的一種擴(kuò)展，C=：

①P為有限庫(kù)所集，表示構(gòu)件狀態(tài)；其中P？勐{p，ip，op}；其中ip，op出入口處的特殊庫(kù)所，是構(gòu)件間相互通信、相互作用、相互依賴的接口庫(kù)所；

②T為有限變遷集，表示構(gòu)件操作與實(shí)現(xiàn)，構(gòu)件的行為動(dòng)作；

③F？哿P×T∪T×P，表示有向的弧集，是構(gòu)件內(nèi)部相互操作行為與狀態(tài)的約束關(guān)系；

④W為非空有限集，表示庫(kù)所變遷中功能屬性和參數(shù)化屬性組合及數(shù)量，構(gòu)件C中弧集集合的權(quán)函數(shù)與容量函數(shù)產(chǎn)生的數(shù)據(jù)類型集；

⑤I/O={IP，OP}IP/OP？哿P分別為構(gòu)件C的邊界出入口集，有？坌ip∈IP，？坌op∈OP

定義2 構(gòu)件網(wǎng)C-net（CN）系統(tǒng)是由多元組組成CN=

④反證法，假如狀態(tài)op不是唯一正常結(jié)束狀態(tài)，那么？堝M∈R（M0）使得（CN，M0）[t>M且M是一個(gè)結(jié)束狀態(tài)，由條件2知（CN，M0）[t>M？圯（CN，M0）[t>op這是矛盾的；綜合1，2，3，4，定理得證。

2.2.2 動(dòng)態(tài)不變性判定

定義5 由兩個(gè)構(gòu)件C1=，C2=