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

陈振庆

（贺州学院 教育技术中心，广西 贺州 542899）

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

陈振庆

（贺州学院 教育技术中心，广西 贺州 542899）

UML不是一种完全形式化的面向对象建模语言，不便于进行形式化分析和验证。文章首先提出了基于描述逻辑的UML用例图形式化方法，介绍了描述逻辑SHOIN（D）扩展部分的语法和语义，以及UML用例图各模型元素的SHOIN（D）描述形式。然后把UML用例图定义为一个二元组，SHOIN（D）知识库定义为一个三元组，并通过转化函数把UML用例图转化为SHOIN（D）知识库，给出了SHOIN（D）知识库的可满足性定理及其正确性证明。最后以图书借还子系统用例图为例，利用Pellet本体推理机实现了可满足性、一致性、分类、信息提取和实现性等推理服务。

描述逻辑；UML用例图；形式化方法；知识库

［1］许维新，虞慧群.基于 TCOZ 的 UML 用例图的形式化模型［J］.华东理工大学学报，2004，30（1）：83-85.

［2］汤小康，王志刚，曹步文.UML 用例图的 Z形式规范［J］.计算机与现代化，2006，135（11）：13.

［3］段建荣.UML用例图的Z形式规范［D］.西安：西安科技大学，2009：39-56.

［4］顾明.用例图的 BNF 描述和扩充的基于约束模块化 Petri网检测［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］柯昌博，黄志球.云计算环境下隐私需求的描述与检测方法［J］.计算机研究与发展，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-），男，广西藤县人，贺州学院副教授，硕士，主研领域：语义网、描述逻辑、软件工程。

广西自然科学基金项目（2014GXNSFBA118278）。