鄒盛榮,彭昱靜,郭忠偉,劉春秋,周 塔,衛(wèi) 麗,顧愛華

摘 要:軟件需求獲取是軟件建模和分析的基礎(chǔ),傳統(tǒng)的軟件需求建模方法主要有2個(gè)重大的缺陷:一是非形式化的需求描述常導(dǎo)致需求的歧義性和不一致性,因而難以確認(rèn)和驗(yàn)證;二是易變性。針對(duì)此問題,結(jié)合實(shí)例提出用UML(Unified Modeling Language)的用例驅(qū)動(dòng)獲取軟件需求,并將得來的需求用形式化B方法的機(jī)器來表示需求,實(shí)現(xiàn)了軟件需求的形式化。實(shí)踐證明,用例驅(qū)動(dòng)的軟件需求獲取可以有效地獲取正確、合理的軟件需求,加上用形式化B方法的需求描述,可以有效地避免上述兩大缺陷。

關(guān)鍵詞:需求獲取;UML;用例驅(qū)動(dòng);B方法;形式化需求

中圖分類號(hào):TP309文獻(xiàn)標(biāo)識(shí)碼:A

文章編號(hào):1004-373X(2009)12-045-04

Case Study of Acquiring Formal Software Requirement

ZOU Shengrong,PENG Yujing,GUO Zhongwei,LIU Chunqiu,ZHOU Ta,WEI Li,GU Aihua

(Information Engineering College,Yangzhou University,Yangzhou,225009,China)

Abstract:Acquiring software requirement is the basis of software modeling and analysis,traditional software requirement modeling has two important defects:one is informal requirements description often leads toambiguity and inconsistency of requirements,so it is difficult to validate and verificate;and the other is variability.According to the above problems,this paper presents the use case driven analysis method of software requirements by Unitied Modeling Language(UML),and describes it by formal method,relizes formal software requirement.Practice proves that acquiring software requirement of use case driven can obtain effectively correct and reasonable software requirement,in addition to requirement description of formal B method.This method effectively avoids the above problems.

Keywords:requirement acquirement;UML;use case driven;B method;formal requirement

0 引 言

隨著計(jì)算機(jī)技術(shù)的發(fā)展,軟件規(guī)模日益龐大,軟件開發(fā)也日益復(fù)雜。隨之而來的問題是許多IT系統(tǒng)都無法實(shí)現(xiàn)期望,它們要么無法實(shí)現(xiàn)業(yè)務(wù)目標(biāo),要么無法有效支持用戶任務(wù),要么成本很難控制在預(yù)算之內(nèi)。究其原因,相當(dāng)多的軟件失敗是因?yàn)樾枨蟛幻靼谆蛘卟淮_定而致。自1991年J.Martin提出“需求工程”[1] 概念后,需求分析作為軟件工程的一個(gè)重要階段開始形成一門獨(dú)立學(xué)科,稱為需求工程。軟件需求的重要性正在不斷提高,因?yàn)樗怯脩纛A(yù)先知道將以什么樣的成本,獲得什么樣產(chǎn)品的途徑。

需求工程在軟件系統(tǒng)開發(fā)中的重要性已不容置疑。需求的獲取是需求工程的主體,是軟件系統(tǒng)開發(fā)過程中最為困難,也是最為重要的部分。只有真正滿足用戶需求的軟件產(chǎn)品才能為用戶接受,不能滿足用戶需求的產(chǎn)品,不管采用了多么先進(jìn)的技術(shù),對(duì)用戶來說都是毫無用處的。根據(jù)Leffingwell 在1997 年的研究,軟件項(xiàng)目中40%～60%的問題都是在需求的獲取和分析階段埋下了禍根[2]。在過去幾年,文獻(xiàn)主要強(qiáng)調(diào)需求建模和規(guī)約方法,現(xiàn)在重點(diǎn)轉(zhuǎn)移到了軟件需求獲取的有效方法。

傳統(tǒng)的需求分析過程通常采用數(shù)據(jù)流圖等方式來描述系統(tǒng)的邏輯模型。由于這些非形式化以及半形式化方法所需求的描述都未給出數(shù)學(xué)意義上嚴(yán)格的語法和語義說明,因此需求階段建立的模型或多或少的帶有不精確性、不完全性和不一致性。形式化方法(Formal Methods)是全面系統(tǒng)地使用基于數(shù)學(xué)的語言、技術(shù)和工具,精確地說明、開發(fā)和驗(yàn)證的軟件系統(tǒng),使用形式化方法描述的規(guī)約具有規(guī)范性和無二義性,而且形式化語言是一種機(jī)器可處理的描述語言,可以保證軟件復(fù)用自動(dòng)化成為可能。

1 用例驅(qū)動(dòng)的需求獲取

1.1 用例模型

