軟件需求獲取形式化的案例研究

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

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

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

中圖分類號:TP309文獻標識碼:A

文章編號: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 引 言

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

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

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

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

1.1 用例模型

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

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

1.2 用例

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

1.3 參與者

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

1.4 用例關(guān)系

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

1.5 案例分析

這里分析一個體液免疫的實例。體液免疫是由B細胞介導的免疫應答。體液免疫可由胸腺依懶性抗原(TD)和非胸腺依懶性抗原(TI)誘發(fā)。這里討論由TD誘發(fā)的體液免疫。

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

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

(1)抗原入侵機體;

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

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

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

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

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

(7) 輔助T細胞增殖、分化形成效應T細胞;

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

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

(10) B細胞增殖、分化形成效應B細胞;

(11) 效應B細胞產(chǎn)生抗體;

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

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

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

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

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

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

圖1 體液免疫用例圖

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

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

2 形式化需求

2.1 形式化B方法的介紹

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

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

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

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

2.2 用B形式化需求

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

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

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

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

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

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的語言表示出來,而參與者機器和用例機器在這里不一一列出。

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

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

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

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

定義常量并對其設置前置條件;

定義變量并對變量設置不變式;

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

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ī)則說明易于驗證前后的一致性等問題。

3 結(jié) 語

采用基于用例建模的方法進行需求獲取。該方法的主要好處是以用戶為中心,用例方法可以使用戶更清楚地認識到新系統(tǒng)允許他們做什么。把用例建模獲取的需求變成形式化B的描述方法,形式化的需求具有無歧義、精確性等優(yōu)點,能提高規(guī)格說明的正確性。下一步的工作就是用B方法的證明技術(shù)來驗證機器,并將其精化、程序?qū)崿F(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].陸莉娜,譯.北京:機械工業(yè)出版社,2000.

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

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

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

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

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

[8]鄒盛榮,陽雪平,郭峰,等.免疫因子網(wǎng)絡的Immune-B模型設計[J].吉首大學學報:自然科學版,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].計算機技術(shù)與發(fā)展,2007,17(8):133-135.

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