擴展斷言知識檢驗一致的需求建模方法

郭新峰，馬世龍，呂江花，李睿

（1.山西大學 軟件學院，山西 太原 030013；2. 北京航空航天大學 計算機學院，北京 100191）

?

擴展斷言知識檢驗一致的需求建模方法

郭新峰1，馬世龍2，呂江花2，李睿2

（1.山西大學 軟件學院，山西 太原 030013；2. 北京航空航天大學 計算機學院，北京 100191）

保證需求完整一致是需求建模的關鍵，文中提出一種基于知識庫推理檢驗一致性的需求建模方法，該方法在建模中引入本體以增強表達能力，并結合語義建立約束規則構建需求模型知識庫，基于描述邏輯描述需求和檢驗需求一致性，將需求建模過程作為斷言知識庫的擴展過程，把需求完整性問題轉化為需求一致性問題，并歸結其為規則約束下的可滿足問題。利用Tableau算法等實現需求一致性的檢驗，在整個建?；顒又斜ＷC需求一致。應用實踐中使用自行編制的ROB半自動建模軟件進行需求建模與分析，驗證了建模方法的需求一致性，并通過案例說明了擴展斷言知識庫檢驗一致的需求建模過程。

需求模型；一致性；完整性；多視點；描述邏輯；知識庫；可滿足性；Tableau；需求工程

軟件依據需求而建模，需求建模目的是抽取和驗證需求，以期真實可靠、穩定。需求是人們對真實世界現象的期望，由于人類認識常存在矛盾，需求不一致難以避免：1）需求沖突、語義矛盾；2）需求信息不完整、模糊；3）需求冗余是需求不一致的根本原因[1-2]。目前相關研究有一些成果，如Nuseibeh等提出不一致需求管理框架[3]，認為不一致的需求是不滿足規則的命題，而任何需求建模方法隱含一組檢驗規則；還有一些相關研究是多視點需求建模的不一致管理[4]，認為需求的不一致源自不同角度的認識和表達，從不同視點將系統分解為多個局部視圖，分別獲取需求完整建模，在集成過程中檢測不一致；而王學智等對C4ISR系統能力需求中存在的不一致問題深入分析，構建能力模糊本體，研究了能力需求模型一致性驗證技術[5]。

需求不一致的處理方法主要有：1）邏輯推理證明方法采用帶標記的邏輯公式作為需求表示形式，通過禁止所有平凡推理暫時容忍不一致需求，然后維護需求一致性斷言集并設置需求優先級別，檢測、跟蹤并自動處理不一致需求；2）模型檢驗方法采用狀態變遷作為需求建模原則，并利用模型檢驗技術進行需求不一致性處理；3）基于目標的方法區分了需求不一致的4種程度，包括矛盾、分歧、競爭和障礙，通過檢測和處理分歧解決不一致問題。這些研究成果已有很多應用，在一些特定領域取得很好效果，為相關研究做出很多有益指導，但這一過程對建模人員有較高的知識要求，缺少更接近普通認知的過渡，進一步的應用受到很大限制，其根本原因是不能將易理解方便溝通與高度自動化形式化2個要求統一起來，導致需求模型難以與實際對應，建模理論難以轉換為實際應用，需求分析管理自動化程度和智能化水平不高?；谫Y源、組織與業務的需求模型（requirement model on resources, organization and business, ROB），用人們認識世界的一般方法抽取需求，將數據、角色和功能指稱到描述真實世界的資源、組織與業務，從不同視角基于遞歸分解思想將需求抽象為需求樹，以期確定、完整一致的表達需求。文中在ROB基礎上提出建立ROB知識庫，通過知識推理檢驗需求一致性，并將一致需求增加到斷言知識庫中，形成逐步擴展斷言庫的需求建模方法，保證了需求完整性、一致性。

1 ROB結構

ROB從3個視點（資源、組織與業務）進行需求分析，形成多視點結構：1）業務視點通過分類、分解的方法分析業務以描述功能需求；2）組織視點分析角色權限和人為活動等需求；3）資源視點獲取數據需求。

