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

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

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

Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method

解决方案枚举抽象：增强轻量级形式方法的建模习惯

DOI：
10.1007/978-3-030-32409-4_21
发表时间：
2019
期刊：
International Conference on Formal Engineering Methods
影响因子：
0
作者：
Sullivan, Allison;Marinov, Darko;Khurshid, Sarfraz
通讯作者：
Khurshid, Sarfraz

A Study of Learning Data Structure Invariants Using Off-the-shelf Tools

使用现成工具学习数据结构不变量的研究

DOI：
10.1007/978-3-030-30923-7_13
发表时间：
2019
期刊：
26th International Symposium on Model Checking Software (SPIN
影响因子：
0
作者：
Usman, Muhammad;Wang, Wenxi;Wang, Kaiyuan;Yelen, Cagdas;Dini, Nima;Khurshid, Sarfraz
通讯作者：
Khurshid, Sarfraz