FM 2012: Formal Methods
FM 2012: Formal Methods
复制标题
FM 2012：形式化方法
DOI：
10.1007/978-3-642-32759-9_20
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Hierons R
中科院分区：
文献类型：
--
作者：
Hierons R
许多系统通过称为端口的物理分布式接口与其环境进行交互。在测试这样的系统时，我们可能会使用分布式方法，其中每个端口都有一个单独的测试仪。如果测试人员在测试过程中不同步，那么我们就不能总是确定在不同端口观察到的事件的相对顺序，并且已经为分布式测试开发了相应的实现关系。加强实现关系的一种可能方法是测试人员通过交换协调消息来同步，但这需要足够快的通信通道并且会增加测试成本。本文探讨了一种替代方案，其中每个测试人员都有一个本地时钟并为其观察结果添加时间戳。如果我们对本地时钟如何关联一无所知，那么这没有帮助，而如果本地时钟完全一致，那么我们可以重建所做的观察序列。然而，在实践中，我们可能会处于这两个极端之间：本地时钟不会完全一致，但我们对它们如何不同有假设。本文探讨了几种这样的假设并推导了相应的实现关系。
Many systems interact with their environment at physically distributed interfaces called ports. In testing such a system we might use a distributed approach in which there is a separate tester at each port. If the testers do not synchronise during testing then we cannot always determine the relative order of events observed at different ports and corresponding implementation relations have been developed for distributed testing. One possible method for strengthening the implementation relation is for testers to synchronise through exchanging coordination messages but this requires sufficiently fast communications channels and can increase the cost of testing. This paper explores an alternative in which each tester has a local clock and timestamps its observations. If we know nothing about how the local clocks relate then this does not help while if the local clocks agree exactly then we can reconstruct the sequence of observations made. In practice, however, we are likely to be between these extremes: the local clocks will not agree exactly but we have assumptions regarding how they can differ. This paper explores several such assumptions and derives corresponding implementation relations.