ROB具有層次結構：1）資源層建立數據模型形成數據需求；2）組織層將參與者抽象為角色，通過權限、關系建立需求模型；3）業務層為真實模擬業務活動過程，從業務分解與協同（角色、資源與業務協作）建立功能需求模型。ROB層次間具有關聯。

ROB基于遞歸分解的思想：1）業務分為復合業務和活動；復合業務由一組更基本的業務構成，這些基本業務之間存在線性、并行等關系，即業務流；活動是最基本的業務，包括角色、資源和API；API定義為五元組，包括前置條件、起始狀態、過程狀態、終止狀態和目標狀態。2）組織分為機構組織和角色；機構組織由更基本的機構組織構成，這些基本組織間存在轄制關系；角色是最基本的組織，角色在特定資源上具有一組操作能力。3）資源分為復合資源和原子資源；復合資源可由更基本的資源構成，這些基本資源可分為主資源和非主資源，二者有確定的函數依賴關系；原子資源是最基本的資源，由一組屬性組成，包括主屬性和非主屬性，主屬性和非主屬性間存在確定的函數依賴關系。ROB將需求抽象為統一的樹形模型，如圖1所示。

2 ROB本體概念體系

從需求理解的角度看，需求工程依賴于人們對現實世界的認識程度，現實世界被抽象為概念與關系，因此在需求工程中引入本體增強了表達能力，在很大程度上滿足了需求分析的要求。本體是相關專題的基本術語和關系，以及利用這些術語和關系構成該專題的規則的集合[6]，本體是領域概念模型的顯示表示[7]。陸汝鈐等將對象和本體結合，提出面向本體的需求分析OORA[8]，此后本體論應用于需求工程的研究有了很大發展，如金芝等提出的基于問題框架的需求建模[9]。

2.1 ROB本體概念層次

本體概念是ROB 建模全過程所有方法及對象分類的概括，主要包括需求任務（Errand）、業務功能（Business）、執行模塊（Task）、業務狀態（State）、組織與角色 （Organization）、資源（Resource）、需求任務類型（ERdType）、資源類型（RscType）和操作類型（OptType）。ROB 本體概念層次結構如圖2所示，T表示ROB 本體概念全域。Errand分為基本簡單任務（Basic）和復合任務（Composite）；Task分為前置模塊（Pretask）和核心模塊（Stage）；State分為前置條件（Precondit）、輸入（Input）、過程（Procedure）、輸出（Output）和后置服務（Postcondi）；Organization分為部門（Department）和角色（Role），Department分為領導（Leader）和員工（Subject）；Resource分為元素（Element）和屬性（Attribute），Element分為主成員（Key）和普通成員（Member）；Attribute 有一組操作權限。

圖2 ROB本體概念層次

2.2 ROB模型本體關系

ROB 本體中概念不是孤立存在的，概念間存在關系，主要包括：1）isA，描述格式為isA （A,B），表示A是B的子類（subclass）；2）hasRsc，描述格式為 hasRsc（A,B），語義解釋為一個A（需求任務/角色/狀態）涉及到一個資源B；3）hasOrg，描述格式為 hasOrg（A,B），語義解釋為一個A（需求任務/狀態）涉及一個組織B；4）hasBusi，描述格式為 hasBusi（A,B），語義解釋為一個基本需求任務A由一個業務功能B實現；5）hasTask，描述格式為 hasTask（A,B），語義解釋為一個復合需求任務A需要分解為一組核心執行模塊B；6）hasErd，描述格式為 hasErd（A,B），語義解釋為一個執行模塊A必須作為一個需求任務B進行分析；7）hasSubR，描述格式為hasSubR（A），語義解釋為一個資源A是一組規模更小的子資源集；8）hasSubO，描述格式為 hasSubO（A），語義解釋為一個組織A是一組規模更小的子組織集；9）hasLead，描述格式為 hasLead（A,B），語義解釋為領導可管轄普通成員；10）hasFuncdep，描述格式為 hasFuncdep（A,B），語義解釋為一個主資源可函數決定一組普通資源；11）hasPremise，描述格式為 hasPremise（A,B），語義解釋為一個核心執行模塊存在必須先執行的一組前置模塊；12）hasCon，描述格式為 hasCon（A,B），語義解釋為業務功能含一前置條件描述；13）hasInt，描述格式為 hasInt（A,B），語義解釋為業務功能含一個輸入描述；14）hasPro，描述格式為 hasPro（A,B），語義解釋為業務功能有一個過程描述；15）hasOut，描述格式為 hasOut（A,B），語義解釋為業務功能含一輸出描述；16）hasPost，描述格式為 hasPost（A,B），語義解釋為業務功能必含一后置結果描述；17）hasType，描述格式為 hasType（A,B），語義解釋為需求任務必有一個任務類型；18）hasErand，描述格式為 hasErand（A,B），語義解釋為角色可參與需求任務；19）hasOpt，描述格式為 hasOpt（A,B），語義解釋為角色可擁有一組操作使用權；20）hasAttr，描述格式為 hasAttr（A,B），語義解釋為每一具體操作是在具體Attribute上的操作；21） hasOptTp，描述格式為 hasOptTp（A,B），語義解釋為每一具體操作有一操作類型。ROB模型本體關系如圖3所示。

