張 杰，燕雪峰

(南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇南京 210016)

面向任務(wù)的作戰(zhàn)系統(tǒng)設(shè)計(jì)過(guò)程是基于任務(wù)需求，實(shí)現(xiàn)自頂向下的作戰(zhàn)系統(tǒng)體系結(jié)構(gòu)設(shè)計(jì)過(guò)程。在需求分析過(guò)程中，多個(gè)分析人員針對(duì)不同的任務(wù)進(jìn)行分析，導(dǎo)致任務(wù)模型之間沖突等問(wèn)題。由于模型的不完整性以及多樣性，特別是動(dòng)態(tài)需求模型和功能需求模型，使沖突很難被發(fā)現(xiàn)。目前很多學(xué)者都對(duì)模型一致性技術(shù)進(jìn)行了研究，文獻(xiàn)［1］中提出通過(guò)SPIN工具來(lái)檢測(cè)順序圖和狀態(tài)圖的一致性，SPIN是一個(gè)模擬有限狀態(tài)并發(fā)系統(tǒng)的模型檢測(cè)工具，以協(xié)議/過(guò)程語(yǔ)言Promela描述的系統(tǒng)模型與待驗(yàn)證的性質(zhì)為輸入，在找出語(yǔ)法錯(cuò)誤的基礎(chǔ)上，模擬系統(tǒng)的交互執(zhí)行;提出用LTL(線性時(shí)代邏輯)來(lái)描述系統(tǒng)的性質(zhì)，需要一定的數(shù)學(xué)基礎(chǔ)，而且模型必須轉(zhuǎn)換成 Promela。文獻(xiàn)［2］提出基于Büchi自動(dòng)機(jī)理論對(duì)狀態(tài)圖和順序圖進(jìn)行一致性驗(yàn)證的方法，把狀態(tài)圖轉(zhuǎn)換成Büchi自動(dòng)機(jī)As，順序圖轉(zhuǎn)換成多個(gè)LTL公式，再把多個(gè)LTL公式轉(zhuǎn)換成Büchi自動(dòng)機(jī)集合{Af1，Af2，…，Afn}，通過(guò)判斷 As與自動(dòng)機(jī)集合的乘積是否為空來(lái)判斷兩者是否一致，但該方法的檢測(cè)結(jié)果不能通過(guò)直觀展示出來(lái)。文獻(xiàn)［3］中提出基于圖轉(zhuǎn)換理論，通過(guò)AGG工具靜態(tài)分析檢測(cè)用例模型之間的潛在沖突和依賴，AGG是一個(gè)對(duì)屬性圖文法進(jìn)行編輯、分析和推理的可視化工具，對(duì)圖變換規(guī)則進(jìn)行臨界對(duì)分析(Critical Pair Analysis)得到規(guī)則間潛在的沖突、依賴關(guān)系，但檢測(cè)出的依賴需進(jìn)一步處理。文中針對(duì)作戰(zhàn)系統(tǒng)任務(wù)模型提出基于AGGCT(Attributed Graph Grammar－based Consistency Checking)的檢測(cè)方法:把作戰(zhàn)系統(tǒng)模型轉(zhuǎn)換成屬性圖文法，再用AGG工具檢測(cè)功能模型間的沖突和依賴，并提出循環(huán)依賴和錯(cuò)誤依賴檢測(cè)算法對(duì)依賴進(jìn)行進(jìn)一步處理。

1 面向任務(wù)的作戰(zhàn)系統(tǒng)模型及結(jié)構(gòu)

