Checking experiments for stream X-machines

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.     

Effective database transformation and efficient support computation for mining sequential patterns

In this paper, we propose a novel algorithm for mining frequent sequences from transaction databases. The transactions of the same customers form a set of customer sequences. A sequence (an ordered list of itemsets) is frequent if the number of customer sequences containing it satisfies the user-specified threshold. The 1-sequence is a special type of sequences because it consists of only a single itemset instead of an ordered list, while the k-sequence is a sequence composed of k itemsets. Compared with the cost of mining frequent k-sequences (k ≥ 2), the cost of mining frequent 1-sequences is negligible. We adopt a two-phase architecture to find the two types of frequent sequences separately in order that the discovery of frequent k-sequences can be well designed and optimized. For efficient frequent k-sequence mining, every frequent 1-sequence is encoded as a unique symbol and the database is transformed into one constituted by the symbols. We find that it is unnecessary to encode all the frequent 1-seqences, and make full use of the discovered frequent 1-sequences to transform the database into one with a smaller size. For every k ≥ 2, the customer sequences in the transformed database are scanned to find all the frequent k-sequences. We devise the compact representation for a customer sequence and elaborate the method to enumerate all distinct subsequences from a customer sequence without redundant scans. The soundness of the proposed approach is verified and a number of experiments are performed. The results show that our approach outperforms the previous works in both scalability and execution time.     

Constructing checking sequences for distributed testing

The objective of testing is to determine whether an implementation under test conforms to its specification. In distributed test architectures involving multiple remote testers, this objective can be complicated by the fact that testers may encounter coordination problems relating to controllability (synchronization) and observability during the application of tests. Based on a finite state machine (FSM) specification of the externally observable behaviour of a distributed system and a distinguishing sequence, this paper proposes a method for constructing a checking sequence where there is no potential controllability or observability problems, and where the use of external coordination message exchanges among testers is minimized. The proposed method does not assume a reliable reset feature in the implementations of the given FSM to be tested by the resulting checking sequence. phone: 613-562-5800(Extn)6684 Received May 2004 Revised March 2005 Accepted April 2005 by J. Derrick, M. Harman and R. M. Herons     

基于UIO的协议测试序列生成方法的改进

文章在FSM模型下基于UIO序列的协议测试生成算法的基础上,介绍了UIO(S)序列和IO(S,K)序列的生成算法.并针对在IUT中,会出现UIO(S)和IO(S,K)序列失效的问题,提出了一种有效的检验方法.最后,给出了完整的测试序列生成方法.     

Effective algorithms for constructing minimum cost adaptive distinguishing sequences

Context: Given a Finite State Machine (FSM), a checking sequence is a test sequence that determines whether the system under test is correct as long as certain standard assumptions hold. Many checking sequence generation methods use an adaptive distinguishing sequence (ADS), which is an experiment that distinguishes the states of the specification machine. Furthermore, it has been shown that the use of shorter ADSs yields shorter checking sequences. It is also known, on the other hand, that constructing a minimum cost ADS is an NP-hard problem and it is NP-hard to approximate. This motivates studying and investigating effective ADS construction methods.Objective: The main objective of this paper is to suggest new methods that can compute compact ADSs to be used in the construction of checking sequences.Method: We briefly present the existing ADS construction algorithms. We then propose generalizations of these approaches with a set of heuristics. We also conduct experiments to compare the size of the resultant ADSs and the length of the checking sequences constructed using these ADSs.Results: The results indicate that when the ADSs are constructed with the proposed methods, the length of the checking sequences may reduce up to 54% (40% on the average).Conclusions: In this paper, we present the state of the art ADS construction methods for FSMs and we propose generalizations of these methods. We show that our methods are effective in terms of computation time and ADS quality.     

多单元协议一致性测试中的同步序列的生成

有限状态机模型一般被用来描述通信协议和其它各类的分布式系统,对于一个多端口的有限状态机,需要多个测试单元进行测试,使用一个包括K个（K≥2）测试单元的测试系统可以检查一个多单元通信协议软件的收发行为是否与协议规格一致,在测试过程中,K个测试单元之间可能会出珊步问题,目前,主要是通过增加外部同步操作来解决同步问题,提出了一种新的同步测试序列生成模型－－同步有向图,它可以判断一个给定的协议规格是否可以在不需要外部同步操作的情况下,产生同步测试序列;如果可以产生,则此生成中以将非同步测试相应的同步测试序列;另外此生成模型还可以用来选择为测试系统增加外部同步通道的方法。     

Approximate fixed point sequence for a finite family of asymptotically pseudocontractive mappings