圖3 ROB本體關系

3 檢驗一致的需求建模

3.1 描述邏輯語言

計算機作為智能化信息處理工具，需要將信息或程序賦予某種程度的知識語義，并編碼表示；需求富含語義知識，描述邏輯是重要的知識表示工具，用描述邏輯處理需求工程問題是計算智能的一個具體應用。

通過一階邏輯賦予非邏輯方法以形式語義是描述邏輯最初思想[10]。本體是對知識顯示的概念化描述[11]，而描述邏輯是一種本體描述語言[12]。描述邏輯建立在概念和關系之上，有很強的語義表達和推理能力，可用于描述需求，檢測需求一致性。

ALC是最小的命題封閉的描述邏輯[13]語言，在保證推理能力基礎上有很強表達能力，近年來有關描述邏輯語言擴展方面的研究也已有很多，如引入構造子、引入具體域[14-15]。文中采用擴展描述邏輯SHOIN（D），是通用本體語言OWL-DL的邏輯基礎。

描述邏輯基本符號包括：1）原子概念：A；2）概念：C, D；3）全概念T，空概念⊥；4）原子關系：P；5）關系：R；6）概念構造子：,∩,∪；7）量詞：? R., ? R.；8）包含符號：?,?；9）括號：（,）；10）個體：a。根據ROB 描述需求，文中采用描述邏輯SHIQ，SHIQ有如下語法[16]：①C::= A|（T|（⊥|C|C∩D）|C∪D）|?R.C|?R.C| θ_n R|θnR.C|θnR；②R::=P|R|R∩S|R∪S|R°S|R^+ |R^-。

描述邏輯知識庫包括術語公理庫TBox和斷言事實庫ABox。TBox公理公式形如A?C和A?C。ABox包括個體斷言和關系斷言。描述邏輯推理問題包括面向概念的推理和面向個體的推理2類。描述邏輯推理的核心問題是可滿足性問題，所有推理問題可化為可滿足性問題。Tableau算法是判定可滿足性問題有效算法，已得到廣泛應用。目前Tableau算法擴展、復雜性及優化策略等研究已較為深入且有具體應用。

3.2 ROB本體知識庫

ROB本體知識庫包括概念集合（Concept）、關系集合（Association）和規則集合（Constraint）。

1）概念

ROB本體概念表示類，如基本概念ERdType和RscType定義為集合：ERdType::={basic,composite},RscType::={int,float,char,string,struct,enum,*},OptType::={create,insert,delete,update,select}

類含有屬性，這些屬性與相關類關聯，相應概念定義等知識加入到TBox。如，Errand具有屬性hasType關聯ERdType類，而其子類Basic的屬性hasBusi關聯Business，屬性hasRsc關聯Resource，屬性hasOrg關聯Organization。ROB 模型核心概念相應的公式如表1所示。

表1 ROB概念集合Table 1 Concept definition in ROB

2）關系