作戰(zhàn)系統(tǒng)模型由作戰(zhàn)需求視圖和UML子圖組成。作戰(zhàn)需求視圖中包含使命和任務(wù)兩種建模元素。使命確定系統(tǒng)的設(shè)計(jì)目的和范圍，需要多個(gè)不同的任務(wù)協(xié)同完成。任務(wù)的動(dòng)態(tài)需求用活動(dòng)圖建模，靜態(tài)需求用類圖建模，功能需求用自然語(yǔ)言對(duì)事件的前置和后置條件進(jìn)行建模。由于自然語(yǔ)言無(wú)法形式化，文中提出用對(duì)象圖來(lái)描述功能需求，把動(dòng)態(tài)需求和靜態(tài)需求結(jié)合。對(duì)象圖中對(duì)象是靜態(tài)需求中類的實(shí)例。

以作戰(zhàn)系統(tǒng)中護(hù)航使命模型為例，潛艇為完成護(hù)航使命需要不斷偵察是否有敵方目標(biāo)出現(xiàn);如果出現(xiàn)敵方潛艇，需要發(fā)射魚(yú)雷攻擊，所以把護(hù)航使命分解成偵察和雷攻擊兩個(gè)任務(wù)。

靜態(tài)需求模型:圖1是護(hù)航使命的類圖。一個(gè)潛艇(Submarine)有多部聲納設(shè)備(Sonar)，同時(shí)裝載了多個(gè)魚(yú)雷(Torpedo)，需要一個(gè)魚(yú)雷發(fā)控裝置(Torpedo Fire Control)來(lái)控制魚(yú)雷。聲納(Sonar)可以同時(shí)探測(cè)多匹目標(biāo)，假定目標(biāo)為敵方潛艇(Enemy Submarine)，檢測(cè)到目標(biāo)后發(fā)射魚(yú)雷攻擊目標(biāo)。由于在需求階段，圖1中的類沒(méi)有添加方法，圖2是類圖的一個(gè)實(shí)例圖。

動(dòng)態(tài)需求模型:圖3是護(hù)航的作戰(zhàn)需求視圖以及任務(wù)的活動(dòng)圖。潛艇用聲納來(lái)偵察，偵察任務(wù)首先需要聲納開(kāi)機(jī)(start Up Sonar)，然后探測(cè)目標(biāo)(detect)，如果目標(biāo)有威脅，攻擊目標(biāo)(attack)。魚(yú)雷攻擊任務(wù)活動(dòng)圖包括魚(yú)雷發(fā)控裝置開(kāi)機(jī)(Startup Torpedo Fire Control)、發(fā)射魚(yú)雷(shoot)和設(shè)置目標(biāo)位置(set Target)。

功能需求模型:功能需求用對(duì)象圖對(duì)事件前置和后置條件進(jìn)行建模。在任務(wù)模型中，事件指動(dòng)態(tài)需求中的活動(dòng)(actions)。偵察任務(wù)和魚(yú)雷攻擊任務(wù)的活動(dòng)圖中事件的前置后置條件分別如圖4和圖5所示，對(duì)象圖中每個(gè)對(duì)象都是靜態(tài)需求UML類圖的實(shí)例，例如:在圖4聲納開(kāi)機(jī)(startUpSonar)功能需求中對(duì)象Submarine是圖1中類Submarine的實(shí)例。

由于多個(gè)需求分析人員分析不同的任務(wù)需求，導(dǎo)致模型中存在語(yǔ)義上的重疊，在多個(gè)任務(wù)協(xié)作完成使命的過(guò)程中產(chǎn)生錯(cuò)誤。需求模型不一致將導(dǎo)致設(shè)計(jì)中的錯(cuò)誤，事后修改代價(jià)非常高;如果錯(cuò)誤未被發(fā)現(xiàn)則會(huì)影響系統(tǒng)的可靠性和健壯性。上例中偵察任務(wù)和魚(yú)雷攻擊任務(wù)的功能需求之間存在語(yǔ)義上的重疊，攻擊目標(biāo)(attack)和發(fā)射魚(yú)雷(shoot)都刪除了Torpedo。由于兩個(gè)任務(wù)協(xié)同完成護(hù)航使命，所有任務(wù)的活動(dòng)必須依次執(zhí)行。但由于語(yǔ)義上的重疊導(dǎo)致攻擊目標(biāo)(attack)和發(fā)射魚(yú)雷(shoot)無(wú)法依次執(zhí)行，所以功能模型之間存在沖突。

