目標(biāo)驅(qū)動(dòng)的軟件需求模型及應(yīng)用

1、第7期姚劍等:目標(biāo)驅(qū)動(dòng)的軟件需求模型及應(yīng)用目標(biāo)驅(qū)動(dòng)的軟件需求模型及應(yīng)用姚劍毋國(guó)慶(武漢大學(xué)軟件工程國(guó)家重點(diǎn)實(shí)驗(yàn)室43072)摘要目標(biāo)驅(qū)動(dòng)的軟件需求模型的研究是需求工程中的一個(gè)新的研究課題.本文首先將介紹基于目標(biāo)驅(qū)動(dòng)的軟件需求模型的KAOS方法然后利用該方法來(lái)描述有關(guān)圖書(shū)館系統(tǒng)的某些需求以探討檢測(cè)需求中存在的沖突和偏差及消除它們的某些方法。關(guān)鍵詞需求工程KAOS方法沖突偏差l介紹需求工程是軟件工程中的一個(gè)重要組成部分一個(gè)系統(tǒng)的成功與否很大

2、部分取決于系統(tǒng)需求是否全面和正確。需求工程與軟件系統(tǒng)的現(xiàn)實(shí)目標(biāo)、功能及約束有關(guān)同時(shí)也與軟件行為精確的詳細(xì)說(shuō)明及軟件所在的外在環(huán)境有關(guān)。目標(biāo)驅(qū)動(dòng)的軟件需求分析方法是近幾年才興起的它與面向?qū)ο蠛褪录?qū)動(dòng)的軟件需求分析方法相比更接近于現(xiàn)實(shí)世界與系統(tǒng)的目的和功能更加緊密相關(guān)。在需求工程過(guò)程中軟件系統(tǒng)的現(xiàn)實(shí)目標(biāo)必須被明確地定義這是因?yàn)?需求的詳細(xì)說(shuō)明必須與目標(biāo)實(shí)現(xiàn)緊密有關(guān)目標(biāo)為需求說(shuō)明提供了一個(gè)完整性的驗(yàn)證標(biāo)準(zhǔn)一若需求說(shuō)明滿足所有規(guī)定的目標(biāo)則此需

3、求說(shuō)明是完全的:目標(biāo)是最終解決需求中沖突、偏差和障礙的來(lái)源目標(biāo)一般是需求文檔中最穩(wěn)定的信息。總之需求“實(shí)現(xiàn)”目標(biāo)如同程序?qū)崿F(xiàn)設(shè)計(jì)規(guī)格說(shuō)明一樣。一般來(lái)說(shuō)一個(gè)系統(tǒng)的需求一開(kāi)始很難完全確定下來(lái)而且需求中的目標(biāo)有些過(guò)于理想目標(biāo)之間會(huì)產(chǎn)生沖突因此怎樣識(shí)別過(guò)于理想的目標(biāo)和檢測(cè)目標(biāo)之間的沖突并采取適當(dāng)?shù)募夹g(shù)與方法來(lái)解決它們成了系統(tǒng)需求是否完全且正確的關(guān)鍵。在目標(biāo)級(jí)檢測(cè)沖突和偏差、識(shí)別障礙并且很好地消除它們這一點(diǎn)在需求工程過(guò)程中尤為重要。本文的目的在于

4、通過(guò)圖書(shū)館系統(tǒng)實(shí)例分析來(lái)說(shuō)明如何從系統(tǒng)目標(biāo)的角度利用一些最新技術(shù)和方法來(lái)檢測(cè)需求規(guī)格說(shuō)明中存在的其它問(wèn)題識(shí)別以及最終消除需求中存在的偏差和障礙。2KAOS方法K八05方法【1一3]是近期推出的一種需求模型其目的是支持基于目標(biāo)驅(qū)動(dòng)的需求的整個(gè)確立過(guò)程一在復(fù)合系統(tǒng)中從可實(shí)現(xiàn)的高級(jí)目標(biāo)到需求、對(duì)象以及分配給各個(gè)代理的操作(“復(fù)合系統(tǒng)”在這里用于強(qiáng)調(diào)系統(tǒng)不僅包括軟件而且包括所在的環(huán)境)。KAOS方法有益于精確定義需求有益于需求文檔的書(shū)寫(xiě)更方便并

5、且有益于最終的需求說(shuō)明書(shū)更易于被他人理解。KAOS方法提供了一門(mén)需求規(guī)格說(shuō)明語(yǔ)言、一種基于目標(biāo)驅(qū)動(dòng)的軟件需求確立模型和有關(guān)的元級(jí)知識(shí)。2.1KAOS語(yǔ)言KAOS語(yǔ)言是一種用于定義需求規(guī)格的說(shuō)明語(yǔ)言它提供了一套豐富的基本概念定義(如對(duì)象、操作、代理、目標(biāo)、需求、假設(shè)和腳本等等)。此語(yǔ)言不僅能捕捉一般語(yǔ)言能捕捉的V幾lat需求而且能捕捉why、v門(mén)飛。和when三類需求。KAOS語(yǔ)言是一種兩級(jí)結(jié)構(gòu)的多范例規(guī)格說(shuō)明語(yǔ)言:i)語(yǔ)義網(wǎng)外層:定義概