ROB知識庫中還以描述邏輯刻畫了關系，如關系hasBusi描述為：（? has Busi.Business）?Basic,Basic?（?hasBusi.Business）。表示hasBusi定義域為Basic，而值域為Business。表2列出主要關系。

表2 ROB關系集合Table 2 Associations in ROB

ROB知識庫還包括概念間的子類關系和關系之間的子類關系，描述為公理加入到TBox中，描述邏輯中將子類描述為公式，形如：Composite?Errand，hasPost?hasStat等，表3列出主要子類關系。

表3 ROB子類關系集合Table 3 Included associations in ROB

3）約束

ROB 模型概念和關系必須滿足一組約束，這些約束用于保證需求完整性和一致性。按約束來源可分為概念約束、關系約束和實例約束。

（1）概念約束，限定實例必須的數量，保證概念完整，如：每個需求任務必有一個資源、一個組織和一個功能實現等，表4列出主要的概念約束。

表4 ROB 概念約束Table 4 Numbers constraint on ROB concept

（2）關系約束，限定概念必要的屬性，表示概念必須存在一些關系，如：每個需求任務必對應一組執行模塊，對應一個表示功能過程的狀態等；表5列出了主要關系約束。

（3）實例約束，通過限定實例間的對應關系，保證語義完整和一致性，如：若任務a對應組織b和資源c，而b對應資源d，則d與c是相同實例。表6列出主要的實例約束規則。

表6 ROB 實例約束Table 6 Individual constraints in ROB

4）性質

通過限定實例間關系和性質，建立可推導的公式，約束對應的需求語義沖突，如：hasSub與isA存在互逆性質；ROB 概念、實例間所有性質包括傳遞性（Transitive）、對稱性（Symmetry）、函數關系（Function）和逆關系（inverse）、屬性繼承（Property Inherit）和特性繼承 （Characteristics inherit）。表7列出ROB性質。

表7 ROB性質Table 7 Universal inference-rule in ROB

根據關系性質可構造出更多推導公式，用于推理驗證，以檢查和判定實例斷言可滿足性。

3.3 檢驗一致的需求建模過程

ROB本體知識庫包括概念集合（Concept）、關系集合（Association）和規則集合（Constraint）。

定義1ROB知識庫。ROB知識庫KB={TBox,ABox}，其中TBox術語公理集合包含了ROB概念（表1）、關系（表2、3）、約束（表4～6）公式；ABox是ROB斷言模塊的有限集合。

定義2ROB斷言模塊。ROB斷言模塊是ROB斷言的有限集合，包括概念斷言和角色斷言。如：一個ROB斷言模塊（AssertionBlock）ablock含一組斷言：概念斷言Errand（?e）， 表示e是一個需求任務；Business（?b）， 表示b是一個業務功能； Organization（?o）， 表示o是一個組織； 關系斷言hasSubO（?o,?o1）， 表示組織o中包含規模更小的組織o1。

通過定義ROB本體概念體系以及約束、性質，在描述邏輯中建立知識庫，并將需求建模過程描述為創建ROB斷言模塊的過程，利用描述邏輯推理能力進行一致性檢查和驗證，目的是發現不完整、不一致問題。

性質1完整性。一個ROB斷言模塊若滿足所有概念約束則稱為具有概念完整性；滿足所有關系約束稱具有關系完整性；滿足所有實例約束稱具有實例完整性。一個ROB斷言模塊具有完整性當且僅當同時具有概念完整性、關系完整性和實例完整性。

定義3沖突。對一個ROB知識庫KB K，ROB斷言模塊中任意斷言按ROB性質推導公式，若出現形如R（a,b）∧R（a,b）的推論，即ROB斷言模塊沖突。

性質2一致性。若一個ROB斷言模塊具有完整性，且對知識庫KB K不存在沖突，則稱具有一致性。

ROB需求一致的建模過程是在本體知識庫基礎上不斷擴展斷言知識的過程，下面進行說明：

