SHF: Small: Generation of High-Quality Tests by Treating Tests as Proof Encoding

SHF：小：通过将测试视为证明编码来生成高质量测试

• 批准号: 1117184
• 负责人: Panagiotis Manolios
• 金额: $ 49.53万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-09-01 至 2015-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1117184&HistoricalAwards=false
• 关键词: SHF; Small; Generation; Quality; Tests

Verification is a bottleneck of crisis proportions in the designof the hardware and software systems society depends on. The twomain approaches to verification are formal verification andtesting. Formal verification has the advantage that it rules outthe existence of any logical bugs that violate the propertiesunder consideration. Unfortunately, current formal methods arenot scalable and cannot be directly applied to entire designs. Incontrast, testing is very scalable and is therefore the method ofchoice in practice. The disadvantage of testing is that it doesnot rule out the existence of bugs, and bugs that escape thetesting process can lead to recalls, software crashes, and eventhe loss of life. The research proposed will make testing moreeffective by developing methods of test generation that reducethe probability of missing bugs while simultaneously keeping thenumber of tests generated relatively small.The proposed research is based on the new idea that tests can bethought of as encodings of proofs. This is a fundamentallydifferent way of viewing testing, which is traditionally thoughtof as a method for sampling the space of all possible systembehaviors. The research will explore several potentiallytranformative directions. The first is that one can effectivelygenerate small and complete test sets, i.e., tests sets that ruleout the existence of bugs. Another direction is that testingregimes can be compared by checking to see which lead to testsets that are closest to encoding relevant proofs. A thirddirection is to establish strong connections that bridge the gapbetween formal verification and testing. Finally, the proposedresearch will lead to the development of efficient algorithms fortest generation that will be applied to a range of importantproblems arising in hardware and software verification.

验证是社会所依赖的硬件和软件系统设计中的一个严重瓶颈，验证的两种主要方法是形式验证和测试。形式化验证的优点在于它排除了任何违反所考虑的属性的逻辑错误的存在。不幸的是，目前的形式化方法是不可扩展的，不能直接应用于整个设计。相反，测试是非常可扩展的，因此是实践中的首选方法。测试的缺点是它不能排除bug的存在，而那些逃过测试过程的bug可能会导致召回、软件崩溃，甚至是生命的丧失。拟议的研究将通过开发测试生成方法来降低遗漏错误的可能性，同时保持生成的测试数量相对较小，从而使测试更加有效。拟议的研究基于测试可以被视为证据编码的新想法。这是一种根本不同的看待测试的方式，传统上认为测试是对所有可能的系统行为进行采样的方法。这项研究将探索几个潜在的变革方向。首先是可以有效地生成小而完整的测试集，即，排除错误存在的测试集。另一个方向是，测试制度可以通过检查来比较，看看哪些测试集最接近编码相关的证明。 第三个方向是建立强有力的连接，弥合形式验证和测试之间的差距。最后，提出的研究将导致开发有效的算法测试生成，将适用于一系列的重要问题，在硬件和软件验证。