代 飛，王黎霞，謝仲文，張 璇，朱 銳

(1.云南大學(xué)軟件學(xué)院，云南昆明650091;2.云南大學(xué)云南省軟件工程重點(diǎn)實(shí)驗(yàn)室，云南昆明650091;3.云南大學(xué)經(jīng)濟(jì)學(xué)院，云南昆明650091)

軟件過(guò)程的研究大致始于20世紀(jì)80年代中期，以O(shè)sterweil于1987年發(fā)表的“軟件過(guò)程也是軟件”為代表性著作，自此掀起了“軟件過(guò)程運(yùn)動(dòng)”，并逐步形成軟件過(guò)程工程.在軟件過(guò)程領(lǐng)域，軟件過(guò)程建模和軟件過(guò)程驗(yàn)證是兩大關(guān)鍵活動(dòng).軟件過(guò)程建模是對(duì)軟件過(guò)程進(jìn)行抽象和表示的活動(dòng)，方式可以是非形式化、半形式化或形式化的，其目的是建立過(guò)程模型［1］.通過(guò)對(duì)過(guò)程模型的認(rèn)識(shí)和分析，增強(qiáng)對(duì)過(guò)程本身的理解，進(jìn)而更好地支持軟件開發(fā).軟件過(guò)程驗(yàn)證是檢驗(yàn)軟件過(guò)程模型與過(guò)程需求是否一致的活動(dòng)，方式也可以是非形式化、半形式化或形式化的，其目的是驗(yàn)證過(guò)程模型的正確性、提高過(guò)程模型的可靠性，進(jìn)而提高軟件質(zhì)量.與非形式化的建模和驗(yàn)證相比，形式化的建模和驗(yàn)證更加準(zhǔn)確，有利于計(jì)算機(jī)實(shí)現(xiàn)，是開發(fā)半自動(dòng)化或自動(dòng)化驗(yàn)證工具的基礎(chǔ).與軟件過(guò)程建模相比，有關(guān)軟件過(guò)程驗(yàn)證的研究相對(duì)較少.

針對(duì)軟件演化過(guò)程建模，本文作者之一基于基本Petri網(wǎng)，擴(kuò)展了面向?qū)ο蠹夹g(shù)和Hoare邏輯，提出了軟件演化過(guò)程元模型EPMM(software evolution process meta model)，以及一系列建模方法、技術(shù)和工具，用以支持軟件演化過(guò)程的建模［2］.EPMM的提出，有效解決了軟件演化過(guò)程的形式建模問(wèn)題.但是，軟件演化過(guò)程模型被EPMM建模產(chǎn)生后，軟件演化過(guò)程模型的形式驗(yàn)證問(wèn)題卻尚未得到解決.

對(duì)軟件過(guò)程驗(yàn)證而言，一方面，目前相關(guān)文獻(xiàn)主要集中在結(jié)構(gòu)和性質(zhì)層面，方法以語(yǔ)法檢驗(yàn)和模型檢測(cè)為主.結(jié)構(gòu)驗(yàn)證是指檢驗(yàn)過(guò)程模型的結(jié)構(gòu)是否滿足某些語(yǔ)法要求，只能從靜態(tài)角度對(duì)軟件過(guò)程模型的結(jié)構(gòu)和語(yǔ)法進(jìn)行檢驗(yàn)，無(wú)法確保動(dòng)態(tài)性質(zhì)的滿足;性質(zhì)驗(yàn)證是指檢驗(yàn)過(guò)程模型在執(zhí)行過(guò)程中是否滿足性質(zhì)，無(wú)法確保過(guò)程模型的行為與過(guò)程規(guī)約一致.本文作者之一在文獻(xiàn)［3］中對(duì)結(jié)構(gòu)驗(yàn)證和性質(zhì)驗(yàn)證的現(xiàn)狀作了系統(tǒng)地總結(jié).另一方面，現(xiàn)有的基于Petri網(wǎng)的過(guò)程模型驗(yàn)證方法可以大致分為4類［4］:①基于狀態(tài)空間的驗(yàn)證方法，以Petri網(wǎng)模型檢測(cè)方法為代表［5］;② 基于結(jié)構(gòu)的驗(yàn)證方法;③ 基于邏輯推理的驗(yàn)證方法;④ 基于代數(shù)網(wǎng)的驗(yàn)證方法.但是，這些方法只能支持結(jié)構(gòu)驗(yàn)證或性質(zhì)驗(yàn)證，并不能很好地支持行為驗(yàn)證［4］.

針對(duì)當(dāng)前軟件過(guò)程缺乏行為驗(yàn)證的不足，文中引入ACP［6］風(fēng)格的進(jìn)程代數(shù)，對(duì)EPMM進(jìn)行擴(kuò)展，提出軟件演化過(guò)程元模型代數(shù)EPMM-A(software evolution process meta model-algebra)，在其公理系統(tǒng)的支持下，基于等式推導(dǎo)驗(yàn)證軟件演化過(guò)程模型的行為與行為規(guī)約是否一致，進(jìn)而使得行為驗(yàn)證方式從模型推導(dǎo)變?yōu)榇鷶?shù)推導(dǎo).最后，通過(guò)證明EPMM-A公理系統(tǒng)的可靠性來(lái)說(shuō)明代數(shù)推導(dǎo)方法的正確性.