6、念、概念的屬性和概念與概念之間的鏈接:il)形式化的內(nèi)層定義:形式化定義概念。外層用于概念模型化、需求跟蹤能力、規(guī)格說(shuō)明重用:內(nèi)層用于形式化推理。KA0s語(yǔ)言包括i)目標(biāo)、需求約束、對(duì)象的實(shí)時(shí)時(shí)序邏輯的規(guī)范化說(shuō)明:i)操作或行為的前置后置條件i)為確保需求或約束而加強(qiáng)的規(guī)范化說(shuō)明。例如考慮以下圖書(shū)館系統(tǒng)的目標(biāo)Achieve[C叩yKep認(rèn)sLongAsNeeded]的規(guī)范化說(shuō)明rGo‘Acuv‘ICopyKp“ongASNedd]‘徜若

7、需毛.啊碑竺一瞇缽絲1co”censBoo匕BOkCopyM呱berLlb叫一與目標(biāo)百關(guān)的對(duì)尿名層’Jlform山弋黑糕優(yōu)篇黑罷默器o一目標(biāo)的非形式忱義Fon司I〕efVln:Memberb:B。比be:BookCoPyBorow婦19《風(fēng)bc)^Copy(beb)今。(決eds(mb)一Boro們lg(瓜bc))一目標(biāo)的形式化定義收稿日期:1999年1月24日形式化聲明內(nèi)層是用實(shí)時(shí)時(shí)序邏輯描述的本文以后將會(huì)用到以下幾種算子:o稱為ne

8、xt算子。A表示“下一時(shí)刻(狀態(tài))有A”心稱為sometimes算子令A(yù)表示“從現(xiàn)行狀態(tài)起終將有狀態(tài)A”口稱為alwa鄉(xiāng)s算子口A表示“從現(xiàn)行狀態(tài)起永遠(yuǎn)是A”體稱為unless算子A環(huán)侶表示“A一直真除非B真”注意:口P等價(jià)于P于們[’alse實(shí)時(shí)限制用下標(biāo)來(lái)指示例如:心自n產(chǎn)意味著“在將來(lái)n個(gè)單位u的時(shí)間之內(nèi)的某一時(shí)刻有A”氏加A意味著“在將來(lái)n個(gè)單位u的時(shí)間之后永遠(yuǎn)第7期姚劍等:目標(biāo)驅(qū)動(dòng)的軟件需求模型及應(yīng)用困G)心日mbeb(Bor

9、~ng(mbe卜Copy(beb)祀ZmoBorO嫩ng(mbe))現(xiàn)用(NG)中子公式oBorowing(mbe)與(D)的結(jié)論進(jìn)行合一然后通過(guò)(D)回代(NG今可得邊界條件:心日mbCb(Borowing(mbe)八Copy(beb)胡、2.noNeeds(mb))即為:令日低be議Bormwing(mbc卜CoPy(beb)A口ZmNeeds(mb))上面的例子沒(méi)有考慮到其它條件現(xiàn)在再次考慮上面的目標(biāo)(Gl)和下面的目標(biāo)(G3):

10、(G3)Achieve[CopiesEventuallyAvailable](需要的書(shū)最終可以獲得)Vmbeblib:Library(Need成mb)八CoPy(beb)八LILib(belib)二O3be(Copy(beb)月川二ib(belib)閃知ai1able(belib)))其中LILib(bclib)意味著“圖書(shū)館曾購(gòu)買(mǎi)過(guò)書(shū)be”戶渾ailabl《bclib)意味著“可從圖書(shū)館中獲得書(shū)be’o所給定的域描述為:(D)日m(B

11、or0wlng(mbe)~戶渾ailabl《belib)顯然會(huì)產(chǎn)生偏差現(xiàn)在再次利用回代否定斷言方法可得出邊界條件:0日mbeblib(Needs(mb)八C叩y(beb)八LILib(belib)A口(Vbe(CoPy(beb)八【nLib(bclib)二日耐:Men1ber(記荊nABorowing(mbe)咖eed成m’b)))))此邊界條件說(shuō)明了這樣一種可能性:某人需要某本已登記入館的書(shū)而所有此書(shū)都被別人永久性地借走。一般我們通過(guò)