2 作戰(zhàn)系統(tǒng)模型一致性檢測(cè)方法

屬性圖文法［4］既有直觀的圖形符號(hào)又有較成熟的形式化理論，基于規(guī)則的圖轉(zhuǎn)換可以有效地描述任務(wù)的功能需求，所以把作戰(zhàn)系統(tǒng)模型的UML子圖轉(zhuǎn)換成屬性圖文法并形式化檢測(cè)功能需求之間的沖突和依賴。

2.1 UML子圖轉(zhuǎn)換成屬性圖文法

2.1.1 UML類圖轉(zhuǎn)換成類型圖

定義1 一個(gè)類圖模型是一個(gè)五元組C=(Cn，Cp，Co，Cr，Cm)，其中，Cn表示類名;Cp表示類屬性;Co表示類的操作;Cr表示類之間的關(guān)系;Cm多重性。文中討論的類圖是處于需求階段，只考慮類圖的靜態(tài)特性，由于類的操作屬于動(dòng)態(tài)性的知識(shí)，不予考慮。

定義2 一個(gè)類型圖模型是一個(gè)四元組TG=(TGn，TGp，TGr，TGm)，其中 TGn表示圖的名稱，TGp表示圖的屬性，TGr表示圖的關(guān)系，TGm表示多重性。

顯然，很容易把類圖轉(zhuǎn)換成屬性圖，由于不考慮類的操作，類圖中的Cn，Cp，Cr，Cm可以直接轉(zhuǎn)換成類型圖中的 TGn，TGp，TGr，TGm。類之間的關(guān)系 Cr有聯(lián)系(Association)和泛化(Generalization)等。類型圖之間的關(guān)系TGr有邊(Edge)和繼承(Extend)兩種。類圖中的泛化關(guān)系可以之間轉(zhuǎn)換成類型圖中的繼承。

在大多數(shù)情況下，類圖中兩個(gè)類之間的聯(lián)系是二元的，而且，聚集和復(fù)合總是二元聯(lián)系。因此，文中只考慮二元聯(lián)系。二元聯(lián)系有一個(gè)聯(lián)系名和兩個(gè)聯(lián)系端。每個(gè)聯(lián)系端有一個(gè)角色名和一個(gè)多重性約束，一個(gè)描述導(dǎo)航性的屬性和一個(gè)描述關(guān)系類型的屬性。多重性約束描述的非負(fù)整數(shù)的范圍表示該位置上可以有多少個(gè)對(duì)象，并且限制了一端的一個(gè)對(duì)象可以和另一端的多少個(gè)對(duì)象有聯(lián)系。類型圖中的邊也是用來(lái)表示兩個(gè)類型圖之間的兩個(gè)類型圖可以相互擁有的對(duì)象的數(shù)目，所以類圖中的聯(lián)系可以直接轉(zhuǎn)換成類型圖中的邊。

2.1.2 UML對(duì)象圖轉(zhuǎn)換成規(guī)則

定義3 UML對(duì)象圖是一個(gè)二元組G={N，E}。N為節(jié)點(diǎn)n的有限集;E為邊e的有限集;節(jié)點(diǎn)n及邊e都用對(duì)象表示。

在上文中已經(jīng)介紹了，活動(dòng)圖的前置后置條件用UML對(duì)象圖來(lái)描述，且UML對(duì)象圖中的對(duì)象都是UML類圖中類的實(shí)例。在屬性圖文法中，規(guī)則的前置后置條件中的屬性圖都是類型圖的實(shí)例，可以直接把UML對(duì)象圖中的對(duì)象轉(zhuǎn)換成規(guī)則前置或者后置條件中的實(shí)例。UML對(duì)象圖中的邊可以轉(zhuǎn)換成規(guī)則前置或者后置條件中的邊，所以UML對(duì)象圖可以轉(zhuǎn)換成規(guī)則的條件后置條件。