文中首先提出擬解決的問(wèn)題及其相關(guān)概念，然后討論行為驗(yàn)證的方式，進(jìn)而證明代數(shù)推導(dǎo)的正確性.

1 問(wèn)題描述與相關(guān)概念

1.1 問(wèn)題描述

形式驗(yàn)證軟件演化過(guò)程模型的行為涉及3個(gè)問(wèn)題:軟件演化過(guò)程模型的形式化描述、行為規(guī)約的形式化描述和形式化的行為驗(yàn)證方式.

1.1.1 軟件演化過(guò)程模型的形式描述

對(duì)于第1個(gè)問(wèn)題，本文作者之一基于基本Petri網(wǎng)，擴(kuò)展了面向?qū)ο蠹夹g(shù)和Hoare邏輯，提出了軟件演化過(guò)程元模型EPMM.自上而下，EPMM分為4層:全局層、過(guò)程層、活動(dòng)層和任務(wù)層.詳細(xì)定義具體參見文獻(xiàn)［2］.由EPMM的形式定義可知，由此建模產(chǎn)生的軟件演化過(guò)程模型是形式化的.

例子 過(guò)程工程師基于EPMM建模產(chǎn)生的軟件演化過(guò)程模型p1，如圖1所示.

本質(zhì)上，由EPMM建模產(chǎn)生的軟件演化過(guò)程模型是一個(gè)擴(kuò)展的基本Petri網(wǎng)，條件集C中的元素只有“有托肯”和“無(wú)托肯”2種狀態(tài).

圖1 一個(gè)軟件演化過(guò)程模型p1

為了簡(jiǎn)便，這里忽略了全局層、活動(dòng)層和任務(wù)層的形式定義，只給出了p1過(guò)程層的形式定義:

C={c1，c2，c3，c4};A={a1，a2，a3};F={(c1，a1)，(a1，c2)，(c2，a2)，(c2，a3)，(a2，c3)，(a3，c4)};M0={c1}，

式中:N={C，A;F}，稱為p1的結(jié)構(gòu).

圖形化的軟件演化過(guò)程模型中的條件通常用圓圈表示，軟件演化過(guò)程模型中的活動(dòng)通常用方框表示.

1.1.2 行為規(guī)約的形式描述

對(duì)于第2個(gè)問(wèn)題，本文作者之一使用ACP風(fēng)格的進(jìn)程代數(shù)對(duì)EPMM進(jìn)行擴(kuò)展，提出了軟件演化過(guò)程元模型代數(shù)EPMM-A，既作為軟件演化過(guò)程模型的代數(shù)語(yǔ)義域，又作為行為規(guī)約的形式規(guī)約語(yǔ)言.

EPMM-A包含3部分:第1部分是類子和常量，第2部分是操作符，第3部分是公理，具體參見表格1.其變遷規(guī)則規(guī)定了進(jìn)程間的操作語(yǔ)義，參見表2.

表1 EPMM-A

關(guān)于EPMM-A的非形式化描述和變遷規(guī)則的非形式化描述，具體參見文獻(xiàn)［3］.

定義1(行為規(guī)約) 行為規(guī)約是過(guò)程工程師根據(jù)過(guò)程需求，規(guī)定軟件演化過(guò)程中活動(dòng)的執(zhí)行順序.

例子 假設(shè)軟件演化過(guò)程開始執(zhí)行活動(dòng)a1，隨后選擇執(zhí)行活動(dòng)a2和a3，最后執(zhí)行終止.根據(jù)過(guò)程需求，過(guò)程工程師使用EPMM-A，行為規(guī)約被描述為a1·(a2·δ+a3·δ).

表2 EPMM-A的變遷規(guī)則

1.2 相關(guān)概念

為了從進(jìn)程理論的角度對(duì)軟件演化過(guò)程的行為進(jìn)行研究，本節(jié)提出了行為空間、行為圖和互模擬關(guān)系等基本概念.

定義2(變遷) 變遷是一個(gè)三元組b=(p，a，p')，形如pp'，其中，①p和p'表示進(jìn)程，p，p'∈P，P是進(jìn)程集;②a表示活動(dòng)，a∈A，A是活動(dòng)集.

變遷pp'表示進(jìn)程p執(zhí)行活動(dòng)a后演化為進(jìn)程p';變遷p表示進(jìn)程p執(zhí)行活動(dòng)a后，能成功終止;變遷pδ表示進(jìn)程p執(zhí)行活動(dòng)a后變?yōu)樗肋M(jìn)程.

需要注意的是，這里P是個(gè)抽象概念.在EPMM的上下文中，P指軟件演化過(guò)程模型的集合;在EPMM-A中，P指進(jìn)程項(xiàng)的集合.