Let E be a real Banach space and K be a nonempty, closed, convex, and bounded subset of E. Let T_i:K→K, i=1,2,…,N, be N uniformly L-Lipschitzian, uniformly asymptotically regular with sequences {ε_n}, and asymptotically pseudocontractive mappings with sequences , where {ε_n} and , i=1,2,…,N, satisfy certain mild conditions. Let a sequence {x_n} be generated from x₁K by

for all integers n1, where T_n=T_n(modN), {u_n} be a sequence in K, and {λ_n}, {θ_n} and {μ_n} are three real sequences in [0,1] satisfying appropriate conditions; then x_n−T_lx_n→0 as n→∞ for each l{1,2,…,N}.     

Testing Conformance to a Quasi-Non-Deterministic Stream X-Machine

Stream X-machines have been used in order to specify a range of systems. One of the strengths of this approach is that, under certain well-defined conditions, it is possible to produce a finite test that is guaranteed to determine the correctness of the implementation under test (IUT). Initially only deterministic stream X-machines were considered in the literature. This is largely because the standard test algorithm relies on the stream X-machine being deterministic. More recently the problem of testing to determine whether the IUT is equivalent to a non-deterministic stream X-machine specification has been tackled. Since non-determinism can be important for specifications, this is an extremely useful extension. In many cases, however, we wish to test for a weaker notion of correctness called conformance. This paper considers a particular form of non-determinism, within stream X-machines, that will be called quasi-non-determinism. It then investigates the generation of tests that are guaranteed to determine whether the IUT conforms to a quasi-non-deterministic stream X-machine specification. The test generation algorithm given is a generalisation of that used for testing from a deterministic stream X-machine. Received November 1999 / Accepted in revised form December 2000     

Bounded Model Checking for Timed Automata

Given a timed automaton M, a linear temporal logic formula φ, and a bound k, bounded model checking for timed automata determines if there is a falsifying path of length k to the hypothesis that M satisfies the specification φ. This problem can be reduced to the satisfiability problem for Boolean constraint formulas over linear arithmetic constraints. We show that bounded model checking for timed automata is complete, and we give lower and upper bounds for the length k of counterexamples. Moreover, we define bounded model checking for networks of timed automata in a compositional way.     

An Overview of Cαml

Cαml is a tool that turns a so-called “binding specification” into an Objective Caml compilation unit. A binding specification resembles an algebraic data type declaration, but also includes information about names and binding. Cαml is meant to help writers of interpreters, compilers, or other programs-that-manipulate-programs deal with α-conversion in a safe and concise style. This paper presents an overview of Cαml's binding specification language and of the code that Cαml produces.     

Fast enumeration algorithm for words with given constraints on run lengths of ones

We propose an algorithm for enumeration and denumeration of words with given constraints on run lengths of ones (dklr-sequences). For large n, operation time of the algorithm (per symbol of a sequence) is at most O(log³ n log log n), where n is the length of enumerated words, whereas for the best known methods it is at least cn, c > 0.     

Discovering Dependencies via Algorithmic Mutual Information: A Case Study in DNA Sequence Comparisons

Algorithmic mutual information is a central concept in algorithmic information theory and may be measured as the difference between independent and joint minimal encoding lengths of objects; it is also a central concept in Chaitin's fascinating mathematical definition of life. We explore applicability of algorithmic mutual information as a tool for discovering dependencies in biology. In order to determine significance of discovered dependencies, we extend the newly proposed algorithmic significance method. The main theorem of the extended method states thatd bits of algorithmic mutual information imply dependency at the significance level 2^–d+O(1). We apply a heuristic version of the method to one of the main problems in DNA and protein sequence comparisons: the problem of deciding whether observed similarity between sequences should be explained by their relatedness or by the mere presence of some shared internal structure, e.g., shared internal repetitive patterns. We take advantage of the fact that mutual information factors out sequence similarity that is due to shared internal structure and thus enables discovery of truly related sequences. In addition to providing a general framework for sequence comparisons, we also propose an efficient way to compare sequences based on their subword composition that does not require any a priori assumptions about k-tuple length.     

Improved bounds on sorting by length-weighted reversals

We study the problem of sorting binary sequences and permutations by length-weighted reversals. We consider a wide class of cost functions, namely f(ℓ)=ℓ^α for all α0, where ℓ is the length of the reversed subsequence. We present tight or nearly tight upper and lower bounds on the worst-case cost of sorting by reversals. Then we develop algorithms to approximate the optimal cost to sort a given input. Furthermore, we give polynomial-time algorithms to determine the optimal reversal sequence for a restricted but interesting class of sequences and cost functions. Our results have direct application in computational biology to the field of comparative genomics.     

