陳振慶

（賀州學(xué)院 教育技術(shù)中心，廣西 賀州 542899）

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

陳振慶

（賀州學(xué)院 教育技術(shù)中心，廣西 賀州 542899）

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

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

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

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

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

［4］顧明.用例圖的 BNF 描述和擴(kuò)充的基于約束模塊化 Petri網(wǎng)檢測［J］.計(jì)算機(jī)應(yīng)用與軟件，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］.計(jì)算機(jī)科學(xué)，2005，32（3）：2.

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

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

［10］柯昌博，黃志球.云計(jì)算環(huán)境下隱私需求的描述與檢測方法［J］.計(jì)算機(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

［責(zé)任編輯］劉麗英

2017-04-05

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

廣西自然科學(xué)基金項(xiàng)目（2014GXNSFBA118278）。