為了以統(tǒng)一的方式比較進(jìn)程間的行為，下面提出行為空間和行為圖.

定義3(行為空間) 行為空間是一個(gè)二元組PBS=(P，B)，其中，①P是進(jìn)程集;②B是變遷集.

定義4(行為圖) 行為圖是一個(gè)三元組BG=(P，E，R)，其中，①P是進(jìn)程集;②E={(pi，pj)|pi，pj∈P，?a∈A:(pi，a，pj)∈B}，其中，A是活動(dòng)集，B是變遷集;③R:E→A，R(pi，pj)=a當(dāng)且僅當(dāng)(pi，a，pj)∈B;④ 選pi∈P作為頂點(diǎn).稱P中的元素為節(jié)點(diǎn)，E中的元素描述進(jìn)程間的執(zhí)行關(guān)系，R中的元素是進(jìn)程執(zhí)行的活動(dòng)，pi為行為圖的頂點(diǎn).

互模擬關(guān)系是行為等價(jià)關(guān)系中最好的一種.所以，采用互模擬關(guān)系作為行為比較的一個(gè)標(biāo)準(zhǔn).

定義5(互模擬關(guān)系) 互模擬關(guān)系R是直積P×P的子集當(dāng)且僅當(dāng)對(duì)于任意的p，p'，q，q'∈P和a

∈ 有:①;②;③ 其中，P是進(jìn)程集，A是活動(dòng)集.2個(gè)進(jìn)程是互模擬的，記為p～q.

2 行為驗(yàn)證方式

仍給一個(gè)由EPMM建模產(chǎn)生的軟件演化過(guò)程模型和一個(gè)基于EPMM-A定義的行為規(guī)約，如何判斷軟件演化過(guò)程模型的行為與行為規(guī)約定義的行為一致，這涉及驗(yàn)證方式.

文中行為驗(yàn)證的方式有兩種:一種是人工推導(dǎo)的方式，稱為模型推導(dǎo)，具體參見定義6;另一種是形式推導(dǎo)的方式，稱為代數(shù)推導(dǎo)，具體參見定義7.

為了說(shuō)明模型推導(dǎo)和代數(shù)推導(dǎo)的區(qū)別，下面將分別使用兩種方式驗(yàn)證圖1所示的P1是否滿足行為規(guī)約a1·(a2·δ+a3·δ).

2.1 模型推導(dǎo)

定義6(模型推導(dǎo)) 判斷一個(gè)由EPMM建模產(chǎn)生的軟件演化過(guò)程模型的行為與一個(gè)基于EPMM-A定義的行為規(guī)約規(guī)定的行為是否等價(jià)，需要分別構(gòu)建各自的行為圖，找到互模擬關(guān)系，進(jìn)行行為比較，這種行為驗(yàn)證方式稱為模型推導(dǎo).

使用模型推導(dǎo)驗(yàn)證p1是否滿足行為規(guī)約a1·(a2·δ+a3·δ)，需要 3 步:

第1步，構(gòu)建軟件演化過(guò)程模型的行為圖.根據(jù)Petri網(wǎng)的點(diǎn)火規(guī)則，p1的行為圖如圖2所示.其中，M0，M1，M2，M3是P1的情態(tài)，為M0={c1}，M1={c2}，M2={c3}，M3={c4};N是P1的結(jié)構(gòu)，N={C，A;F}.

第2步，構(gòu)建行為規(guī)約的行為圖.根據(jù)EPMM-A的變遷規(guī)則，a1·(a2·δ+a3·δ)的行為圖如圖3所示.

第3步，判斷軟件演化過(guò)程模型和行為規(guī)約間是否存在互模擬關(guān)系.根據(jù)互模擬關(guān)系的定義，對(duì)基于p1的行為圖和a1·(a2·δ+a3·δ)的行為圖進(jìn)行比較，不難發(fā)現(xiàn)，p1和a1·(a2·δ+a3·δ)間存在互模擬關(guān)系，如圖4所示.

圖4 p1和 a1·(a2·δ+a3·δ)間的互模擬關(guān)系

為了直觀，圖4中將存在互模擬關(guān)系的進(jìn)程用虛線連接起來(lái).不難證明:(N，M0)和a1·(a2·δ+a3·δ)、(N，M1)和 (a2·δ+a3·δ)、(N，M2)和 δ、(N，M3)和δ均是互模擬的.值得注意的是，p1在情態(tài)M2和M3處不能發(fā)生點(diǎn)火任何操作，則(N，M2)和(N，M3)代表死進(jìn)程.

綜上所述，軟件演化過(guò)程模型p1與行為規(guī)約a1·(a2·δ+a3·δ)規(guī)定的行為等價(jià).

從上述驗(yàn)證步驟可以看出，模型推導(dǎo)的過(guò)程需要分別構(gòu)建軟件演化過(guò)程模型和行為規(guī)約的行為圖，并根據(jù)互模擬關(guān)系的定義，人工判斷兩者之間是否是互模擬的.