第一，擴展斷言知識過程描述：1）創建ROB斷言模塊，捕獲需求，根據語義抽取ROB需求對象及聯系，將這些對象、聯系表示為ROB斷言，形成ROB斷言模塊；2）完整性檢查，若具有完整性則進行第3步，否則根據檢查結果增加斷言以擴展ROB斷言模塊，擴展后重新執行第2步完整性檢查；3）一致性檢查，若具有一致性則進行第4步，否則根據檢查結果修改斷言后執行第2步完整性檢查；4）擴展斷言知識。

ROB斷言模塊對應一個在知識庫KB上的解釋（即ROB斷言模塊的一個模型）M1，M1作為新的斷言知識擴展為特定斷言庫ABox A1；ROB斷言模塊具有原子性，一個ROB斷言模塊要么被取消，要么作為斷言知識增加到ABox。

第二，擴展斷言庫過程描述：ROB基于遞歸分解思想反復獲取需求，每次增加新的ROB斷言模塊都對應一模型M，整個建模過程就是一個有限集合：{Mi|i=1,2,…,n}，其中每個元素Mi是一個模型；模型Mi對應特定的斷言庫ABox Ai，可作為模型Mi+1的ABox，與公理知識庫TBox T一起構成Mi+1的完整知識庫。

ROB建模過程不斷創建ROB斷言模塊，經過完整性、一致性檢驗后轉化為斷言知識增加到斷言知識庫，核心工作就是完整性、一致性檢驗。由性質2可知，一致性問題包含完整性問題；一致性檢驗是在ROB知識庫基礎上的推理問題，可轉化為可滿足問題；可滿足問題推理驗證Tableau算法等可參閱文獻[17-20]，文中主要提出ROB需求一致的建模方法，Tableau算法的擴展、復雜性和優化策略等。

4 案例分析

需求建模是一項浩大工程，常需反復迭代。文中在論述理論的基礎上編制了相應的建模分析軟件，提高了ROB建模自動化與智能化水平，本節以一個案例展示ROB需求建模過程。案例：某學校研發智能化綜合實訓管理平臺的需求。

4.1 擴展斷言知識

ROB知識庫中初始ABox A為空，即ABox A0=?。

1）創建ROB斷言模塊

（1）捕獲需求：①項目名稱：智能化綜合實訓管理平臺；②需求單位：某學校；③目標任務：實訓教學教務綜合管理；④項目目的：提高實訓教學質量，提高實訓室管理水平。（2）抽取ROB需求對象個體：t0：實訓室、實訓教學綜合管理；b0：智能化綜合實訓管理平臺；o0：某學校；r0：整體資源；（3）創建ROB斷言模塊：ablock0={Task（t0）,Basic（e0）,Business（b0）,Organization（o0）,Resource（r0）,hasErand（t0,e0）,hasBusi（e0,b0）,hasOrg（e0,o0）,hasRsc（e0,r0）}

2）完整性檢查

遍歷ROB斷言模塊中斷言，應用Tableau算法依次進行完整性檢查，完整性可滿足性問題約束包括：（1）概念完整性約束；（2）關系完整性約束；（3）實例完整性約束。

例如：遍歷ROB斷言模塊ablock0中個體斷言，檢驗對概念約束的可滿足性，由于不滿足Business?≥1hasPro∩≤1hasPro（表4公式⑥），ablock0不具有完整性,添加個體斷言Procedure（p0）以擴展ablock0，即：ablock0=ablock0∪{Procedure（p0）}，然后重新執行完整性檢查。

3）一致性檢查

遍歷ROB斷言模塊中斷言，應用Tableau算法依次判定可滿足性：（1）把TBox帶入到ABox中消除TBox；（2）ABox中斷言轉化為否定正則形；（3）ABox上應用擴展規則直到無可用規則； （4）只要存在解釋， 也就是說只要有一個ABox一致， 則原始ABox一致。

4）擴展斷言知識

將ROB斷言模塊中的所有斷言公式添加到ABox A0中，如：A0=A0∪ablock0；ablock0={Task（t0）,Basic（e0）,Business（b0）,Organization（o0）,Resource（r0）,Procedure（p0）,hasErand（t0,e0）,hasBusi（e0,b0） ,hasOrg（e0,o0）,hasRsc（e0,r0）,hasOrg（p0,o0）,hasRsc（p0,r0）}.

