Checking experiments for stream X-machines

Checking experiments for stream X-machines
复制标题

检查流 X 机的实验

DOI:
10.1016/j.tcs.2010.05.014
复制
发表时间:
2010
期刊:
Theor. Comput. Sci.
影响因子:
--
通讯作者:
R. Hierons
R. Hierons
中科院分区:
--
文献类型:
--
作者:
R. Hierons

文献摘要

被引文献

相似文献

流X机器是一种基于状态的形式主义,它与一个特定的开发过程相关联,在这个过程中,系统是从可信组件构建的。因此,测试主要检查这些组件是否以正确的方式组合,以及它们出现的顺序是否与规范一致。重要的是,有一些测试生成方法返回一个检查实验:只要被测实现(IUT)在功能上等同于给定故障域的未知元素,就保证确定正确性的测试。以前的工作已经表明,如何从有限状态机(FSM)生成检查实验的三种方法可以适用于从流X机测试。然而,还有许多其他方法可以从FSM生成检查实验,并且这些方法具有与不同测试场景相对应的各种好处。本文展示了如何从有限状态机生成检查实验的任何方法都可以适用于生成检查实验,用于针对流X机测试实现。无论我们进行测试以检查IUT在功能上等同于规范,还是我们进行测试以检查IUT的每个跟踪(输入/输出序列)也是非确定性规范的跟踪,情况都是如此。有趣的是,即使所使用的故障域不是传统上与流X机测试相关联的故障域,这也成立。结果也适用于确定性和非确定性的实现。
Stream X-machines are a state based formalism that has associated with it a particular development process in which a system is built from trusted components. Testing thus essentially checks that these components have been combined in a correct manner and that the orders in which they can occur are consistent with the specification. Importantly, there are test generation methods that return a checking experiment: a test that is guaranteed to determine correctness as long as the implementation under test (IUT) is functionally equivalent to an unknown element of a given fault domain Ψ. Previous work has show how three methods for generating checking experiments from a finite state machine (FSM) can be adapted to testing from a stream X-machine. However, there are many other methods for generating checking experiments from an FSM and these have a variety of benefits that correspond to different testing scenarios. This paper shows how any method for generating a checking experiment from an FSM can be adapted to generate a checking experiment for testing an implementation against a stream X-machine. This is the case whether we are testing to check that the IUT is functionally equivalent to a specification or we are testing to check that every trace (input/output sequence) of the IUT is also a trace of a nondeterministic specification. Interestingly, this holds even if the fault domain Ψ used is not that traditionally associated with testing from a stream X-machine. The results also apply for both deterministic and nondeterministic implementations.