SHF: Small: Data Model Verification for Web Applications
SHF: Small: Data Model Verification for Web Applications
批准号:
1423623
负责人:
Tevfik Bultan
金额:
$49.99万
依托单位国家:
美国
项目类别:
Standard Grant
财政年份:
2014
资助国家:
美国
项目状态:
已结题
起止时间:
2014-07-15 至 2018-06-30
中文摘要
一个典型的Web应用程序是一个复杂的分布式系统,它由多个组件组成,这些组件在多台机器上并行运行,并通过Internet以复杂的方式相互交互。正如人们所预料的那样,开发这样的软件系统是一个容易出错的任务,现有的软件开发过程不够健壮,无法产生可靠的Web应用程序。作为该项目的一部分开发的工具可以通过使软件开发人员能够在将Web应用程序部署到最终用户之前消除Web应用程序中的编程错误而产生广泛的影响。Web应用程序的基本构建块是数据模型,该数据模型指定对象的类型以及应用程序存储的对象之间的关系,关系上的约束,以及通过基于用户输入向后端服务器发送查询来更新数据的操作。 该项目开发的技术,自动提取一个正式的模型,从一个给定的Web应用程序,其特点是如何存储和修改的数据基于用户的行动,并推断有关正式的数据模型的属性。 然后,可以通过将关于数据模型的正确性查询转换为关于逻辑公式的可满足性的查询来检查推断的属性,并修复数据模型以强制执行预期保持的属性。
英文摘要
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.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
FMitF: Track I: Scalable and Quantitative Verification for Neural Network Analysis and Design
-
批准号:2124039
-
项目类别:Standard Grant
-
资助金额:$74.92万
-
财政年份:2021
-
负责人:Tevfik Bultan
-
依托单位:
Collaborative Research: SHF: Small: Automated Quantitative Assessment of Testing Difficulty
-
批准号:2008660
-
项目类别:Standard Grant
-
资助金额:$35.97万
-
财政年份:2020
-
负责人:Tevfik Bultan
-
依托单位:
SHF: Medium: Collaborative Research: HUGS: Human-Guided Software Testing and Analysis for Scalable Bug Detection and Repair
-
批准号:1901098
-
项目类别:Continuing Grant
-
资助金额:$40.0万
-
财政年份:2019
-
负责人:Tevfik Bultan
-
依托单位:
SHF: Small: Differential Policy Verification and Repair for Access Control in the Cloud
-
批准号:1817242
-
项目类别:Standard Grant
-
资助金额:$50.0万
-
财政年份:2018
-
负责人:Tevfik Bultan
-
依托单位:
NSF Travel and Attendance Grant Proposal for ISSTA/SPIN 2017
-
批准号:1741648
-
项目类别:Standard Grant
-
资助金额:$0.9万
-
财政年份:2017
-
负责人:Tevfik Bultan
-
依托单位:
EAGER: Collaborative Research: Leveraging Graph Databases for Incremental and Scalable Symbolic Analysis and Verification of Web Applications
-
批准号:1548848
-
项目类别:Standard Grant
-
资助金额:$10.0万
-
财政年份:2015
-
负责人:Tevfik Bultan
-
依托单位:
TC: Small: Collaborative Research: Viewpoints: Discovering Client- and Server-side Input Validation Inconsistencies to Improve Web Application Security
-
批准号:1116967
-
项目类别:Standard Grant
-
资助金额:$30.0万
-
财政年份:2011
-
负责人:Tevfik Bultan
-
依托单位:
SHF: Small: Collaborative Research: Formal Analysis of Distributed Interactions
-
批准号:1117708
-
项目类别:Standard Grant
-
资助金额:$32.86万
-
财政年份:2011
-
负责人:Tevfik Bultan
-
依托单位:
TC: Small:Automata Based String Analysis for Detecting Vulnerabilities in Web Applications
-
批准号:0916112
-
项目类别:Standard Grant
-
资助金额:$35.0万
-
财政年份:2009
-
负责人:Tevfik Bultan
-
依托单位:
SoD-HCER: Design for Verification
-
批准号:0614002
-
项目类别:Standard Grant
-
资助金额:$20.0万
-
财政年份:2006
-
负责人:Tevfik Bultan
-
依托单位:
Reliable Concurrent Software Development Via Reliable Concurrency Controllers
-
批准号:0341365
-
项目类别:Continuing Grant
-
资助金额:$33.6万
-
财政年份:2003
-
负责人:Tevfik Bultan
-
依托单位:
CAREER: Verifiable Specifications: Tools for Reliable Reactive Software Development
-
批准号:9984822
-
项目类别:Continuing Grant
-
资助金额:$20.0万
-
财政年份:2000
-
负责人:Tevfik Bultan
-
依托单位:
A Composite Model Checking Toolset for Analyzing Software Systems
-
批准号:9970976
-
项目类别:Continuing Grant
-
资助金额:$30.0万
-
财政年份:1999
-
负责人:Tevfik Bultan
-
依托单位:
国内基金
海外基金
登录
查看更多内容
昼夜节律性small RNA在血斑形成时间推断中的法医学应用研究
-
批准号:
-
项目类别:省市级项目
-
资助金额:--
-
批准年份:2024
-
负责人:
-
依托单位:
tRNA-derived small RNA上调YBX1/CCL5通路参与硼替佐米诱导慢性疼痛的机制研究
-
批准号:
-
项目类别:省市级项目
-
资助金额:10.0万元
-
批准年份:2022
-
负责人:张祥忠
-
依托单位:
Small RNA调控I-F型CRISPR-Cas适应性免疫性的应答及分子机制
-
批准号:32000033
-
项目类别:青年科学基金项目
-
资助金额:24.0万元
-
批准年份:2020
-
负责人:林平
-
依托单位:
Small RNAs调控解淀粉芽胞杆菌FZB42生防功能的机制研究
-
批准号:31972324
-
项目类别:面上项目
-
资助金额:58.0万元
-
批准年份:2019
-
负责人:高学文
-
依托单位:
变异链球菌small RNAs连接LuxS密度感应与生物膜形成的机制研究
-
批准号:81900988
-
项目类别:青年科学基金项目
-
资助金额:21.0万元
-
批准年份:2019
-
负责人:毛梦莹
-
依托单位:
肠道细菌关键small RNAs在克罗恩病发生发展中的功能和作用机制
-
批准号:31870821
-
项目类别:面上项目
-
资助金额:56.0万元
-
批准年份:2018
-
负责人:陈江宁
-
依托单位:
基于small RNA 测序技术解析鸽分泌鸽乳的分子机制
-
批准号:31802058
-
项目类别:青年科学基金项目
-
资助金额:26.0万元
-
批准年份:2018
-
负责人:麻慧
-
依托单位:
Small RNA介导的DNA甲基化调控的水稻草矮病毒致病机制
-
批准号:31772128
-
项目类别:面上项目
-
资助金额:60.0万元
-
批准年份:2017
-
负责人:吴建国
-
依托单位:
基于small RNA-seq的针灸治疗桥本甲状腺炎的免疫调控机制研究
-
批准号:81704176
-
项目类别:青年科学基金项目
-
资助金额:20.0万元
-
批准年份:2017
-
负责人:赵继梦
-
依托单位:
水稻OsSGS3与OsHEN1调控small RNAs合成及其对抗病性的调节
-
批准号:91640114
-
项目类别:重大研究计划
-
资助金额:85.0万元
-
批准年份:2016
-
负责人:何祖华
-
依托单位: