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应用程序。 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. 该项目开发了从给定的Web应用程序中自动提取正式模型的技术，该技术根据用户操作来表征其数据如何存储和修改，并侵入有关正式数据模型的属性。 然后，可以通过将有关数据模型的正确性查询转换为查询逻辑公式的可满足性，并修复数据模型以实施预期持有的属性来检查推断的属性。