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文档，图形及其组合的权衡，选择合适且性能的数据模型越来越具有挑战性。本研究提出了一种定量合成技术，该技术可以基于给定的工作量生成最佳数据模型，并自动合成基于模型的最佳数据库应用程序。定量合成技术可以简化数据建模过程，并帮助开发人员通过最佳数据模型获得最佳的数据库应用程序。该研究计划探讨了用于通过各种数据库迁移数据库应用程序的编程语言技术。它有可能开放一个结合了编程语言研究和数据库研究的新研究领域，这可以激发更多的研究人员在这两个领域中做出创新的科学贡献。此外，它提供了培训计算机科学领域的多个博士学位和硕士学生的好机会，并帮助他们学习尖端技术并在编程语言和数据库中建立研究技能。最后，本研究计划中提出的技术和工具可能会受益于利用数据库应用程序来管理其日常运营或向公众提供服务的大量加拿大公司和组织。