用例模型是系統(tǒng)既定功能和系統(tǒng)環(huán)境的模型,它可以作為客戶和開發(fā)人員之間的契約。系統(tǒng)建模有許多種方法,每種建模方法,均可滿足不同的目的。然而,用例模型最重要的作用是將系統(tǒng)行為傳達(dá)給客戶或最終用戶,因此模型必須易于理解。用例模型驅(qū)動(dòng)了需求分析之后開發(fā)工作的各個(gè)階段和UML的各個(gè)模型。

用例模型采用若干個(gè)用例圖描述。用例圖是一個(gè)參與者和用例以及另外的定義和說明的可視化表示。用例圖不僅是一個(gè)圖,而且是系統(tǒng)想要的行為的全文檔化模型[3-5]。

1.2 用例

用例表示一個(gè)完整的給用戶傳值的功能性單元。用例是系統(tǒng)和用戶之間的動(dòng)作序列,而不是逐條的個(gè)體需求。顯著的用例改進(jìn)了這一問題?，F(xiàn)在,需求是用例的形式,需求以順序的方式提供系統(tǒng)的行為,以相關(guān)的替換和異常信息結(jié)束。用例只說明了系統(tǒng)要做什么,而且在設(shè)計(jì)上領(lǐng)先,因?yàn)樗鼘?duì)于收集需求和開始設(shè)計(jì)過程都非常便利。

1.3 參與者

參與者和用例從功能需求的分析中就確定了,功能需求具體化為用例,用例通過給參與者提供某個(gè)值的結(jié)果來滿足功能需求。業(yè)務(wù)分析員是選擇首先表識(shí)參與者,然后再表識(shí)用例或者相反。

1.4 用例關(guān)系

用例描述的是系統(tǒng)外部可見的行為,是系統(tǒng)為某一個(gè)或幾個(gè)參與者提供的一段完整服務(wù)[4]。從原則上來講,用例之間都是并列的,它們之間并不存在包含的從屬關(guān)系,但是從保證用例模型的可維護(hù)性和一致性角度來看,可以在用例之間抽象出包含(include)、擴(kuò)展(extend)和泛化 (generalization)這幾種關(guān)系。這幾種關(guān)系都是從現(xiàn)有的用例中抽取出公共的那部分信息,然后通過不同的方法重用這部分公共信息,以減少模型維護(hù)的工作量。

1.5 案例分析

這里分析一個(gè)體液免疫的實(shí)例。體液免疫是由B細(xì)胞介導(dǎo)的免疫應(yīng)答。體液免疫可由胸腺依懶性抗原(TD)和非胸腺依懶性抗原(TI)誘發(fā)。這里討論由TD誘發(fā)的體液免疫。

TD誘發(fā)的體液免疫必須要有抗原遞呈細(xì)胞APC(Antigen Presenting Cell) 和輔助T細(xì)胞(TH細(xì)胞)。TD誘發(fā)的體液免疫過程大致如下:當(dāng)抗原侵入機(jī)體內(nèi)時(shí),抗原遞呈細(xì)胞識(shí)別抗原,并處理和遞呈抗原狀決定族給輔助T細(xì)胞;輔助T細(xì)胞識(shí)別抗原狀決定族,然后把抗原狀決定族傳遞給B細(xì)胞,輔助T細(xì)胞自身活化,增殖分化成效應(yīng)T細(xì)胞;B細(xì)胞接受來自輔助T細(xì)胞的抗原狀決定族,活化并增殖分化為效應(yīng)B細(xì)胞和記憶細(xì)胞;效應(yīng)B細(xì)胞產(chǎn)生抗體,當(dāng)同種抗原再次進(jìn)入機(jī)體時(shí),記憶B細(xì)胞便分化成大量的效應(yīng)B細(xì)胞,進(jìn)而使抗體與抗原結(jié)合,抗體將抗原殺死[6]。

分析上述體液免疫的過程,可以把該軟件系統(tǒng)需要實(shí)現(xiàn)的功能歸結(jié)為以下幾個(gè)問題:

(1)抗原入侵機(jī)體;

(2) 抗原遞呈細(xì)胞攝取抗原;

(3) 抗原遞呈細(xì)胞處理抗原;

(4) 抗原遞呈細(xì)胞遞呈抗原狀決定族給輔助T細(xì)胞;

(5) 輔助T細(xì)胞識(shí)別來自抗原遞呈細(xì)胞傳遞的抗原;

(6) 輔助T細(xì)胞傳遞抗原決定簇給B細(xì)胞;

(7) 輔助T細(xì)胞增殖、分化形成效應(yīng)T細(xì)胞;

(8) B細(xì)胞接受輔助T細(xì)胞的抗原決定簇;

(9) B細(xì)胞增殖、分化形成記憶B細(xì)胞;

