权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

SHF: Small: Test-Driven Development and Maintenance of Declarative Models

SHF：小型：声明性模型的测试驱动开发和维护

基本信息

批准号：
1718903
负责人：
Sarfraz Khurshid
金额：
$ 49.55万
依托单位：
University of Texas at Austin
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2017
资助国家：
美国
起止时间：
2017-09-01 至 2022-08-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1718903&HistoricalAwards=false
关键词：
SHF Small Test Driven Development

项目摘要

As software systems become more and more pervasive, developing reliable and dependable systems becomes more and more critical. Software designs, which model high-level, declarative properties of intended systems, hold a key to increasing reliability and dependability. Declarative modeling is not yet a common practice, because writing declarative models correctly is still challenging and a barrier to challenging problem. To remove this impediment to the practical application of declarative (relational) modeling, the project brings software testing concepts, methods, and tool chains to formal specifications based on the Alloy relational modeling system and its underlying satisfiability solving back-ends. Such approaches include unit testing, test generation, the definition and use of coverage metrics to underpin notions of test suite adequacy, and selective regression testing in the face of small changes to specifications.Three primary research thrusts are proposed: to build the foundations of a test-driven approach for declarative models; to define testing techniques to validate the correctness of models that users write; and to introduce sketching techniques that allow users to write incomplete models, which are completed using automated synthesis. The implementation of robust tools and a rigorous experimental evaluation based on controlled experiments and case-studies cross-cuts the research thrusts. The ability to develop correct designs, as envisioned by this project, can lead to a major increase in software reliability and dependability, which can bring substantial economic benefits and significantly improve quality of life.

随着软件系统变得越来越普遍，开发可靠和可依赖的系统变得越来越重要。软件设计是对预期系统的高级声明性属性进行建模，是提高可靠性和可信性的关键。声明性建模还不是一种常见的实践，因为正确地编写声明性模型仍然具有挑战性，并且是挑战问题的障碍。为了消除这一障碍，声明式（关系）建模的实际应用，该项目带来了软件测试的概念，方法和工具链，以正式规范的基础上合金关系建模系统及其底层的可满足性解决后端。这些方法包括单元测试，测试生成，定义和使用覆盖度量来支持测试套件充分性的概念，以及面对规范的小变化的选择性回归测试。并介绍草图技术，使用户能够编写不完整的模型，这是使用自动合成完成。强大的工具和严格的实验评估的基础上控制实验和案例研究的实施交叉研究的推力。开发正确的设计的能力，如本项目所设想的，可以导致软件可靠性和可靠性的大幅提高，这可以带来可观的经济效益，并显着提高生活质量。

项目成果

期刊论文数量（27）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

AlloyMC: Alloy meets model counting

AlloyMC：合金与模型计数的结合

DOI：
10.1145/3368089.3417938
发表时间：
2020
期刊：
Demo Papers (ESEC/FSE Demo 2020
影响因子：
0
作者：
Yang, Jiayi;Wang, Wenxi;Marinov, Darko;Khurshid, Sarfraz
通讯作者：
Khurshid, Sarfraz

Deep Molecular Programming: A Natural Implementation of Binary-Weight ReLU Neural Networks

DOI：
发表时间：
2020-03
期刊：
影响因子：
0
作者：
Marko Vasić;Cameron T. Chalk;S. Khurshid;D. Soloveichik
通讯作者：
Marko Vasić;Cameron T. Chalk;S. Khurshid;D. Soloveichik

TestSage: Regression Test Selection for Large-Scale Web Service Testing

DOI：
10.1109/icst.2019.00052
发表时间：
2019-04
期刊：
2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST)
影响因子：
0
作者：
Hua Zhong;Lingming Zhang;S. Khurshid
通讯作者：
Hua Zhong;Lingming Zhang;S. Khurshid

Automated Model Repair for Alloy

DOI：
10.1145/3238147.3238162
发表时间：
2018-09
期刊：
2018 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE)
影响因子：
0
作者：
Kaiyuan Wang;Allison Sullivan;S. Khurshid
通讯作者：
Kaiyuan Wang;Allison Sullivan;S. Khurshid

A Study of Symmetry Breaking Predicates and Model Counting