這種行為驗(yàn)證方式缺乏嚴(yán)格的形式化基礎(chǔ)，具有相當(dāng)?shù)碾S意性，不利于開發(fā)計(jì)算機(jī)輔助驗(yàn)證工具.

2.2 代數(shù)推導(dǎo)

定義7(代數(shù)推導(dǎo)) 在EPMM-A的上下文中，基于公理系統(tǒng)，使用等式關(guān)系判斷軟件演化過(guò)程模型和行為規(guī)約是否等價(jià)，這種方式稱為代數(shù)推導(dǎo).

使用代數(shù)推導(dǎo)驗(yàn)證p1是否滿足行為規(guī)約a1·(a2·δ+a3·δ)，需要2 步:

第1步，計(jì)算p1的代數(shù)語(yǔ)義.基于文獻(xiàn)［3］提出的軟件演化過(guò)程模型的代數(shù)語(yǔ)義，在行為等價(jià)的前提下，可以將待驗(yàn)證的軟件演化過(guò)程模型p1形式轉(zhuǎn)換為一個(gè)基于EPMM-A定義的進(jìn)程項(xiàng)a1·(a2·δ+a3·δ).限于篇幅，具體計(jì)算過(guò)程參見文獻(xiàn)［3］.

第2步，使用EPMM-A的公理系統(tǒng)，形式推導(dǎo)p1的代數(shù)語(yǔ)義和a1·(a2·δ+a3·δ)是否存在等式關(guān)系.若存在，則軟件演化過(guò)程模型滿足行為規(guī)約規(guī)定的行為.通過(guò)推導(dǎo)，不難發(fā)現(xiàn)，p1的代數(shù)語(yǔ)義a1·(a2·δ+a3·δ)和行為規(guī)約a1·(a2·δ+a3·δ)間存在等式關(guān)系.

綜上所述，軟件演化過(guò)程模型p1與行為規(guī)約a1·(a2·δ+a3·δ)規(guī)定的行為等價(jià).

從上述驗(yàn)證步驟可以看出，代數(shù)推導(dǎo)的過(guò)程不需要構(gòu)建軟件演化過(guò)程模型和行為規(guī)約的行為圖，也不需要人工判斷兩者間是否存在互模擬關(guān)系，只需計(jì)算軟件演化過(guò)程模型的代數(shù)語(yǔ)義，并根據(jù)公理系統(tǒng)，形式推導(dǎo)軟件演化過(guò)程模型的代數(shù)語(yǔ)義和行為規(guī)約間是否存在等式關(guān)系.

這種行為驗(yàn)證方式具有嚴(yán)格的形式化基礎(chǔ)，支持形式驗(yàn)證，有利于開發(fā)計(jì)算機(jī)輔助驗(yàn)證工具.

3 代數(shù)推導(dǎo)的正確性

對(duì)軟件演化過(guò)程模型的行為驗(yàn)證而言，為了說(shuō)明代數(shù)推導(dǎo)的正確性，需要證明EPMM-A作為一個(gè)形式推理系統(tǒng)的可靠性.非形式化地說(shuō)，可靠性是指在EPMM-A中，若存在進(jìn)程項(xiàng)p和q，且p=q是由公理系統(tǒng)推導(dǎo)出的等式關(guān)系，則在進(jìn)程項(xiàng)的行為空間中，p和q是互模擬的，即由公理系統(tǒng)形式推導(dǎo)出的互模擬關(guān)系一個(gè)也不會(huì)多，形式定義見定理4.

既然等式關(guān)系是由EPMM-A的公理系統(tǒng)通過(guò)替換性、等價(jià)性和同余性3種方式推導(dǎo)所得，從可靠性證明的角度，那么互模擬關(guān)系也應(yīng)具有這3種性質(zhì).因此，文中首先證明互模擬關(guān)系具有等價(jià)性和同余性(congruence).

直觀地說(shuō)，等價(jià)關(guān)系是指如果p和q是互模擬的，則在EPMM-A的公理系統(tǒng)中，將p換成q后，不會(huì)改變系統(tǒng)的行為;同余關(guān)系是指多次應(yīng)用EPMMA的公理系統(tǒng)中的公理將p轉(zhuǎn)換成p'，將q轉(zhuǎn)換成q'后，p'和q'也是互模擬的，參見定義9.

文中借鑒了通信與移動(dòng)系統(tǒng)Pi演算中［7］進(jìn)程上下文的定義，給出了代數(shù)項(xiàng)上下文的定義.非正式地說(shuō)，一個(gè)進(jìn)程項(xiàng)的上下文是包含一個(gè)洞的進(jìn)程項(xiàng)表達(dá)式.

定義8(進(jìn)程項(xiàng)的上下文) 一個(gè)進(jìn)程項(xiàng)的上下文C由如下文法定義:

C::=［］|C+p|p+C|C·p|p·C|C‖p|p‖C|C╙p|p╙C|p*C|C*p，其中［］表示洞，p表示進(jìn)程項(xiàng).

C［q］表示將C中的洞里填入進(jìn)程項(xiàng)q后得到的結(jié)果.