(10) B細(xì)胞增殖、分化形成效應(yīng)B細(xì)胞;

(11) 效應(yīng)B細(xì)胞產(chǎn)生抗體;

(12) 記憶B細(xì)胞記憶抗原;

(13)同一種抗原再次進(jìn)入B機(jī)體,記憶B細(xì)胞增殖分化成大量的效應(yīng)B細(xì)胞;

(14) 抗體和抗原結(jié)合殺滅抗原。

根據(jù)上述這些問題,可以把所涉及的操作歸結(jié)為:入侵、識(shí)別、攝取、處理、傳遞、活化、增殖分化、產(chǎn)生、記憶、結(jié)合并殺滅這幾個(gè)方面。根據(jù)這些分析結(jié)果,可以創(chuàng)建以下用例:入侵(Intrusion);攝取(Inhale);處理(Processing);傳遞(Present);活化(Activation);增殖分化(Proliferation and Differentiation);產(chǎn)生(Produce);記憶(Memory);識(shí)別(Recognition);結(jié)合并殺滅(Binding and Kill)。

根據(jù)上述分析,系統(tǒng)的參與者分別為抗原遞呈細(xì)胞(APC);輔助T細(xì)胞(TH);B細(xì)胞(B);抗原(antigen);記憶B細(xì)胞(memory B cell);效應(yīng)B細(xì)胞(effect B cell);抗體(antibody)。

根據(jù)上述分析,可以畫出圖1所示的體液免疫用例圖。

圖1 體液免疫用例圖

這里采用順序圖建立對(duì)象間的動(dòng)態(tài)交互的模型。

由TD介導(dǎo)的體液免疫過程已在上面詳細(xì)描述,由于篇幅限制,體液免疫的順序圖不再列出,但是它的形式化描述將在下面介紹。

2 形式化需求

2.1 形式化B方法的介紹

B方法是形式化方法之一。B方法以規(guī)格說明語言的研究為背景,在引入一些面向?qū)ο髾C(jī)制等特點(diǎn)的同時(shí),保留了語言的優(yōu)點(diǎn)。B方法使用相對(duì)簡(jiǎn)單且運(yùn)用人們熟悉的符號(hào)表示法廣義代換表達(dá)狀態(tài)的轉(zhuǎn)換,從軟件的規(guī)格說明到編碼的形成是一致的形式描述,使程序和程序的規(guī)格說明處于統(tǒng)一的數(shù)學(xué)框架之下,以一種基于集合論的符號(hào)表示法來書寫,減少了出現(xiàn)語義錯(cuò)誤的可能性。這種數(shù)學(xué)框架是通過謂詞變換和擴(kuò)展的最弱前置條件為前提的[6,7]。

B包含一種AMN的結(jié)構(gòu)化機(jī)制,AMN是B方法中的一種基本封裝機(jī)制,非常接近人們?cè)诔绦蛟O(shè)計(jì)中所熟知的一些概念,如類(SIMULA)、抽象數(shù)據(jù)結(jié)構(gòu)(CLUE)、模塊(MODULA-2)、包(ADA)、對(duì)象(EIFFEL)等概念[8,9]。

AMN中有賦值和條件語句,也有前置條件、多重賦值、約束選擇、衛(wèi)、無約束選擇。AMN中沒有定序和循環(huán),理解AMN的根據(jù)是狀態(tài)及改變狀態(tài)的操作,即包括靜態(tài)和動(dòng)態(tài)分析。靜態(tài)對(duì)應(yīng)狀態(tài)的定義,動(dòng)態(tài)對(duì)應(yīng)其操作[10]。

下面通過論述的實(shí)例來獲得體液免疫形式化B的需求。

2.2 用B形式化需求

根據(jù)上述用例圖,定義如下轉(zhuǎn)換規(guī)則[11]:

(1) 所有的參與者用枚舉集合來表示,并把相應(yīng)的變量、不變式等封裝在參與者的機(jī)器里;

(2) 所有的用例用枚舉集合來表示,并把相應(yīng)的變量、不變式等封裝在參與者的機(jī)器里;

(3) 參與者與用例的關(guān)聯(lián)關(guān)系用二元關(guān)系組成的枚舉集合來表示,并把相應(yīng)的變量、不變式等封裝在關(guān)聯(lián)關(guān)系的機(jī)器里。

因?yàn)樵诒纠?沒有參與者與用例的關(guān)聯(lián)關(guān)系,所以不在此列出,方法類似規(guī)則(2)。根據(jù)以上規(guī)則,得出參與者與用例關(guān)聯(lián)關(guān)系的機(jī)器如下:

MACHINE

Association

SETS

ACTOR={Antigen,antibody,TH,B,APC,effect T,effect B,memory B};