利用上述轉(zhuǎn)換方法，靜態(tài)需求中UML類圖對(duì)應(yīng)屬性圖文法中的類型圖。UML類圖的實(shí)例圖作為屬性圖文法的開(kāi)始圖，開(kāi)始圖代表圖轉(zhuǎn)換的起點(diǎn)。功能需求轉(zhuǎn)換成屬性圖文法中的圖轉(zhuǎn)換規(guī)則集，功能需求前置條件對(duì)象圖對(duì)應(yīng)規(guī)則的左部圖，后置條件對(duì)象圖對(duì)應(yīng)規(guī)則的右部圖。由于模型中沒(méi)有對(duì)功能需求限制執(zhí)行條件，所以屬性圖文法中約束集為空。本文用AGG工具來(lái)分析任務(wù)模型轉(zhuǎn)化的屬性圖文法，得到功能需求之間的沖突和依賴。

兩個(gè)圖轉(zhuǎn)換規(guī)則之間有依賴關(guān)系是指一個(gè)規(guī)則的執(zhí)行必須以另一個(gè)規(guī)則的執(zhí)行為前提條件，AGG工具檢測(cè)出所有功能需求之間的依賴關(guān)系，但沒(méi)有進(jìn)行詳細(xì)分析。循環(huán)依賴是指依賴關(guān)系中出現(xiàn)環(huán)，錯(cuò)誤依賴表示功能需求之間依賴關(guān)系與動(dòng)態(tài)需求中活動(dòng)圖的執(zhí)行流程不一致。循環(huán)依賴或錯(cuò)誤依賴一般是設(shè)計(jì)中的錯(cuò)誤，所以需要對(duì)依賴關(guān)系進(jìn)行驗(yàn)證。

2.2 循環(huán)依賴檢測(cè)算法

該算法對(duì)使命中功能需求之間的依賴關(guān)系深度搜索，同時(shí)加入棧來(lái)記錄搜索路徑，如果在搜索中出現(xiàn)棧中已經(jīng)存在的功能需求，說(shuō)明找到環(huán)，同時(shí)輸出環(huán)中所有元素。假設(shè)有3個(gè)功能需求A、B、C，A依賴B，B依賴C，C依賴A，三者的依賴關(guān)系形成一個(gè)環(huán)。首先對(duì)A的依賴關(guān)系進(jìn)行深度搜索，通過(guò)A的依賴關(guān)系找到B，再對(duì)B進(jìn)行搜索，找到C，這時(shí)棧中保存的是A、B、C，在對(duì)C進(jìn)行搜索的過(guò)程中找到A，因?yàn)锳已經(jīng)存在棧中，所以找到一個(gè)環(huán)，輸出環(huán)中元素A、B、C、A。相關(guān)定義如下:(1)功能需求 FunctionRequirement=＜name，dependencs＞，name是名稱，dependeces是該功能需求依賴關(guān)系數(shù)組。(2)任務(wù)Task=＜name，functionRequirements＞，name表示任務(wù)的名稱，functionRequirements是任務(wù)的功能需求數(shù)組。(3)使命Mission=＜name，tasks＞，name表示使命的名稱，tasks是完成使命的所有任務(wù)。(4)frs數(shù)組記錄使命中所有功能需求，用visited數(shù)組來(lái)表示功能需求是否被遍歷過(guò)，初始化為false。(5)棧stack用來(lái)記錄遍歷路徑，算法調(diào)用之前棧為空;top表示棧頂?shù)奈恢茫跏蓟癁椋?。(6)count用來(lái)記錄環(huán)的個(gè)數(shù)，初始化為0。

2.3 錯(cuò)誤依賴檢測(cè)算法

圖6 循環(huán)依賴檢測(cè)算法