4.2 擴展斷言庫

1）ROB需求分解

ROB建?；痉椒ㄊ欠纸?，每一次分解都對應一組ROB斷言模塊：（1）分解得新需求轉化為ROB需求斷言模塊；（2）分解本身需轉化為ROB斷言模塊。對每一個ROB斷言模塊，都需要經過完整擴展斷言知識（4.1）的過程。

例如，按ROB結構對需求任務e0分解為：t1（實訓教學核心任務）；t2（實訓教學基礎任務）；t3（實訓教學日常任務）。（1）分解得新的需求：①Task（t1）；②Task（t2）；③Task（t3）。分別執行完整的擴展斷言知識的過程；分別對應為有序的斷言知識庫：①ABox A1；②ABox A2；③ABox A3。（2）分解本身是斷言知識：①對應的ROB斷言模塊ablock（decomposed）=（KB-{Basic（e0）}）∪{Composite（e0）}；②完整性檢查，得：ablock（decomposed）= ablock（decomposed）∪{hasTask（e0,t1）,hasTask（e0,t2）,hasTask（e0,t3）}∪{hasPremise（t1,t2）}；③ablock（decomposed）經過一致性檢查和擴展斷言知識后，對應新的斷言知識庫ABox Ade1。

分解說明：①需求分解逐步進行，細化的程度由分析人員確定；②分解的結果作為新需求，擴展為斷言知識的過程是相同的；③重點討論保證一致地建模過程和方法，為論述方便，這里不對詳細分解過程描述。

2）擴展斷言庫

ROB建模過程逐步分解細化需求，不斷產生ROB斷言模塊，每一個ROB斷言模塊經過一致性檢驗和擴展，作為斷言知識增加到知識庫中，在初始知識庫基礎上形成一個新的ABox。從最初對應原始知識庫ABox=?，到分析結束整個過程，形成一個有序的ABox有限集合：ABox Aset={ABox Ai|i=1,2，…,n}，其中每個元素是一個特定的斷言知識庫，Aset記錄了斷言知識庫的擴展過程，表示了需求分析的整個過程，為基于推理的需求管理提供了方便。例如，案例需求分解過程對應一個有序ABox的集合，斷言庫擴展過程如圖4所示。

圖4 需求任務分解案例斷言庫擴展過程

斷言知識庫擴展過程每一步通過斷言知識擴展實現，斷言知識擴展需經過完整性檢查、一致性檢查，保證了完整一致地進行需求分析。

5 結束語

ROB需求建模提取需求分析要素：資源、組織和業務，從這3個視點抽取需求信息，通過演繹分解建立需求樹，分析約束規則消除冗余，將不同視點下的需求樹裝配為完整需求樹。ROB模型引入本體理論，建立概念層次體系，形成概念及關系，進一步結合語義建立了約束與規則，基于描述邏輯構建了需求模型公理知識庫，根據推理規則及公式性質建立了基本的斷言知識庫，ROB需求建模過程不斷建立新的實例斷言，將需求建模過程轉化為斷言知識庫的逐步擴展過程。由于將需求完整問題轉化為需求一致問題，需求一致檢驗歸結為規則約束下的可滿足問題，利用現有研究成果Tableau算法等檢驗，保證了ROB建模的需求一致性。

檢驗一致的ROB需求建模方法借鑒了現有的需求建模技術和觀點，設計了一組規則用于推理、驗證和約束，并基于邏輯知識庫的推理能力實現需求模型的一致性檢驗。目前研究存在一些不足：1）主要關注功能需求而對非功能需求等其他需求問題考慮不足；2）著重于特定需求建模實例和復雜問題的解決，沒有從軟件工程全局設計模型；3）專注于描述邏輯知識庫中邏輯推理問題而對ROB需求分解方法缺乏規范指導，依然依賴于專家經驗；4）由于將需求一致性問題轉化為可滿足問題，而Tableau算法復雜難解。