12、避免邊界條件來(lái)解決此偏差:每本受歡迎的書(shū)在圖書(shū)館內(nèi)都保留一本不借。同樣也可引入新的避免目標(biāo)徹oid[LasteopyBorowed](防止每本書(shū)的最后一份副本被借出)來(lái)解決此偏差:vln.bebl颯Requesting(mbe)幾astCopy(beb)八LILib(belib)幼氏(Borowing(mbe)八Copy(beb)八1llLlb(belib)))其中RequeSting(mbc)意味著“借書(shū)者m要借書(shū)be?，F(xiàn)在再次考慮上

13、面的Avoid目標(biāo)和下面的實(shí)現(xiàn)目標(biāo)AchieveIB。~ngRequestsatisfied1(滿足借書(shū)請(qǐng)求):Vmbeblib(Requesting(m.be)沁opy(beb卜玩Lib(belib)幼心(Borowing(低be)八Copy(beb)八L止ib(belib)))以上兩個(gè)目標(biāo)正符合下邊的“實(shí)現(xiàn)一避免”偏差模型〔l]。(實(shí)現(xiàn)目標(biāo)〕(通免目標(biāo)).(城抽由、一假設(shè)P:Requesting(mbe)八CoPy(beb)八InL

14、ib(blib)Q:Bormwl幻g(mbe)ACopy(beb)八1llLib(belib):R:Requesting(mb)ALastCOPy(beb)入加工ib(behb):s與Q相同:可得邊界條件:心日mbeblib(Requesting(mbe)八InLib(belib)ACoPy(beb)從astCoPy(beb))為了解決上面的偏差我們可削弱實(shí)現(xiàn)目標(biāo)Achieve[Borm誠(chéng)ngRe明estsatislied]成為:Vmb

15、eblib(Requesting(mbe)八LastCoPy(beb)八Copy(bcb)八1llLib(belib)幼心(Borowing(mbc)八Copy(beb)八InLib(belib)))我們從上面的例子中可看出假如多個(gè)目標(biāo)以及其域描述集之間存在偏差為了消除它我們將引入新的目標(biāo)但是新目標(biāo)很可能會(huì)與其它目標(biāo)相沖突從而有利于徹底解決需求中存在的問(wèn)題因此我們建議在消除偏差時(shí)最好引入新目標(biāo)而且新目標(biāo)剛好夠消除此偏差。倘若需求說(shuō)明中存

16、在術(shù)語(yǔ)沖突(在需求說(shuō)明中同一現(xiàn)實(shí)概念用不同的語(yǔ)法名稱來(lái)表示例如:“借書(shū)者需要某本書(shū)”這一現(xiàn)實(shí)概念在不同的目標(biāo)中分別用Neds(mbc)和v抽nt成mbc床示)和命名沖突(在需求說(shuō)明中同一語(yǔ)法名稱表示不同的現(xiàn)實(shí)概念例如:Borowing(mbe)在不同目標(biāo)中分別表示“借書(shū)者m借了書(shū)be”和“借書(shū)者m正要借書(shū)bc”)需求中存在的偏差很可能無(wú)法檢測(cè)出來(lái)這樣會(huì)導(dǎo)致系統(tǒng)的最終需求不完全且不正確為此我們將第二節(jié)中的需求確立模型略為修改在“偏差檢測(cè)、

17、障礙識(shí)別”之前檢測(cè)術(shù)語(yǔ)沖突和命名沖突并想辦法消除它們。以上各例子都是關(guān)于沖突和偏差檢測(cè)以及消除的當(dāng)然圖書(shū)館系統(tǒng)中不只存在這些沖突和偏差檢測(cè)沖突和偏差以及消除它們的技術(shù)和方法也遠(yuǎn)不只這些。下面舉幾個(gè)有關(guān)障礙識(shí)別和消除障礙的例子例如:考慮如下目標(biāo)Vmbeblib(Need漢mb)八CoPy(beb)加勺ailable(belib)二合Borowing(mbe))其域描述為:Vln.bcli議Bormwing(mbe)二OPen(libm)月

18、物ailabl《bclib))其中oPen(libm)表示“此時(shí)圖書(shū)館可以借書(shū)”很明顯此目標(biāo)過(guò)于理想例如電腦出現(xiàn)故障、以前所借的書(shū)中有過(guò)期的、書(shū)借滿了或書(shū)己被別人借光等等都會(huì)導(dǎo)致障礙為此首先介紹一下回代否定目標(biāo)方法[zl的一般過(guò)程:1)初始步:取0:=G(G為某一目標(biāo))2)歸納步設(shè)A勸C為被選擇的域規(guī)則用C匹配公式0中某子公式L則林二mgu(LC)0:=0[LIA.閃現(xiàn)利用此方法可形式化地推導(dǎo)出潛在的障礙:心日mbeblib(Nee奴風(fēng)