假設(shè)活動(dòng)action1的功能需求依賴活動(dòng)action2的功能需求，且action1和action2在同個(gè)活動(dòng)圖中，那么action2必須在action1之前執(zhí)行，即活動(dòng)圖中必須存在action2→action1或者action2→…→action1執(zhí)行流程，否則該依賴關(guān)系是一個(gè)錯(cuò)誤依賴。UML活動(dòng)圖中主要的建模元素是活動(dòng)(Action)、判斷(Decision)和轉(zhuǎn)換(Transition)，因此判斷活動(dòng)圖的執(zhí)行流程時(shí)節(jié)點(diǎn)只考慮這3個(gè)元素。首先需要遍歷活動(dòng)圖中的所有模型元素，找到所有的活動(dòng)和判斷節(jié)點(diǎn)。然后從action2開(kāi)始對(duì)活動(dòng)圖進(jìn)行深度搜索通過(guò)單步轉(zhuǎn)換(Transition)到達(dá)的活動(dòng)或判斷節(jié)點(diǎn)，如果在搜索的過(guò)程中發(fā)現(xiàn)action1，說(shuō)明活動(dòng)圖中有該活動(dòng)流，否則繼續(xù)至結(jié)束。相關(guān)定義如下:(1)功能需求FunctionRequirement=＜name，dependencs＞，name表示名稱，dependeces是該功能需求依賴關(guān)系數(shù)組。(2)任務(wù)Task=＜name，functionRequirements＞，name表示任務(wù)的名稱，functionRequirements是任務(wù)功能需求數(shù)組。(3)actions數(shù)組記錄活動(dòng)圖中所有的活動(dòng)，decisions記錄活動(dòng)圖中所有的判斷。(4)isActionVisited數(shù)組用于記錄活動(dòng)圖中所有的活動(dòng)是否被搜索過(guò)，與actions數(shù)組對(duì)應(yīng);isDecisionVisited數(shù)組用來(lái)記錄活動(dòng)圖中所有的判斷是否被搜索過(guò)，與decisions數(shù)組對(duì)應(yīng)。

圖7 錯(cuò)誤依賴檢測(cè)算法

3 一致性檢測(cè)系統(tǒng)的實(shí)現(xiàn)及驗(yàn)證

作戰(zhàn)系統(tǒng)需求工具中用AGGCT一致性檢測(cè)方法來(lái)保證建模的正確性。基于AGGCT一致性檢測(cè)系統(tǒng)的輸入是有領(lǐng)域模型和UML模型組成的作戰(zhàn)系統(tǒng)模型，檢測(cè)結(jié)果會(huì)輸出所有的沖突依賴關(guān)系、錯(cuò)誤依賴和循環(huán)依賴。檢測(cè)系統(tǒng)的類圖如圖8所示，其主要職責(zé)如表1所示。

圖8 基于AGGCT一致性檢測(cè)系統(tǒng)的類圖

表1 基于AGGCT一致性檢測(cè)系統(tǒng)中類的主要職責(zé)

用該系統(tǒng)檢測(cè)第一章中的護(hù)航使命模型，圖8是AGG檢測(cè)出shoot和attack都刪除了torpedo引起的沖突。由于協(xié)同完成護(hù)航使命，只能由其中一個(gè)執(zhí)行刪除操作。所以修改了attack活動(dòng)的功能需求，刪除torpedo操作只由shoot活動(dòng)來(lái)執(zhí)行，消除了沖突。

圖9 shoot和attack之間的沖突

AGG工具把所有任務(wù)的功能需求之間的依賴關(guān)系用矩陣顯示，如圖10所示，記每個(gè)功能需求為pi，如果pi依賴pj，則表格第j行第i列的數(shù)字＞0，如果沒(méi)有依賴關(guān)系，則等于0。例如:attack依賴于detect，那么第2行第3列上的數(shù)字約為0。功能需求不能依賴本身，所以矩陣對(duì)角線的位置并沒(méi)有計(jì)算。