C::=［］|C+p|p+C|C·p|p·C|C‖p|p‖C|C╙p|p╙C|p*C|C*p稱為進(jìn)程項(xiàng)的上下文.

定義9(進(jìn)程項(xiàng)上的同余關(guān)系) 令 Σ是EPMM-A上的基調(diào)，p，q和u是進(jìn)程項(xiàng)，若進(jìn)程項(xiàng)上的等價(jià)關(guān)系?被進(jìn)程項(xiàng)的上下文所保持，則稱這個(gè)等價(jià)關(guān)系為進(jìn)程項(xiàng)上的同余關(guān)系.

形式地說(shuō)，等價(jià)關(guān)系?被代數(shù)項(xiàng)的上下文所保持是指如果p?q成立，則下列式子都成立:①p+u?q+u;②u+p?u+q;③pu?qu;④up?uq;⑤p‖u?q‖u;⑥u‖p?u‖q;⑦p╙u?q╙u;⑧p*u?q*u;⑨ λM(p)?λM(q).

從定義9可知，同余關(guān)系必然是等價(jià)關(guān)系.

為證明進(jìn)程項(xiàng)間的互模擬關(guān)系是同余關(guān)系，需引入兩個(gè)概念:推導(dǎo)后的肯定變遷系統(tǒng)規(guī)約和組合格式.

3.1 推導(dǎo)后的肯定變遷系統(tǒng)規(guī)約

在并發(fā)交互式系統(tǒng)中，否定前提(參見定義10)的引入可以很好地解決死鎖檢測(cè)、優(yōu)先級(jí)、隨機(jī)行為和離散時(shí)間等問(wèn)題.但是，否定前提的引入帶來(lái)2個(gè)嚴(yán)重問(wèn)題:①變遷規(guī)則不一致;② 變遷規(guī)則無(wú)法決定操作語(yǔ)義［8］.

定義10(肯定前提和否定前提) 若變遷規(guī)則的前提中包含否定變遷，則稱前提為否定前提.若變遷規(guī)則的前提中不包含否定變遷，則稱前提為肯定前提.

例如，一個(gè)變遷規(guī)則形如

由于前提中存在t!t'，所以此前提為負(fù)前提.由前提可知，代數(shù)項(xiàng)t不能執(zhí)行活動(dòng)a，演變?yōu)榇鷶?shù)項(xiàng)t';由結(jié)論可知，代數(shù)項(xiàng)t執(zhí)行活動(dòng)a，演變?yōu)榇鷶?shù)項(xiàng)t'.顯然，前提和結(jié)論不一致，根據(jù)變遷規(guī)則無(wú)法判斷變遷是否發(fā)生.

為了解決第1個(gè)問(wèn)題，Groote在文獻(xiàn)［8］中提出了一個(gè)方法用于檢查變遷規(guī)則是否一致的問(wèn)題.該方法基于邏輯編程(logic programming)中的分層法(stratification)，其基本思路:如果變遷規(guī)則的結(jié)論復(fù)雜性大于前提的復(fù)雜性，則此變遷規(guī)則是一致的.

為了解決第2個(gè)問(wèn)題，Baeten在“帶優(yōu)先規(guī)則的項(xiàng)重寫系統(tǒng)”中提出了三值穩(wěn)定模型(three valued stable model)［9］，其基本思路:將變遷系統(tǒng)規(guī)約 TSS(由變遷規(guī)則組成)推導(dǎo)出的變遷分為彼此互不相交的3個(gè)集合:① 集合T表示可以發(fā)生的變遷集合;②集合F表示不可以發(fā)生的變遷集合;③集合U表示不確定是否可以發(fā)生的變遷集合.這樣，一個(gè)變遷集合的劃分可以由一個(gè)序偶＜T，U＞來(lái)決定，通過(guò)序偶＜T，U＞消除負(fù)前提帶來(lái)的不確定性.

定義11(肯定變遷系統(tǒng)規(guī)約) 對(duì)于變遷系統(tǒng)規(guī)約TSS，若每個(gè)變遷規(guī)則的前提都不包含負(fù)變遷，則稱TSS為肯定變遷系統(tǒng)規(guī)約.

由于肯定變遷系統(tǒng)規(guī)約不包含否定變遷，那么就不會(huì)出現(xiàn)變遷規(guī)則不一致的情形，因此也就不會(huì)出現(xiàn)無(wú)法判斷變遷是否發(fā)生的情況.

定義12(推導(dǎo)后的肯定變遷系統(tǒng)規(guī)約)［8］若一個(gè)變遷系統(tǒng)規(guī)約TSS的最小三值穩(wěn)定模型不包含不確定的變遷，則稱變遷系統(tǒng)規(guī)約是推導(dǎo)后的肯定變遷系統(tǒng)規(guī)約.

定理1 EPMM-A的變遷系統(tǒng)規(guī)約是推導(dǎo)后的肯定變遷系統(tǒng)規(guī)約.

