陳振慶

（賀州學院 教育技術中心，廣西 賀州 542899）

UML用例圖的形式化及其推理

陳振慶

（賀州學院 教育技術中心，廣西 賀州 542899）

UML不是一種完全形式化的面向對象建模語言，不便于進行形式化分析和驗證。文章首先提出了基于描述邏輯的UML用例圖形式化方法，介紹了描述邏輯SHOIN（D）擴展部分的語法和語義，以及UML用例圖各模型元素的SHOIN（D）描述形式。然后把UML用例圖定義為一個二元組，SHOIN（D）知識庫定義為一個三元組，并通過轉化函數(shù)把UML用例圖轉化為SHOIN（D）知識庫，給出了SHOIN（D）知識庫的可滿足性定理及其正確性證明。最后以圖書借還子系統(tǒng)用例圖為例，利用Pellet本體推理機實現(xiàn)了可滿足性、一致性、分類、信息提取和實現(xiàn)性等推理服務。

描述邏輯；UML用例圖；形式化方法；知識庫

［1］許維新，虞慧群.基于 TCOZ 的 UML 用例圖的形式化模型［J］.華東理工大學學報，2004，30（1）：83-85.

［2］湯小康，王志剛，曹步文.UML 用例圖的 Z形式規(guī)范［J］.計算機與現(xiàn)代化，2006，135（11）：13.

［3］段建榮.UML用例圖的Z形式規(guī)范［D］.西安：西安科技大學，2009：39-56.

［4］顧明.用例圖的 BNF 描述和擴充的基于約束模塊化 Petri網(wǎng)檢測［J］.計算機應用與軟件，2005，22（11）：26-27.

［5］Horrocks I，Patel-Schneider PF，Harmelen FV.From SHIQ and RDF to OWL：The making of a Web ontology language［J］.Journal of Web Semantics，2003，1（1）：7-26.

［6］SIRIN E，PARSIA B.Pellet：A Practical OWL-DL reasoner［J］.Journal of Web Semantics，2007，5（2）：51-53.

［7］梅婧，林作銓.從 ALC 到 SHOQ（D）：描述邏輯及其 Tableau 算法［J］.計算機科學，2005，32（3）：2.

［8］陳振慶.基于 SHOIN（D）的 UML類圖形式化方法［J］.計算機工程，2009，35（19）：43.

［9］陳振慶，羅蘭花.基于 OWL 本體的 UML類圖推理［J］.計算機應用與軟件，2011，28（8）：191.

［10］柯昌博，黃志球.云計算環(huán)境下隱私需求的描述與檢測方法［J］.計算機研究與發(fā)展，2015，52（4）：886.

On the Formalization and Reasoning of UML Use Case Diagram

CHEN Zhen-Qing
（Educational Technology Center，Hezhou University，Hezhou Guangxi 542899）

UML is not a completely formalized object-oriented modeling language，so it is not adaptable for formalized analysis and verification.This paper puts forward the UML use case diagram formal method based on description logic，introduces syntax and semantics of description logic SHOIN（D）extension and the description form of every model element in UML use case diagram.Then the paper defines the UML use case diagram as a binary set and SHOIN （D）knowledge base as a triad，transfers UML use case diagram into SHOIN （D）knowledge base by transferring function，and comes up with the satisfiability theorem of the SHOIN（D）knowledge base and the proof of correctness.In the end，taking books circulation subsystem in the graph as an example，inference services are realized as satisfiability，consistency，classification，information extraction，and realizability by pellet ontology reasoning machine.

description logics；UML use case diagram；formal method；knowledge bases

TP182

A

1673—8861（2017）02—0144—05

［責任編輯］劉麗英

2017-04-05

陳振慶（1973-），男，廣西藤縣人，賀州學院副教授，碩士，主研領域：語義網(wǎng)、描述邏輯、軟件工程。

廣西自然科學基金項目（2014GXNSFBA118278）。