圖10 修改之后的攻擊目標(biāo)(attack)功能需求

一致性檢測(cè)系統(tǒng)對(duì)圖10中所有的依賴關(guān)系進(jìn)行檢測(cè)，發(fā)現(xiàn)依賴關(guān)系中沒(méi)有循環(huán)依賴，shoot對(duì)setTarget的依賴關(guān)系是錯(cuò)誤依賴。在圖3中，魚(yú)雷攻擊任務(wù)的活動(dòng)圖中發(fā)射魚(yú)雷(shoot)發(fā)生在設(shè)置目標(biāo)位置(setTarget)之前，而功能需求中shoot對(duì)setTarget的依賴則要求設(shè)置目標(biāo)位置(setTarget)必須在發(fā)射魚(yú)雷(shoot)之前執(zhí)行。所以，修改魚(yú)雷攻擊任務(wù)的活動(dòng)圖，把設(shè)置目標(biāo)位置活動(dòng)(setTarget)放在發(fā)射魚(yú)雷活動(dòng)(shoot)之前，活動(dòng)的執(zhí)行流程與依賴關(guān)系一致，消除了錯(cuò)誤依賴。

圖11 功能需求之間的依賴關(guān)系

4 結(jié)束語(yǔ)

模型一致性以及驗(yàn)證一直是軟件工程領(lǐng)域內(nèi)研究的熱點(diǎn)，本文考慮作戰(zhàn)系統(tǒng)中不同需求分析人員針對(duì)不同的任務(wù)進(jìn)行分析的特點(diǎn)，提出一種基于圖文法形式化檢測(cè)任務(wù)模型一致性的方法，把作戰(zhàn)系統(tǒng)模型轉(zhuǎn)換成屬性圖文法并檢測(cè)功能需求間的沖突和依賴，同時(shí)驗(yàn)證了依賴關(guān)系中是否存在循環(huán)依賴和錯(cuò)誤依賴。提出了相應(yīng)的檢測(cè)算法，循環(huán)依賴檢測(cè)算法通過(guò)深度優(yōu)先搜索找到依賴關(guān)系中的環(huán)，同時(shí)輸出環(huán)中的所有依賴關(guān)系;錯(cuò)誤依賴檢測(cè)算法對(duì)活動(dòng)圖進(jìn)行深度優(yōu)先搜索，檢測(cè)功能模型的依賴關(guān)系與動(dòng)態(tài)模型的執(zhí)行流程是否一致。任務(wù)可能還含有子任務(wù)，子任務(wù)是否可以繼承父任務(wù)的約束關(guān)系，以及如何檢測(cè)子任務(wù)間的沖突和依賴，可以作為下一步的研究方向。

［1］陳卉，竇萬(wàn)峰.UML順序圖與狀態(tài)圖的一致性檢查［J］.計(jì)算機(jī)工程，2008，34(18):62 －64.

［2］張自強(qiáng).基于自動(dòng)機(jī)理論的UML模型一致性研究［D］.蘭州:蘭州大學(xué)，2009.

［3］JAN H H，REIKO H，GABI T.Detection of conflicting fuctional requirements in a use case － driven approach［J］.SoftWare Enginneering，2002:105 －115.

［4］邢陽(yáng)，謝德平，馬曉星，等.一種圖文法制導(dǎo)的軟件體系結(jié)構(gòu)開(kāi)發(fā)環(huán)境Artemis－GADE［J］.計(jì)算機(jī)研究與發(fā)展，2010，47(7):1166 －1173.

［5］韓秀清，曾曉勤，鄒陽(yáng)，等.圖文法綜述［J］.計(jì)算機(jī)科學(xué)，2008，35(8):10 －16.

［6］劉輝，麻志毅，邵維忠.一種基于圖轉(zhuǎn)換的模型重構(gòu)描述語(yǔ)言［J］.軟件學(xué)報(bào)，2009，20(8):2087－2101.