證明 據(jù)表2可知，EPMM-A的每個(gè)變遷規(guī)則均不含有否定變遷，自然，EPMM-A的變遷系統(tǒng)規(guī)約必然是推導(dǎo)后的肯定變遷系統(tǒng)規(guī)約.

證畢.

綜上所述，EPMM-A的變遷規(guī)則中由于不包含否定變遷，因此不必考慮負(fù)前提所帶來(lái)的兩個(gè)嚴(yán)重問(wèn)題.

3.2 變遷規(guī)則的格式

自1981年P(guān)lotkin首次提出了結(jié)構(gòu)化操作語(yǔ)義方法以來(lái)，使用Plotkin式的結(jié)構(gòu)化方法定義進(jìn)程代數(shù)、進(jìn)程演算和規(guī)約語(yǔ)言的操作語(yǔ)義已經(jīng)成為了一種事實(shí)上的標(biāo)準(zhǔn).對(duì)于結(jié)構(gòu)化操作語(yǔ)義，一個(gè)關(guān)鍵問(wèn)題是:通過(guò)研究變遷規(guī)則的語(yǔ)法格式來(lái)確保互模擬關(guān)系是同余關(guān)系.

定義13(組合格式)［10］一個(gè)變遷規(guī)則ρ符合組合格式(panth format)，當(dāng)滿足以下3個(gè)條件:①對(duì)于ρ中的每個(gè)形如tt'的肯定前提，t'是單個(gè)變量;②對(duì)于ρ中的源只含有不超過(guò)一個(gè)的操作符;③在ρ的肯定前提的右邊和ρ的源中都出現(xiàn)的相同變量，出現(xiàn)次數(shù)不能超過(guò)一次.

事實(shí)上，組合格式是ntyft/ntyxt格式［8］和path格式［10］的組合.它允許變遷和謂詞同時(shí)存在，具有最大的語(yǔ)法自由性.

定理2 EPMM-A的變遷規(guī)則滿足組合格式.

證明 據(jù)表2可知，EPMM-A的每個(gè)變遷規(guī)則均滿足定義13的3個(gè)條件，因此，EPMM-A的變遷規(guī)則滿足組合格式.

證畢.

定理3 如果EPMM-A的變遷規(guī)則滿足推導(dǎo)后的肯定變遷系統(tǒng)規(guī)約和組合格式，那么由變遷系統(tǒng)規(guī)約所推導(dǎo)出的進(jìn)程項(xiàng)間的互模擬關(guān)系是同余關(guān)系，稱為同余互模擬關(guān)系，記為.

證明 設(shè)p，q，u是進(jìn)程項(xiàng);～是進(jìn)程項(xiàng)上的互模擬關(guān)系.

先證互模擬關(guān)系是等價(jià)關(guān)系，再證其是同余關(guān)系.

1)證明互模擬關(guān)系是等價(jià)關(guān)系.根據(jù)互模擬關(guān)系的定義，p～p成立，即～是自反的，所以有:

若p～q成立，根據(jù)互模擬關(guān)系的定義，進(jìn)程項(xiàng)p和q之間的行為可以相互模擬，那么q～p也成立，因此～是對(duì)稱的.

若p～q和p～u成立，根據(jù)互模擬關(guān)系的定義，則有:進(jìn)程項(xiàng)p和q之間的行為可以相互模擬，進(jìn)程項(xiàng)q和u之間的行為也可以相互模擬，即p，q和u之間的行為都可以相互模擬，那么p～u成立，因此～是傳遞的.

綜上所述，互模擬關(guān)系～是等價(jià)關(guān)系.

2)證明～是被進(jìn)程項(xiàng)的上下文所保持.也就是說(shuō)，如果p～q成立，則下列式子都成立:

①p+u?q+u;②u+p?u+q;③p·u?q·u;④u·p?u·q;⑤p‖u?q‖u;⑥u‖p?u‖q;⑦p╙u?q╙u;⑧p*u?q*u;⑨ λM(p)?λM(q).

證明的詳細(xì)過(guò)程，參見文獻(xiàn)［6］.

綜上所述，互模擬關(guān)系～是同余關(guān)系.證畢.

3.3 替換性的證明

證明了互模擬關(guān)系具有等價(jià)性和同余性后，對(duì)于可靠性的證明，還需要證明互模關(guān)系具有替換性，即證明:公理系統(tǒng)中的公理x=y(x和y代表變量，屬于過(guò)程集P)，通過(guò)替換操作后，σ(x)和σ(y)是互模擬的.

定理4(可靠性) 如果EPMM-A┝p=q成立，則在進(jìn)程項(xiàng)的行為空間中╞p～q成立，其中┝代表形式推導(dǎo)，╞代表邏輯蘊(yùn)含.

證明 為了證明簡(jiǎn)便，令σ(x)=a，σ(y)=b，σ(z)=c，其中a，b，c∈T(Σ).

1)在EPMM-A中，對(duì)于公理A1-A7而言，可靠性的證明過(guò)程如下:

公理A1:x+y=y+x描述了選擇復(fù)合操作符具有交換性.通過(guò)替換操作，2個(gè)進(jìn)程項(xiàng)的行為圖如圖5所示.

