Software assurance by bounded exhaustive testing
Software assurance by bounded exhaustive testing
复制标题
通过有限的详尽测试来保证软件
DOI：
10.1145/1007512.1007531
复制
发表时间：
2004
影响因子：
7.4
通讯作者：
K. Sullivan
中科院分区：
文献类型：
--
作者：
D. Coppit;Jinlin Yang;S. Khurshid;Wei Le;K. Sullivan
有限的详尽测试（BET）是一种验证技术，在该技术中，将自动测试所有有效输入到指定尺寸范围的软件。在采用结构复杂输入的系统的背景下，出现了一个特别有趣的BET案例。早期研究表明，BET方法可以揭示出具有低结构复杂性输入的小型系统中的故障，但其对具有更复杂输入结构的较大系统的潜在效用尚不清楚。我们着手在一个这样的系统上测试其实用程序。我们使用合金和Testera生成输入来测试伽利略动态故障树分析工具，我们已经对输入空间进行了正式规范，又有测试甲骨文。初步尝试使用我们对合金规范的直接翻译生成输入的尝试并不能很好地工作。发电机未能生成有意义的范围的输入。我们开发了一种方法，其中我们将规范考虑在其中，使用Testera根据一个因素生成抽象输入，并通过后处理器通过后处理器将结果通过，该后处理器从第二个因素中重新调查了信息。使用此技术，我们能够生成对有意义的界限的测试输入，并且输入揭示了伽利略实现，我们的规范和甲骨文中的非平凡故障。我们的结果表明，BET与规范抽象和保理技术相结合，可能成为我们验证工具包的宝贵补充，并有必要进行进一步的研究。
Bounded exhaustive testing (BET) is a verification technique in which software is automatically tested for all valid inputs up to specified size bounds. A particularly interesting case of BET arises in the context of systems that take structurally complex inputs. Early research suggests that the BET approach can reveal faults in small systems with inputs of low structural complexity, but its potential utility for larger systems with more complex input structures remains unclear. We set out to test its utility on one such system. We used Alloy and TestEra to generate inputs to test the Galileo dynamic fault tree analysis tool, for which we already had both a formal specification of the input space and a test oracle. An initial attempt to generate inputs using a straightforward translation of our specification to Alloy did not work well. The generator failed to generate inputs to meaningful bounds. We developed an approach in which we factored the specification, used TestEra to generate abstract inputs based on one factor, and passed the results through a postprocessor that reincorporated information from the second factor. Using this technique, we were able to generate test inputs to meaningful bounds, and the inputs revealed nontrivial faults in the Galileo implementation, our specification, and our oracle. Our results suggest that BET, combined with specification abstraction and factoring techniques, could become a valuable addition to our verification toolkit and that further investigation is warranted.