進一步工作主要有：1）設計合理的實驗，通過實驗分析和數據比對，發現實際可行的有效算法；2）通過專家審議和驗證分析，規范ROB需求分解過程和評估度量體系，以進一步提高建模的自動化程度；3）分析運用非功能需求等其他需求的建模研究成果，從功能需求、非功能需求等擴展ROB模型，形成全面、統一的建模方法；4）分析軟件全生命周期的工作，基于ROB在軟件工程各階段設計相應的工作，以形成完整的需求建模體系，進一步提高軟件工程的自動化智能化水平。

[1]SPANOUDAKIS G, ZISMAN A. Inconsistency management in software engineering: survey and open research issues[M]. Handbook of Software Engineering and Knowledge Engineering. Singapore: World Scientific Publishing Co., 2001: 329-380.

[2]SPANOUDAKIS G, FINKELSTEIN A, TILL D. Overlaps in requirements engineering[J]. Automated Software Engineering, 1999, 6（2）: 171-198.

[3]NUSEIBEH B, EASTERBROOK S, RUSSO A. Leveraging inconsistency in software development[J]. Computer, 2000, 33（4）: 24-29.

[4]NUSEIBEH B, FINKELSTEIN A, KRAMER J. Viewpoints: meaningful relationships are difficult![C] // Proc of the 25th Int’l Conf. on Software Engineering. Portland: IEEE Computer Press, 2003: 676-683.

[5]王智學，董慶超，朱衛星,等．一種支持能力需求概念一致性和合理性分析的方法[J]．計算機學報， 2013， 36（1）： 10-21. WANG Zhixue，DONG Qingchao,ZHU Weixing． An approach for conceptual analysis on capability requirements consistency and reasonability [J]．Chinese Journal of Computers， 2013， 36（1）： 10-21.

[6]NECHES R, FIKES R E, FININ T, et al. Enabling technology for knowledge sharing[J]. AI Magazine, 1991, 12（3）: 36-56.

[7]GRUBER T R. A translation approach to portable ontology specifications[J]. Knowledge Acquisition, 1993, 5（3） : 199-220.

[8]陸汝鈐，金芝，陳剛．面向本體的需求分析[J]．軟件學報，2000，11（8）：1009-1017. LU Ruqian，JIN Zhi，CHEN Gang． Ontology-oriented requirements analysis[J]． Journal of Software, 2000， 11（8）： 1009-1017.

[9]陳小紅，尹斌，金芝．基于問題框架的需求建模：一種本體制導的方法[J]．軟件學報， 2011， 22（2）： 177-194. CHEN Xiaohong，YIN Bin，JIN Zhi． Ontology—guided requirements modeling based on problem frames approach[J]．Journal of Software, 2011， 22（2）： 177-194.

[10]FRANZ B, DIEGO C, DEBORAH L, et al. The description logic handbook: theory, implementation, and applications[M]. New York : Cambridge University Press, 2003: 555-574.

[11]GRUBER T R. A translation approach to portable ontology specifications[J]. Knowledge Acquisition, 1993 , 5（2） : 199-220.

[12]FRANZ B, IAN H, ULRIKE S. Description logics as ontology languages for the semantic web[C]// Mechanizing Mathematical Reasoning: Essays in Honor of JORG H Siekmann on the Occasion of His 60th Birthday, 2005:228-248.

[13]SCHMIDT S, SMOLKA G. Attributive concept descriptions with complements[J]. Artificial Intelligence, 1991.48（1）: 1-26.

[14]常亮，史忠植，陳立民,等．一類擴展的動態描述邏輯[J]．軟件學報， 2010， 21（1）： 1-13. CHANG Liang， SHI Zhongzhi， CHEN Limin, et al． Family of extended dynamic description logics[J]． Journal of Software, 2010， 21（1）： 1-13 .

[15]常亮，史忠植，古天龍,等．可判定的時序動態描述邏輯[J]．軟件學報， 2011， 22（7）： 1524-1537 CHANG Liang， SHI Zhongzhi， GU Tianlong， et al． Decidable Temporal Dynamic Description Logics[J]． Journal of Software， 2011， 22（7）： 1524-1537 .

[16]沈國華，張偉，黃志球,等．基于描述邏輯的特征語義建模及驗證[J]．計算機研究與發展， 2013， 50（7）： 1501-

