基于时序逻辑规范的自适应测试策略综合
Synthesizing Adaptive Test Strategies from Temporal Logic Specifications
摘要：
构造好的测试用例是困难和耗时的，特别是当被测系统仍在开发中，其确切行为尚未确定时。我们提出了一种新的方法来计算测试策略的反应式系统从一个给定的时序逻辑规范，使用形式化的方法。计算的策略保证揭示某些简单的故障在每个实现的规范和系统的环境的不可控部分的每一个行为。所提出的方法支持不同的假设发生的故障（从一个单一的瞬态故障到持续故障），并在默认情况下，旨在揭示最弱的。基于完善的假设，基于故障的测试，我们认为，这样的测试也是敏感的更复杂的错误。由于规范可能没有完全定义系统的行为，我们使用反应式合成算法与部分信息。计算的策略是自适应的测试策略，在运行时的行为作出反应。我们制定了自适应测试策略综合的基本理论，并提出了一个真实世界的卫星系统的安全关键部件的实验。我们证明，我们的方法可以应用于工业规格，合成的测试策略是能够检测到的错误，很难检测到随机测试。
英文摘要：
Constructing good test cases is difficult and time-consuming, especially if the system under test is still under development and its exact behavior is not yet fixed. We propose a new approach to compute test strategies for reactive systems from a given temporal logic specification using formal methods. The computed strategies are guaranteed to reveal certain simple faults in every realization of the specification and for every behavior of the uncontrollable part of the system's environment. The proposed approach supports different assumptions on occurrences of faults (ranging from a single transient fault to a persistent fault) and by default aims at unveiling the weakest one. Based on well-established hypotheses from fault-based testing, we argue that such tests are also sensitive for more complex bugs. Since the specification may not define the system behavior completely, we use reactive synthesis algorithms with partial information. The computed strategies are adaptive test strategies that react to behavior at runtime. We work out the underlying theory of adaptive test strategy synthesis and present experiments for a safety-critical component of a real-world satellite system. We demonstrate that our approach can be applied to industrial specifications and that the synthesized test strategies are capable of detecting bugs that are hard to detect with random testing.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
