arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2403.18599cs.DB
收藏

证明OCL约束的SQL实现的正确性

Proving correctness for SQL implementations of OCL constraints

Hoang Nguyen, Manuel Clavel

AI总结:

本文提出一种基于模型的方法,通过将SQL子集和OCL映射到多类一阶逻辑,利用SMT求解器自动证明手动编写的OCL约束SQL实现的正确性,并给出示例和工具支持。

摘要:

在以模型驱动开发数据密集型应用的背景下,OCL约束在提高源模型(如数据模型和安全模型)的精确性方面发挥着重要作用。目前已提出多种代码生成器,以弥合带有OCL约束的源模型与其对应数据库实现之间的鸿沟。然而,从执行时间性能的角度来看,这些代码生成器生成的数据库查询远不如数据库专家手动编写的实现高效。在本文中,我们提出了一种不同的方法来弥合带有OCL约束的模型与其对应数据库实现之间的鸿沟。具体而言,我们引入了一种基于模型的方法论,用于证明手动编写的OCL约束的SQL实现的正确性。该方法论基于一种新颖的映射,将SQL语言的一个重要子集映射到多类一阶逻辑。此外,通过利用已有的从OCL语言到多类一阶逻辑的映射,我们可以使用SMT求解器自动证明OCL约束的SQL实现的正确性。为了说明并展示我们方法的适用性,我们在文中包含了一些非平凡的示例。最后,我们报告了支持我们方法的一套工具的状态。

英文摘要:

In the context of the model-driven development of data-centric applications, OCL constraints play a major role in adding precision to the source models (e.g., data models and security models). Several code-generators have been proposed to bridge the gap between source models with OCL constraints and their corresponding database implementations. However, the database queries produced by these code-generators are significantly less efficient -- from the point of view of execution-time performance -- than the implementations manually written by database experts. In this paper, we propose a different approach to bridge the gap between models with OCL constraints and their corresponding database implementations. In particular, we introduce a model-based methodology for proving the correctness of manually written SQL implementations of OCL constraints. This methodology is based on a novel mapping from a significant subset of the SQL language into many-sorted first-order logic. Moreover, by leveraging on an already existing mapping from the OCL language into many-sorted first-order logic, we can use SMT solvers to automatically prove the correctness of SQL implementations of OCL constraints. To illustrate and show the applicability of our approach, we include in the paper a number of non-trivial examples. Finally, we report on the status of a suite of tools supporting our approach.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