1512 SHEN Guohua, ZHANG Wei, HUANG Zhiqiu. Description-logic-based feature modeling and verification[J]． Journal of Computer Research and Development, 2013, 50（7）: 1501-1512.

[17]劉全，崔志明，高陽,等．一種邏輯強化學習的tableau推理方法[J]．智能系統學報， 2008, 3（4）： 355-360. LIU Quan,CUI Zhi-ming,GAO Yang, et al. Tableau reasoning method based on logical reinforcement learning[J]． CAAI Transactions on Intelligent Systems, 2008, 3（4）： 355-360.

[18]葉育鑫，歐陽丹彤，劉瑤,等．基于SHOIQ（D）的本體一致性檢測[J]．計算機工程與科學，2009, 31（8）：7-10. YE Yuxin,OUYANG Dantong, LIU Yao, et al. Consistency checking of the SHOIQ（D）-based ontology[J]．Computer Engineering & Science, 2009, 31（8）：7-10.

[19]石蓮，孫吉貴．描述邏輯綜述[J]．計算機科學，2006, 33（1）：194-197. SHI Lian,SUN Jigui. Description Logic Survey[J]．Computer Science，2006, 33（1）：194-197.

[20]古華茂，王勛，凌云，等．完全析取范式群判定 SHOIN（D）-可滿足性[J]．軟件學報，2010, 21（8）：1863-1877. GU Huamao, WANG Xun, LING Yun, et al. Determining the SHOIN（D）-satisfiability with a complete disjunctive normal form group[J]. Journal of Software，2010，21（8）：1863-1877.

郭新峰，男，1974年生，碩士，主要研究方向軟件工程、智能計算及應用。

馬世龍，男，1953年生，教授，博士生導師，博士，主要研究方向為計算機軟件與理論。

呂江花，女，1975年生，副教授，博士后，主要研究方向為計算機軟件與理論。

Extension abox requirements modeling method

GUO Xinfeng1, MA Shilong2, LYU Jianghua2, LI Rui2

（1.College of Software, Shanxi University, Taiyuan 030013, China；2. Computer College, Beihang University, Beijing 100191, China）

Assuring a complete and consistent requirement is the key to requirement modeling. This paper proposes a requirement modeling method for inspecting consistency on the basis of knowledge base reasoning. An ontology is added into the modeling process to improve the expression ability. In addition, the semantic establishment constraint rule is used to build the knowledge base of requirement modeling. The requirement modeling process is taken as an expansion process of the assertion knowledge base based on the consistency among the descriptive logic, descriptive requirement and inspection requirement. The matter of requirement completeness is converted into requirement consistency and attributed to the satisfiability under the constraint by rules. Tableau algorithm is utilized to realize the inspection on requirement consistency, assuring the requirement to be consistent in the entire modeling process. In the application practice, the self-programmed ROB semiautomatic modeling software was applied to requirement modeling and analysis to verify the requirement consistency of the modeling method. In addition, the requirement modeling process on detecting the consistency of an expanded asserted knowledge base was shown by cases.

model; consistency; completeness; multi-view; description logic; knowledge base; satisfiability; Tableau; requirement engineering

2014-09-09.

日期：2015-01-13.

國家自然科學基金資助項目（61300007, 61003016）; 軟件開發環境國家重點實驗室開放基金資助項目（SKLSDE-2012ZX-28,SKLSDE-2013ZX-11）.

郭新峰. E-mail：rjxy_gxf@sxu.edu.cn.

DOI:10.3969/j.issn.1673-4785.201409015

http://www.cnki.net/kcms/doi/10.3969/j.issn.1673-4785.html

TP311

A

1673-4785（2015）01-0081-10

郭新峰，馬世龍，呂江花，等.擴展斷言知識檢驗一致的需求建模方法[J]. 智能系統學報， 2015, 10（1）: 81-89.

英文引用格式：GUO Xinfeng, MA Shilong, LYU Jianghua, et al. Requirement modeling method for inspecting the consistency of the expanded asserted knowledge [J]. CAAI Transactions on Intelligent Systems, 2015, 10（1）: 81-89.