USECASE={instrusion,present,processing,recognition,inhale,activation,proliferate,differentiate,producce,memory,bind and kill};

ASSOCIATION={(Antigen,intrusion),(APC,inhale),(APC,present)(APC,processing),(TH,recognition),(TH,present),(TH,activation),(TH,proliferate),(TH,differentiate),(B,recognition),(B,activation ),(B,proliferate ),(B,differentiate ),(effect B,produce),(memory B,memory),(memory B,proliferate),(memory B,differentiate),(antibody,bind and kill)}

VIRIABLES

actor,usecase,association

INVARIANT

actor∈ACTOR∧

usecase∈USECASE∧

association∈ASSOCIATION

INITIALIZATION

actor,usecase,association:={},{},{}

OPERATIONS

…

END

這樣就可以把參與者與用例之間的關(guān)系用形式化B的語言表示出來,而參與者機(jī)器和用例機(jī)器在這里不一一列出。

下面再來看如何把順序圖轉(zhuǎn)換成形式化B的語言,定義以下幾個(gè)規(guī)則:

把順序圖中的對(duì)象用枚舉集合來表示;

把順序圖中對(duì)象之間的操作名用枚舉集合來表示;

把順序圖中對(duì)象之間的操作順序用枚舉集合來表示;

定義常量并對(duì)其設(shè)置前置條件;

定義變量并對(duì)變量設(shè)置不變式;

根據(jù)轉(zhuǎn)換規(guī)則,得到順序圖形式化B的機(jī)器表示形式如下:

MACHINE

ImmuneResponse

SETS

OBJECT={ Antigen,antibody,TH,B,APC,effect T,effect B,memory B };

MESSAGE={ instrusion,present,processing,recognition,inhale,activation,proliferate,differentiate,producce,memory,bind and kill };

MSGID={m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15,m16}

CONSTANTS

ID_max

PROPERIES

ID_max∈NAT1

VARIABLES

object,msgid,msg,sequence

INVARIANT

object∈OBJECT∧msg∈object→MESSAGE∧

msgid∈object→MSGID∧

sequence∈sequence(MSGID)

INITIALIZATION

object,msg,msgid,sequence:= {},{},{},{}

OPERATIONS

Sequence(i1)

PRE i1∈ MESSAGE→msgid∧ i1>=msgid

THEN sequence:=sequence(msgid)

END

END

這里得到了形式化B的規(guī)格說明,避免非形式化需求描述的歧義性,并且形式化的規(guī)則說明易于驗(yàn)證前后的一致性等問題。

3 結(jié) 語

采用基于用例建模的方法進(jìn)行需求獲取。該方法的主要好處是以用戶為中心,用例方法可以使用戶更清楚地認(rèn)識(shí)到新系統(tǒng)允許他們做什么。把用例建模獲取的需求變成形式化B的描述方法,形式化的需求具有無歧義、精確性等優(yōu)點(diǎn),能提高規(guī)格說明的正確性。下一步的工作就是用B方法的證明技術(shù)來驗(yàn)證機(jī)器,并將其精化、程序?qū)崿F(xiàn)。

參考文獻(xiàn)

[1]Zave P.Classification of Research Efforts in Requirements Engineering[J].ACM Computing Surveys,1997,29(4):315-321.

[2]WIegers K E.軟件需求[M].陸莉娜,譯.北京:機(jī)械工業(yè)出版社,2000.

[3]F Martin.UML精粹[M].2版.徐家福,譯.北京:清華大學(xué)出版社,2002.

[4]湯小康,王志剛,曹步文.UML用例圖的Z形式規(guī)范[J].計(jì)算機(jī)與現(xiàn)代化,2006(11):12-13,16.

[5]范曉平.UML建模實(shí)例詳解[M].北京:清華大學(xué)出版社,2005.

[6]陳慰峰.醫(yī)學(xué)免疫學(xué)[M].4版.北京:人民衛(wèi)生出版社,2007.

[7]裘宗燕.B方法[M].北京:電子工業(yè)出版社,2004.

[8]鄒盛榮,陽雪平,郭峰,等.免疫因子網(wǎng)絡(luò)的Immune-B模型設(shè)計(jì)[J].吉首大學(xué)學(xué)報(bào):自然科學(xué)版,2006,27(3):27-32.

[9]Zou Shengrong.Modeling Distributed Algorithm Using B[A].Proceeding of the International Grid and Cooperative Computing Conference[C].2004:683-689.

[10]張志鋒,徐潔,鄧璐娟,等.基于B的UML形式化需求分析[J].計(jì)算機(jī)技術(shù)與發(fā)展,2007,17(8):133-135.

[11]侯麗珍,蔡小娟,鄒恒明.軟件需求的形式化轉(zhuǎn)換模型[J].計(jì)算機(jī)工程,2007,33(5):73-75.