圖5 2個(gè)進(jìn)程項(xiàng)的行為圖

由圖5可以找出進(jìn)程項(xiàng)間存在的互模擬關(guān)系:a+b～b+a，b～b，a～a.因此，進(jìn)程項(xiàng)a+b和b+a是互模擬的.

公理A2:(x+y)+z=x+(y+z)描述了選擇復(fù)合操作符具有結(jié)合性，采用上述方法，不難證明(x+y)+z=x+(y+z)是互模擬的.

公理A3:x+x=x描述了變量x和x之間的選擇復(fù)合等價(jià)于x本身，采用上述方法，不難證明x+x和x是互模擬的.

公理A4:(x+y)·z=x·z+y·z描述了選擇復(fù)合操作符對(duì)于順序復(fù)合操作符滿足分配律，采用上述方法，不難證明(x+y)·z和x·z+y·z是互模擬的.

公理A5:(x·y)·z=x·(y·z)描述了順序復(fù)合操作符具有結(jié)合性，采用上述方法，不難證明(x·y)·z=x·(y·z)是互模擬的.

公理A6:x+δ=x描述了變量x和死進(jìn)程δ之間的選擇關(guān)系，采用上述方法，不難證明x+δ和x是互模擬的.

公理A7:δ·x=δ描述了變量x和死進(jìn)程δ之間的順序關(guān)系，采用上述方法，不難證明δ·x和δ是互模擬的.

2)在EPMM-A中，對(duì)于公理S1和S2而言，可靠性的證明過(guò)程如下:

公理S1:t1|t2=t2|t1描述了任務(wù)間同步操作具有交換性.在EPMM-A中，活動(dòng)由任務(wù)通過(guò)|合成.因此，執(zhí)行活動(dòng)a意味著執(zhí)行活動(dòng)a內(nèi)部的所有任務(wù).從執(zhí)行效果看，t1|t2和t2|t1均表示活動(dòng)a，因此兩者是互模擬的.

公理S2:(t1|t2)|t3=t1|(t2|t3)描述了任務(wù)間的同步操作具有結(jié)合性.從執(zhí)行效果看，(t1|t2)|t3和t1|(t2|t3)均表示活動(dòng)a，因此兩者是互模擬的.

3)在EPMM-A中，對(duì)于公理M1-M4而言，可靠性的證明過(guò)程如下:

公理M1:x‖y=x╙y+y╙x定義了并發(fā)復(fù)合操作的內(nèi)涵.EPMM-A支持交疊式語(yǔ)義，并發(fā)復(fù)合操作可以簡(jiǎn)化為左并發(fā)復(fù)合操作符.在交織式語(yǔ)義的上下文中，從觀察者的角度，x‖y和x╙y+y╙x的執(zhí)行效果是等價(jià)的，因此兩者是互模擬的.

公理M2:a╙x=a·x定義了左并發(fā)復(fù)合操作符的內(nèi)涵.在交織式語(yǔ)義的上下文中，從觀察者的角度，a╙x和a·x的執(zhí)行效果是等價(jià)的，因此兩者是互模擬的.

公理M3:a·x╙y=a·(x‖y)也定義了左并發(fā)復(fù)合操作符的內(nèi)涵.在交織式語(yǔ)義的上下文中，從觀察者的角度，a·x╙y和a·(x‖y)的執(zhí)行效果是等價(jià)的，因此兩者是互模擬的.

公理M4:(x+y)╙z=x╙z+y╙z描述了左并發(fā)復(fù)合操作符對(duì)選擇復(fù)合操作符具有右分配性.采用上述方法，不難證明(x+y)╙z和x╙z+y╙z x是互模擬的.

4)在EPMM-A中，對(duì)于公理C1-C3而言，可靠性的證明過(guò)程如下:

公理C1:x‖y=y‖x描述了并發(fā)復(fù)合操作符具有交換性.采用上述方法，不難證明x‖y和y‖x是互模擬的.

公理C2:(x‖y)‖z=x‖(y‖z)描述了并發(fā)副惡化操作符具有結(jié)合性.采用上述方法，不難證明(x‖y)‖z和x‖(y‖z)是互模擬的.

公理C3:(x╙y)╙z=x╙(y‖z)描述了左并發(fā)復(fù)合操作符和并發(fā)復(fù)合操作符之間的關(guān)系.采用上述方法，不難證明(x╙y)╙z和x╙ (y‖z)是互模擬的.

5)在EPMM-A中，對(duì)于公理CSO1-CSO5而言，可靠性的證明過(guò)程如下:

公理CSO1:λM(δ)=δ描述了死進(jìn)程不能發(fā)生任何點(diǎn)火操作.從觀察者的角度，λM(δ)和δ都不能執(zhí)行任何活動(dòng)，兩者是互模擬的.

公理CSO2:·a?M∧a·∩M=?λM(a)=a定義了狀態(tài)操作符的內(nèi)涵.若活動(dòng)a在情態(tài)M處是使能的，則λM(a)=a，那么，λM(a)和a是互模擬的.

