From UML and OCL to relational logic and back
From UML and OCL to relational logic and back
复制标题
从 UML 和 OCL 到关系逻辑并返回
DOI：
10.1007/978-3-642-33666-9_27
复制
发表时间：
2012
期刊：
影响因子：
2.9
通讯作者：
Martin Gogolla
中科院分区：
文献类型：
--
作者：
Mirco Kuhlmann;Martin Gogolla
UML 和 OCL 等语言用于对系统进行精确建模。因此，复杂的 UML 和 OCL 模型代表了模型驱动开发的关键部分，因为它们正式指定了主要系统属性。因此，创建完整且正确的模型是一个关键问题。为此，我们提供了一种基于高效 SAT 求解技术的轻量级模型验证方法。在本文中，我们提出了从 UML 类图和 OCL 概念到关系逻辑的转换。关系逻辑又代表了基于 SAT 的高级模型实例查找器（如 Kodkod）的来源。本文重点关注一种自然转换方法，旨在通过限制主要 UML 和 OCL 功能的处理来尽可能直接地利用关系逻辑的功能。这种方法使我们能够明确受益于 Kodkod 中关系逻辑的有效处理，并根据 UML 和 OCL 向后解释找到的结果。
Languages like UML and OCL are used to precisely model systems. Complex UML and OCL models therefore represent a crucial part of model-driven development, as they formally specify the main system properties. Consequently, creating complete and correct models is a critical concern. For this purpose, we provide a lightweight model validation method based on efficient SAT solving techniques. In this paper, we present a transformation from UML class diagram and OCL concepts into relational logic. Relational logic in turn represents the source for advanced SAT-based model instance finders like Kodkod. This paper focuses on a natural transformation approach which aims to exploit the features of relational logic as directly as possible through straitening the handling of main UML and OCL features. This approach allows us to explicitly benefit from the efficient handling of relational logic in Kodkod and to interpret found results backwards in terms of UML and OCL.