Program Verification and Synthesis for Migrating Database Applications

迁移数据库应用程序的程序验证和综合

• 批准号: RGPIN-2022-04983
• 负责人: Wang, Yuepeng
• 金额: $ 1.82万
• 依托单位: Simon Fraser University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=750586
• 关键词: Program; Verification; Synthesis; Migrating; Database

Database applications are ubiquitous in today's software infrastructure and play important roles in many aspects of modern society. Various emerging database systems (e.g., Redis, MongoDB, Neo4j) and cloud database services (e.g., Amazon DynamoDB) bring new challenges for migrating database applications. This research program aims to develop new programming language techniques and tools that facilitate correct, automated, and optimal migrations of database applications. 1. Correctness. To ensure the correctness of the migration process, developers need to verify the database application after the migration is equivalent to, or refinement of, the original version. Motivated by this problem, this research program proposes new verification techniques for checking equivalence and refinement of database applications over relational and non-relational databases. 2. Automation. Since migrating database applications requires lots of manual effort, there is a pressing demand for automating the migration process. This research program presents a novel program synthesis technique that can automatically generate an application over relational, document-oriented, and graph databases. This synthesis technique can significantly reduce the manual effort involved in the migration process and thus improve developer productivity. 3. Optimality. With the proliferation of various kinds of databases, selecting a suitable and performant data model is increasingly challenging because of the trade-offs in relations, JSON documents, graphs, and their combinations. This research proposes a quantitative synthesis technique that can generate an optimal data model based on a given workload and automatically synthesize an optimal database application based on the model. The quantitative synthesis technique can simplify the data modeling procedure and help developers obtain the best database application over an optimal data model. This research program explores programming language techniques for migrating database applications over various databases. It has the potential to open up a new research area that combines programming language research and database research, which can inspire more researchers to make innovative scientific contributions in both fields. In addition, it provides good opportunities to train several PhD and master students in computer science and help them learn cutting-edge technologies and build research skills in programming languages and databases. Finally, the techniques and tools proposed in this research program can potentially benefit a broad spectrum of Canadian companies and organizations that leverage database applications to manage their daily operations or provide services to the public.

数据库应用程序在当今的软件基础设施中无处不在，并在现代社会的许多方面发挥着重要作用。各种新兴的数据库系统（例如，Redis，MongoDB，Neo4j）和云数据库服务（例如，Amazon DynamoDB）为迁移数据库应用程序带来了新的挑战。该研究计划旨在开发新的编程语言技术和工具，以促进数据库应用程序的正确，自动和最佳迁移。1.正确性。为了确保迁移过程的正确性，开发人员需要验证迁移后的数据库应用程序是否等同于或细化了原始版本。出于这个问题，本研究计划提出了新的验证技术，检查等价性和完善的数据库应用程序的关系和非关系数据库。2.自动化.由于迁移数据库应用程序需要大量的手动工作，因此迫切需要自动化迁移过程。本研究计划提出了一种新的程序合成技术，可以自动生成一个应用程序的关系，面向文档和图形数据库。这种合成技术可以显著减少迁移过程中涉及的手动工作，从而提高开发人员的生产力。3.最优性。随着各种数据库的激增，选择合适且高性能的数据模型越来越具有挑战性，因为关系，JSON文档，图形及其组合需要权衡。本研究提出了一种定量的综合技术，可以产生一个最佳的数据模型的基础上，给定的工作量和自动合成的最佳数据库应用程序的基础上。定量综合技术可以简化数据建模过程，帮助开发人员在最佳数据模型上获得最佳的数据库应用。这个研究项目探讨了在各种数据库上迁移数据库应用程序的编程语言技术。它有可能开辟一个新的研究领域，将编程语言研究和数据库研究结合起来，这可以激励更多的研究人员在这两个领域做出创新的科学贡献。此外，它提供了良好的机会，培养几个博士和硕士生在计算机科学，并帮助他们学习尖端技术，建立在编程语言和数据库的研究技能。最后，在这项研究计划中提出的技术和工具可以潜在地受益于广泛的加拿大公司和组织，利用数据库应用程序来管理他们的日常运作或向公众提供服务。