公理CSO3:·a!?M∧a·∩M≠?λM(a)=δ定義了狀態(tài)操作符的內(nèi)涵.同上，兩者也是互模擬的.

公理 CSO4:λM(x+y)=λM(x)+λM(y)描述了狀態(tài)操作符對(duì)選擇復(fù)合操作符具有左分配律.通過(guò)替換操作，2個(gè)進(jìn)程項(xiàng)為λM(a+b)和λM(a)+λM(b)，分4種情況進(jìn)行討論:若活動(dòng)a在情態(tài)M處是使能的，則 λM(a+b)=a，λM(a)+λM(b)=a+δ=a，因此，λM(a+b)=a和 λM(a)+λM(b)是互模擬的;若活動(dòng)b在情態(tài)M處是使能的，則λM(a+b)=b，λM(a)+λM(b)=δ+b=b，因此，λM(a+b)=a和λM(a)+λM(b)是互模擬的;若活動(dòng)a和b在情態(tài)M處不是使能的，則 λM(a+b)=δ，λM(a)+λM(b)=δ，因此，λM(a+b)=a和 λM(a)+λM(b)是互模擬的;若活動(dòng)a和b在情態(tài)M處都是使能的，則 λM(a+b)=a+b，λM(a)+ λM(b)=a+b，因此，λM(a+b)=a和λM(a)+λM(b)是互模擬的.綜上所述，λM(x+y)和λM(x)+λM(y)是互模擬的.

公理 CSO5:λM(a·x)= λM(a)·(x)定義了狀態(tài)操作符的內(nèi)涵.采用上述方法，不難證明 λM(a·x)和 λM(a)·λ(x)是互模擬的.

6)在 EPMM-A中，對(duì)于公理 BKS1、BKS2和BKS3的可靠性證明過(guò)程，請(qǐng)參看文獻(xiàn)［6］.

證畢.

4 結(jié)論

1)使用ACP對(duì)EPMM進(jìn)行擴(kuò)展，提出了軟件演化過(guò)程元模型代數(shù)EPMM-A.

2)使用EPMM-A形式定義軟件演化過(guò)程模型的行為規(guī)約.

3)基于文獻(xiàn)［3］提出的代數(shù)語(yǔ)義，在EPMM-A公理系統(tǒng)的支持下，使用等式推導(dǎo)驗(yàn)證軟件演化過(guò)程模型的行為與行為規(guī)約是否一致，進(jìn)而使得行為驗(yàn)證方式從模型推導(dǎo)(非形式化)變?yōu)榇鷶?shù)推導(dǎo)(形式化).

4)為了說(shuō)明代數(shù)推導(dǎo)的正確性，證明了軟件演化過(guò)程元模型代數(shù)作為一個(gè)形式推理系統(tǒng)的可靠性.

References)

［1］ 李明樹，楊秋松，翟 健.軟件過(guò)程建模方法研究［J］.軟件學(xué)報(bào)，2009，20(3):524-545.Li Mingshu，Yang Qiusong，Zhai Jian.Systematic review of software process modeling and analysis［J］.Journal of Software，2009，20(3):524-545.(in Chinese)

［2］ Li T.An Approach to Modelling Software Evolution Processes［M］.Berlin:Springer-Verlag，2008.

［3］ 代 飛，李 彤，謝仲文，等.一種軟件演化過(guò)程模型的代數(shù)語(yǔ)義［J］.軟件學(xué)報(bào)，2012，23(4):846-863.Dai Fei，Li Tong，Xie Zhongwen，et al.Towards an algebraic semantics of software evolution process models［J］.Journal of Software，2012，23(4):846-863.(in Chinese)

［4］ 代 飛.基于EPMM的軟件演化過(guò)程模型驗(yàn)證［D］.昆明:云南大學(xué)軟件學(xué)院，2011.

［5］ 段振華，張 曼.Petri網(wǎng)模型檢測(cè)概述［J］.中國(guó)計(jì)算機(jī)學(xué)會(huì)通訊，2009，5(10):21-28.Duan Zhenhua，Zhang Man.Detection survey of Petri net model［J］.Communications of the CCF，2009，5(10):21-28.(in Chinese)

［6］ Fokkink W.Introduction to Process Algebra［M］.Berlin:Springer-Verlag，2007.

［7］ Robin Milner.通信與移動(dòng)系統(tǒng)π演算［M］.北京:清華大學(xué)出版社，2009.

［8］ Groote J F.Transition system specifications with negative premises［J］.Theoretical Computer Science，1993，118(2):263-299.

［9］ Baeten JCM，Bergstra JA，Klop JW，et al.Term-rewriting systems with rule priorities［J］.Theoretical Computer Science，1989，67(2/3):283-301.

［10］ Baeten J C M，Verhoef C.A congruence theorem for structured operational semantics with predicates［C］∥Proceedings of CONCUR93，LNCS715.Berlin:Springer-Verlag，1993:477-492.