Verifying equivalence of database-driven applications
Verifying equivalence of database-driven applications
复制标题
验证数据库驱动应用程序的等效性
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
W. Cook
中科院分区：
文献类型：
--
作者：
Yuepeng Wang;Işıl Dillig;Shuvendu K. Lahiri;W. Cook
本文解决了在不同模式的数据库上运行的一对程序之间验证等价性的问题。这个问题在web应用程序的上下文中尤为重要，因为web应用程序通常会因为性能或可维护性原因而进行数据库重构。虽然web应用程序在模式迁移之前和之后应该具有相同的外部可观察行为，但没有现有的工具来证明这些程序的等价性。本文通过形式化数据库驱动应用程序的等价性和精化检查问题，迈出了解决这个问题的第一步。我们还提出了一种基于关系代数上具有更新的双模拟不变量概念的证明方法，并描述了一种合成这种双模拟不变量的技术。我们已经在一个名为Mediator的工具中实现了所提出的技术，用于验证用我们的中间语言编写的数据库驱动的应用程序之间的等价性，并在从教科书和实际web应用程序中提取的21个基准上评估我们的工具。我们的结果表明，所提出的方法可以成功地验证这些基准中的20个。
This paper addresses the problem of verifying equivalence between a pair of programs that operate over databases with different schemas. This problem is particularly important in the context of web applications, which typically undergo database refactoring either for performance or maintainability reasons. While web applications should have the same externally observable behavior before and after schema migration, there are no existing tools for proving equivalence of such programs. This paper takes a first step towards solving this problem by formalizing the equivalence and refinement checking problems for database-driven applications. We also propose a proof methodology based on the notion of bisimulation invariants over relational algebra with updates and describe a technique for synthesizing such bisimulation invariants. We have implemented the proposed technique in a tool called Mediator for verifying equivalence between database-driven applications written in our intermediate language and evaluate our tool on 21 benchmarks extracted from textbooks and real-world web applications. Our results show that the proposed methodology can successfully verify 20 of these benchmarks.