Reasoning on UML class diagrams

Reasoning on UML class diagrams
复制标题

DOI:
10.1016/j.artint.2005.05.003
复制
发表时间:
2005-10-01
影响因子:
14.4
通讯作者:
De Giacomo, G
De Giacomo, G
中科院分区:
计算机科学2区
文献类型:
--
作者:
Berardi, D;Calvanese, D;De Giacomo, G

文献摘要

被引文献

相似文献

UML是用于软件设计和分析的事实上的标准形式主义。为了支持大规模工业应用的设计,市场上提供了复杂的案例工具,该工具为用户友好的环境提供了编辑,存储和访问多个Unil图。非常需要为此类案例工具配备具有自动推理功能,例如在人工智能中,尤其是在知识代表和推理中研究的功能。这样的功能将允许自动检测UML图的相关形式属性,例如不一致或冗余。关于这个问题,我们考虑UML类图,这是UML最重要的组成部分之一,我们解决了此类图中推理的问题。我们诉诸于知识表示和推理领域中开发的几个结果,关于描述逻辑(DLS),这是一个承认可决定的推理程序的逻辑家庭。我们的第一个贡献是表明,即使在限制性的假设下,UML类图的推理也是指数障碍。我们通过显示DL中推理的多项式减少来证明这一结果。第二个贡献是在UML类图上建立推理的Exptime-Membership,前提是不允许使用任意OCL(一阶)约束。我们通过使用DLRIFD(一种非常表现力的exptime DL,可以捕获概念性和面向对象的数据模型的典型特征)来获得此结果。 NE的最后贡献具有更实用的风味,包括对DL Alcqi中UML类图的多项式编码,该编码本质上是最具表现力的DL,由当前的基于DL的最新基于DL的推理系统支持。虽然不如DLRIFD表现力,但DL ALC Qi保留了足够的语义,以保持有关UML类图的推理声音和完整。利用这种编码,可以将当前基于DL的推理系统用作下一代案例工具的核心推理引擎,这些案例工具配备了UML类图上的推理功能。 (c)2005 Elsevier B.V.保留所有权利。
UML is the de-facto standard formalism for software design and analysis. To support the design of large-scale industrial applications, sophisticated CASE tools are available on the market, that provide a user-friendly environment for editing, storing, and accessing multiple UNIL diagrams. It would be highly desirable to equip such CASE tools with automated reasoning capabilities, such as those studied in Artificial Intelligence and, in particular, in Knowledge Representation and Reasoning. Such capabilities would allow to automatically detect relevant formal properties of UML diagrams, such as inconsistencies or redundancies. With regard to this issue, we consider UML class diagrams, which are one of the most important components of UML, and we address the problem of reasoning on such diagrams. We resort to several results developed in the field of Knowledge Representation and Reasoning, regarding Description Logics (DLs), a family of logics that admit decidable reasoning procedures. Our first contribution is to show that reasoning on UML class diagrams is EXPTIME-hard, even under restrictive assumptions; we prove this result by showing a polynomial reduction from reasoning in DLs. The second contribution consists in establishing EXPTIME-membership of reasoning on UML class diagrams, provided that the use of arbitrary OCL (first-order) constraints is disallowed. We get this result by using DLRifd, a very expressive EXPTIME-decidable DL that has been developed to capture typical features of conceptual and object-oriented data models. ne last contribution has a more practical flavor, and consists in a polynomial encoding of UML class diagrams in the DL ALCQI, which essentially is the most expressive DL supported by current state-of-the-art DL-based reasoning systems. Though less expressive than DLRifd, the DL ALC QI preserves enough semantics to keep reasoning about UML class diagrams sound and complete. Exploiting such an encoding, one can use current DL-based reasoning systems as core reasoning engines for a next generation of CASE tools, that are equipped with reasoning capabilities on UML class diagrams. (c) 2005 Elsevier B.V. All rights reserved.