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

A Study of Symmetry Breaking Predicates and Model Counting

DOI：
10.1007/978-3-030-45190-5_7
发表时间：
2020-03-13
期刊：
Tools and Algorithms for the Construction and Analysis of Systems
影响因子：
0
作者：
Wang W;Usman M;Almaawi A;Wang K;Meel KS;Khurshid S
通讯作者：
Khurshid S

Test Input Generation with Java PathFinder: Then and Now (Invited Talk Abstract)

DOI：
10.1145/3213846.3234687
发表时间：
2018-01-01
期刊：
ISSTA'18: PROCEEDINGS OF THE 27TH ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS
影响因子：
0
作者：
Khurshid, Sarfraz;Pasareanu, Corina S.;Visser, Willem
通讯作者：
Visser, Willem