On conformance testing of non-deterministic systems

Conformance testing aims at checking if an implementation conforms to its specification. This paper presents the definition of distinguishing sequences of non-deterministic systems. It pro-poses a novel algorithm for derivation of distinguishing sequences in a reduced system based on an observational equivalence. It extends the previous method [2] for dynamic testing of deterministic finite state machines for testing non-deterministic labeled transition systems.     

The identification of nonlinear models for process control using tailored “plant-friendly” input sequences

This paper considers certain practical aspects of the identification of nonlinear empirical models for chemical process dynamics. The primary focus is the identification of second-order Volterra models using input sequences that offer the following three advantages: (1) they are “plant friendly;” (2) they simplify the required computations; (3) they can emphasize certain model parameters over others. To provide a quantitative basis for discussing the first of these advantages, this paper defines a friendliness index f that relates to the number of changes that occur in the sequence. For convenience, this paper also considers an additional nonlinear model structure: the Volterra–Laguerre model. To illustrate the practical utility of the input sequences considered here, second-order Volterra and Volterra–Laguerre models are developed that approximate the dynamics of a first-principles model of methyl methacrylate polymerization.     

Empirical Bayes estimation of the scale parameter in a Pareto distribution

Let f(xθ) = αθ^αx^−(α+1)I(x>θ) be the pdf of a Pareto distribution with known shape parameter α>0, and unknown scale parameter θ. Let {(X_i, θ_i)} be a sequence of independent random pairs, where X_i's are independent with pdf f(xα_i), and θ_i are iid according to an unknown distribution G in a class of distributions whose supports are included in an interval (0, m), where m is a positive finite number. Under some assumption on the class and squared error loss, at (n + 1)th stage we construct a sequence of empirical Bayes estimators of θ_n+1 based on the past n independent observations X₁,…, X_n and the present observation X_n+1. This empirical Bayes estimator is shown to be asymptotically optimal with rate of convergence O(n^−1/2). It is also exhibited that this convergence rate cannot be improved beyond n^−1/2 for the priors in class .     

Heuristics for fault diagnosis when testing from finite state machines

When testing from finite state machines, a failure observed in the implementation under test (IUT) is called a symptom. A symptom could have been caused by an earlier state transfer failure. Transitions that may be used to explain the observed symptoms are called diagnosing candidates. Finding strategies to generate an optimal set of diagnosing candidates that could effectively identify faults in the IUT is of great value in reducing the cost of system development and testing. This paper investigates fault diagnosis when testing from finite state machines and proposes heuristics for fault isolation and identification. The proposed heuristics attempt to lead to a symptom being observed in some shorter test sequences, which helps to reduce the cost of fault isolation and identification. The complexity of the proposed method is analysed. A case study is presented, which shows how the proposed approach assists in fault diagnosis. Copyright © 2006 John Wiley & Sons, Ltd.     

Monitoring Interfaces for Faults

We consider the problem of a module interacting with an external interface (environment) where the interaction is expected to satisfy some system specification Φ. While we have the full implementation details of the module, we are only given a partial external specification for the interface. The interface specification being partial (incomplete) means that the interface displays only a strict subset of the behaviors allowed by the interface specification.Based on the assumption that interface specifications are typically incomplete, we address the question of whether we can tighten the interface specification into a strategy, consistent with the given partial specification, that will guarantee that all possible interactions resulting from possible behaviors of the module will satisfy the system specification Φ. We refer to such a tighter specification as Φ-guaranteeing specification. Rather than verifying whether the interface, which is often an off-the-shelf component, satisfies the tighter specification, the paper proposes a construction of a run-time monitor which continuously checks the existence of a Φ-guaranteeing interface.We view the module and the external interface as players in a 2-player game. The interface has a winning strategy if it can guarantee that no matter what the module does, the overall specification Φ is met. The problem of incomplete specifications is resolved by allowing the interface to follow any strategy consistent with the interface specification. Our approach essentially combines traditional run-time monitoring and static analysis. This allows going beyond the focus of traditional run-time monitoring tools – error detection in the execution trace, towards the focus of the static analysis – bug detection in the programs.     

基于UML时序图的集成测试序列自动生成

该文研究了基于UML时序图的集成测试序列自动生成方法。该方法分析了时序图的语义信息并添加语义约束规约生成可测试模型,从中提取相关信息生成有限状态机;然后使用Wp方法构造测试序列;最后使用中国邮递员算法对Wp方法进行改进生成最优测试序列。该方法生成的测试序列长度相对较短,并能充分满足测试用例覆盖需求。