Verifying Equivalence of Database-Driven Applications

TL;DR

This paper introduces a formal approach and a tool for verifying the equivalence of database-driven applications with different schemas, addressing a key challenge in web application refactoring.

Contribution

It formalizes the equivalence checking problem, proposes a bisimulation invariant synthesis technique, and implements a tool that successfully verifies real-world web application benchmarks.

Findings

Successfully verified 20 out of 21 benchmarks

Proposed a novel bisimulation invariant synthesis method

Demonstrated practical applicability on real-world applications

Abstract

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.