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

On the Formalization and Reasoning of UML Use Case Diagram

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

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.