SHF: Small: Data Model Verification for Web Applications

SHF：小型：Web 应用程序的数据模型验证

• 批准号: 1423623
• 负责人: Tevfik Bultan
• 金额: $ 49.99万
• 依托单位: University of California-Santa Barbara
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-07-15 至 2018-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1423623&HistoricalAwards=false
• 关键词: SHF; Small; Data; Model; Verification

A typical web application is a complicated distributed systemthat consists of multiple components that run concurrently on multiplemachines and interact with each other in complex ways via the Internet.As one would expect, developing such software systems is an error-pronetask, and existing software development processes are not robust enoughto produce dependable web applications. The tools developed as part of thisproject could have a broad impact by enable software developers to eliminate programming errors in web applications before they are deployed to end users.The fundamental building block of a web application is the data model thatspecifies the types of objects and the relations among the objects stored bythe application, the constraints on the relations, and the actions that update the data by sending queries to the back-end datastore based on the user input. The project develops techniques that automatically extract a formal model from a given web application that characterizes how its data is storedand modified based on user actions, and infers properties about the formal datamodel. It is then possible to check the inferred properties by converting correctness queries about the data model to queries about satisfiability of logical formulas,and repair the data model to enforce the properties that are expectedto hold.

典型的Web应用程序是一个复杂的分布式系统，它由多个组件组成，这些组件在多个机器上并发运行，并通过Internet以复杂的方式相互作用。正如人们所预期的那样，开发这样的软件系统是一项容易出错的任务，现有的软件开发过程不足以产生可靠的Web应用程序。作为此项目的一部分开发的工具可以产生广泛的影响，使软件开发人员能够在Web应用程序部署到最终用户之前消除它们中的编程错误。Web应用程序的基本构建块是数据模型，该数据模型指定了应用程序存储的对象的类型和对象之间的关系，对关系的约束，以及通过基于用户输入向后端数据存储发送查询来更新数据的操作。该项目开发的技术可以自动从给定的Web应用程序中提取形式模型，该模型描述了其数据是如何根据用户操作存储和修改的，并推断出关于形式数据模型的属性。然后，可以通过将关于数据模型的正确性查询转换为关于逻辑公式的可满足性的查询来检查推断的属性，并修复数据模型以强制执行预期保持的属性。