SUMMARY Dependence analysis on an Extended Finite State Machine representation of the requirements of a system under test identifies various types of control and data dependencies between transitions caused by a set of modifications on the requirements. These particular types of dependencies capture the effects of the modifications, that is, their direct effects on the changed parts of the system and their side effects on the unchanged parts of the system. Recent work on model‐based regression testing shows that dependencies capturing direct effects and side effects of the changes made on the requirements can be used for regression test suite (RTS) reduction (reducing the size of a given test suite by eliminating redundancies), for RTS prioritization (ordering test cases in a given test suite for early fault detection), or for RTS generation (designing a test suite covering the identified dependencies). This paper proposes an additional use of such dependencies, namely, RTS selection, which is the process of selecting a subset of a given test suite to form an RTS by considering the coverage of dependencies related to the effects of the modifications. The dependencies marked during this process as uncovered provide a basis for augmenting an (incomplete) RTS with test cases covering uncovered dependencies. Copyright © 2012 John Wiley & Sons, Ltd.

Dependence analysis on an Extended Finite State Machine (EFSM) representation of the requirements of a system under test has been used in requirements-based regression testing for regression test suite (RTS) reduction (reducing the size of a given test suite by eliminating redundancies), for RTS prioritization (ordering test cases in a given test suite for early fault detection) or for RTS selection (selecting a subset of a test suite covering the identified dependencies). These particular uses of dependence analysis are based on definitions of various types of control and data dependencies (between transitions in an EFSM) caused by a given set of modifications on the requirements. This abstract considers the definitions of data dependencies, gives examples of incompleteness of existing definitions, and presents insights on completing these definitions.

SUMMARY During regression testing, a modified system is often retested using an existing test suite. Since the size of the test suite may be very large, testers are interested in detecting faults in the modified system as early as possible during this retesting process. Test prioritization attempts to order tests for execution so that the chances of early detection of faults during retesting are increased. The existing prioritization methods are based on the source code of the system under test. In this paper, we present and evaluate two model‐based selective methods and a dependence‐based method of test prioritization utilizing the state‐based model of the system under test. These methods assume that the modifications are made both on the system under test and its model. The existing test suite is executed on the system model and information about this execution is used to prioritize tests. Execution of the model is inexpensive as compared with execution of the system under test; therefore, the overhead associated with test prioritization is relatively small. In addition, we present an analytical framework for evaluation of test prioritization methods. This framework may reduce the cost of evaluation as compared with the framework that is based on observation. We have performed an empirical study in which we compared different test prioritization methods. The results of the empirical study suggest that system models may improve the effectiveness of test prioritization with respect to early fault detection. Copyright © 2011 John Wiley & Sons, Ltd.

Abstract Lower bounds on the lengths of checking sequences constructed for testing from Finite State Machine-based specifications are established. These bounds consider the case where a distinguishing sequence is used in forming state recognition and transition verification subsequences and identify the effects of overlapping among such subsequences. Empirical results show that the existing methods for construction of checking sequences provide checking sequences with lengths that are within acceptable distance to these lower bounds.

Methods for testing from finite state machine-based specifications often require the existence of a preset distinguishing sequence for constructing checking sequences. It has been shown that an adaptive distinguishing sequence is sufficient for these methods. This result is significant because adaptive distinguishing sequences are strictly more common and up to exponentially shorter than preset ones. However, there has been no study on the actual effect of using adaptive distinguishing sequences on the length of checking sequences. This paper describes experiments that show that checking sequences constructed using adaptive distinguishing sequences are almost consistently shorter than those based on preset distinguishing sequences. This is investigated for three different checking sequence generation methods and the results obtained from an extensive experimental study are given.

We consider the problem of update processing in a peer-to-peer (P2P) database network where each peer consists of an independently created relational database. We assume that peers store related data, but data has heterogeneity wrt instances and schemas. The differences in schema and data vocabulary are bridged by value correspondences called mapping tables. Peers build an overlay network called acquaintance network, in which each peer may get acquainted with any other peer that stores related data. In this setting, the updates are free to initiate in any peer and are executed over other peers which are acquainted directly or indirectly with the updates initiator. The execution of an update is achieved by translating, through mapping tables, the update into a set of updates that are executed against the acquainted peers. We consider both the soundness and completeness of update translation. When updates are generated and propagated in the network initiated from a peer, a tree is built dynamically called Update Dependency Tree (UDT). The UDT depicts the relationships among the component updates generated from the initial update. We also discuss the issues of the update propagation when a peer is temporarily unavailable or offline. Our propagation mechanism keeps track of a peer when the peer is not available for a certain period of time and once the peer comes back online the system propagates the updates destined to the returning peer to keep it's database synchronized. Moreover, conflict detection and resolution strategies have been proposed for such a dynamic P2P database network. We have implemented and experimentally tested a prototype of our update processing mechanism on a small P2P database network. We show the results of our experiments.

Abstract This paper proposes a model‐based regression test suite reduction method. The proposed method considers an SDL model representing the requirements of a system under test and a set of modifications on this model, applies dependence analysis to identify interaction patterns related to each type of modifications, i.e., adding, deleting, and changing transitions in the SDL model, and reduces the size of a given regression test suite by examining interaction patterns covered by each test case in the test suite. Results of empirical studies are reported. Copyright © 2009 John Wiley & Sons, Ltd.

There has been much interest in testing from finite-state machines (FSMs). If the system under test can be modelled by the (minimal) FSM N then testing from an (minimal) FSM M is testing to check that N is isomorphic to M. In the distributed test architecture, there are multiple interfaces/ports and there is a tester at each port. This can introduce controllability/synchronization and observability problems. This paper shows that the restriction to test sequences that do not cause controllability problems and the inability to observe the global behaviour in the distributed test architecture, and thus relying only on the local behaviour at remote testers, introduces fundamental limitations into testing. There exist minimal FSMs that are not equivalent, and so are not isomorphic, and yet cannot be distinguished by testing in this architecture without introducing controllability problems. Similarly, an FSM may have non-equivalent states that cannot be distinguished in the distributed test architecture without causing controllability problems: these are said to be locally s-equivalent and otherwise they are locally s-distinguishable. This paper introduces the notion of two states or FSMs being locally s-equivalent and formalizes the power of testing in the distributed test architecture in terms of local s-equivalence. It introduces a polynomial time algorithm that, given an FSM M, determines which states of M are locally s-equivalent and produces minimal length input sequences that locally s-distinguish states that are not locally s-equivalent. An FSM is locally s-minimal if it has no pair of locally s-equivalent states. This paper gives an algorithm that takes an FSM M and returns a locally s-minimal FSM M′ that is locally s-equivalent to M.

Abstract 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.

Abstract Existing distributed delay constrained multicast routing algorithms construct a multicast tree in a sequential fashion and need to be restarted when failures occur during the multicast tree construction phase or during an on‐going multicast session. This article proposes an efficient distributed delay constrained multicast routing algorithm that constructs a multicast tree in a concurrent fashion by taking advantage of the concurrency in the underlying distributed computation. The proposed algorithm has a message complexity of O(mn) and time complexity of O(n) in the worst case, wheremis the number of destinations andnis the number of nodes in the network. It constructs multicast trees with the same tree costs as the ones constructed by well‐known algorithms such as DKPP and DSHP while utilizing 409 to 1734 times fewer messages and 56 to 364 times less time than these algorithms under comparable success rate ratios. The proposed algorithm has been augmented with a fault recovery mechanism that efficiently constructs a multicast tree when failures occur during the tree construction phase and recovers from any failure in the multicast tree during an on‐going multicast session without interrupting the running traffic on the unaffected portion of the tree. © 2005 Wiley Periodicals, Inc. NETWORKS, Vol. 47(1), 37–51 2006

A checking sequence, generated from a finite state machine, is a test sequence that is guaranteed to lead to a failure if the system under test is faulty and has no more states than the specification. The problem of generating a checking sequence for a finite state machine M is simplified if M has a distinguishing sequence: an input sequence D~ with the property that the output sequence produced by M in response to D is different for the different states of M. Previous work has shown that, where a distinguishing sequence is known, an efficient checking sequence can be produced from the elements of a set A of sequences that verify the distinguishing sequence used and the elements of a set /spl gamma/ of subsequences that test the individual transitions by following each transition t by the distinguishing sequence that verifies the final state of t. In this previous work, A is a predefined set and /spl gamma/ is defined in terms of A. The checking sequence is produced by connecting the elements of /spl gamma/ and A to form a single sequence, using a predefined acyclic set E/sub c/ of transitions. An optimization algorithm is used in order to produce the shortest such checking sequence that can be generated on the basis of the given A and E/sub c/. However, this previous work did not state how the sets A and E/sub c/ should be chosen. This paper investigates the problem of finding appropriate A and E/sub c/ to be used in checking sequence generation. We show how a set A may be chosen so that it minimizes the sum of the lengths of the sequences to be combined. Further, we show that the optimization step, in the checking sequence generation algorithm, may be adapted so that it generates the optimal E/sub c/. Experiments are used to evaluate the proposed method.

This paper presents a model checking-based approach to dataflow testing. We characterize dataflow oriented coverage criteria in temporal logic such that the problem of test generation is reduced to the problem of finding witnesses for a set of temporal logic formulas. The capability of model checkers to construct witnesses and counterexamples allows test generation to be fully automatic. We discuss complexity issues in minimal cost test generation and describe heuristic test generation algorithms. We illustrate our approach using CTL as temporal logic and SMV as model checker.

The problem of testing from an extended finite state machine (EFSM) is complicated by the presence of infeasible paths. This paper considers the problem of expanding an EFSM in order to bypass the infeasible path problem. The approach is developed for the specification language SDL but, in order to aid generality, the rewriting process is broken down into two phases: producing a normal form EFSM (NF-EFSM) from an SDL specification and then expanding this NF-EFSM.

Reverse engineering in distributed systems is essential to recovering the designs of large and complex distributed systems that evolve often without proper documentation. This paper proposes rules for the automated construction of deadlock-free designs of communication protocols from the execution histories of existing systems, defines the properties of the constructed designs and identifies the conditions for a constructed design to be equivalent to the presumed design implied by the given set of global observations.

Here, the method proposed by Ural, Wu and Zhang (1997) for constructing minimal-length checking sequences based on distinguishing sequences is improved. The improvement is based on optimizations of the state recognition sequences and their use in constructing test segments. It is shown that the proposed improvement further reduces the length of checking sequences produced from minimal, completely specified, and deterministic finite state machines.

This paper presents a method for the selection of test sequences from statecharts. It is shown that a statechart can be transformed into a flow graph modelling the flow of both control and data in the statechart. The transformation enables the application of conventional control and data flow analysis techniques to test sequence selection from statecharts. The resulting set of test sequences provides the capability of determining whether an implementation establishes the desired flow of control and data expressed in statecharts. Copyright © 2000 John Wiley & Sons, Ltd.

State explosion is well-known to be the principle limitation in protocol verification. In this paper, leaping reachability analysis (LRA) is advocated as an incremental improvement of a verification technique called simultaneous reachability analysis (SRA) to tackle state explosion. SRA is a relief strategy for the verification of progress properties of protocols modeled as networks of communicating finite state machines (CFSMs) without any topological or structural constraints. The improvement is a uniform and property-driven relief strategy which proves to be adequate for detecting all deadlocks, all non-executable transitions, all unspecified receptions and all buffer overflows in a protocol specified in the CFSM model. Experiments show that LRA can largely relieve the state explosion problem by reducing the amount of storage space and execution time required for verification.

Partial-order reduction methods form a collection of state exploration techniques set to relieve the state-explosion problem in concurrent program verification. Their use often reduces significantly the memory needed for verifying local and termination properties of concurrent programs and, moreover, for verifying that concurrent programs satisfy their linear-time temporal logic specifications (i.e. for LTL model-checking). One particular such method is implemented in the verification system SPIN, which is considered to be one of the most efficient and most widely used LTL model-checkers. This paper builds on SPIN's partial-order reduction method to yield an approach that enables further space reductions for verifying concurrent programs. © 1998 John Wiley & Sons, Ltd.

In LOTOS, a system is specified as a behaviour expression describing the externally observable behaviour of the system in terms of possible sequences of interactions between the system and its environment. The desired control flow and data flow that must be established by a possible implementation of the system are specified in the behaviour expression as implicit enumerations of allowed sequences of interaction identifiers and relationships among interaction parameters, respectively. A model exposing the desired flow of data within the allowed control flow expressed in a system specification in LOTOS is presented. Based on the explicit information provided by the model, data flow anomaly detection and data flow oriented test selection are facilitated. A comprehensive example, i.e. an alternating bit protocol specification, is used to illustrate both these validation activities. An error in this specification is revealed by the analysis of a data flow anomaly detected within the specification. A set of test paths is derived from the specification by the application of an existing data flow oriented test selection criterion, called all-uses criterion.

A general model for constructing minimal length checking sequences employing a distinguishing sequence is proposed. The model is based on characteristics of checking sequences and a set of state recognition sequences. Some existing methods are shown to be special cases of the proposed model and are proven to construct checking sequences. The minimality of the resulting checking sequences is discussed and a heuristic algorithm for the construction of minimal length checking sequences is given.

We generalize the technique of fair reachability analysis to multi-cyclic protocols modeled as networks of communicating finite state machines, where a number of cyclic protocols are interconnected in such a way that any two component cyclic protocols share at most one process and each channel in the protocol belongs to exactly one component cyclic protocol. By composing the fair reachability relations of the component cyclic protocols, we prove that the set of fair reachable states of a multi-cyclic protocol is exactly the set of reachable states that are of equal channel length with respect to each of its component cyclic protocols. As a result, each deadlock state is fair reachable, and deadlock detection is decidable for the class of multi-cyclic protocols whose fair reachable state spaces are finite. Under the assumption that the underlying communication topology of a protocol is strongly connected, we show that fair reachability analysis is inherently infeasible for logical correctness validation beyond multi-cyclic protocols.

No abstract available.

Abstract The optimality of the length of a test sequence for a given finite‐state machine can be determined only with respect to the class of test sequences that employ the same number and type of state identification/verification (SIV) sequences and satisfy the same requirements for the starting and terminating states. Given a certain number and type of SIV sequences, we identify three different types of optimality for test sequences: Type11 requires test sequences to begin and end at the initial state; Type1y requires only that test sequences begin at the initial state; and Typexy imposes no requirements whatsoever on the starting and terminating states. Based on these definitions, we investigate the case where Unique Input Output (UIO) sequences are given as SIV sequences and derive lower bounds for the length of test sequences of Type11, Type1y, and Typexy.

A test sequence generation method is proposed for testing the conformance of a protocol implementation to its specification in a remote testing system where both external synchronization and input/output operation costs are taken into consideration. The method consists of a set of transformation rules that constructs a duplexU digraph from a given finite state machine (FSM) representation of a protocol specification; and an algorithm that finds a rural postman tour in the duplexU digraph to generate a synchronizable test sequence utilizing multiple UIO sequences. If the protocol satisfies a specific property, namely, the transitions to be tested and the UIO sequences to be employed form a weakly-connected subgraph of the duplexU digraph, the proposed algorithm yields a minimum-cost test sequence. X.25 DTE and ISO Class 0 transport protocols are shown to possess this property. Otherwise, the algorithm yields a test sequence whose cost is within a bound from the cost of the minimum-cost test sequence. The bound for the test sequence generated from the Q.931 network-side protocol is shown to be the cost sum of an input/output operation pair and an external synchronization operation.>

The authors present an efficient method for extracting a behavior description of a process (communicating finite state machine), as constrained by a given protocol. In the case where the constrained behavior corresponds to the unconstrained behavior depicted by the process specification, the process is said to be effective. The authors call the derived behavior description a process event graph (PEG). By comparing the PEG with the process specification, they determine whether a process in a protocol is effective. Two extensions to the basic algorithm are given, one to introduce parallelism to reachability analysis and one to detect traces that lead to process blockage. The authors focus initially on the two-process case, and then consider implications of more general protocols.>

A test sequence generation method is proposed for testing the conformance of a protocol implementation to its specification in a remote testing system, taking both external synchronization and input/output operation costs into consideration. The method consists of a set of transformation rules that constructs a duplexU digraph from a given finite state machine (FSM) representation of a protocol specification and a heuristic algorithm that finds a rural postman tour in the duplexU digraph to generate a synchronizable test sequence utilizing multiple UIO sequences. If the protocol satisfies a specific property, the heuristic algorithm yields a minimum-cost test sequence. The X.25 DTE and ISO Class 0 Transport protocols are proved to possess this specific property. otherwise, the heuristic algorithm yields a test sequence whose cost is within a bound from the cost of the minimum-cost test sequence. The bound for the test sequence generated from the Q.931 Network-side protocol is shown to be the cost sum of an input/output operation and an external synchronization operation.>

The optimization of the length of test sequences for finite state machine based protocol conformance testing is studied. The study focuses on test generation methods, called D-methods, that utilize distinguishing sequences in the construction of test segments. The extent of the optimization of the length of a test sequence is investigated with respect to two cases. The first case establishes the lower bound for the length of test sequences generated by any D-method that overlaps test segments. The second case establishes the lower bound for the length of test sequences generated by any D-method that does not overlap test segments. It is observed that the reduction in the length of test sequences due to overlapping is significant. An efficient algorithm for the generation of test sequences is proposed. This algorithm utilizes a distinguishing sequence and overlaps test segments. Sufficiency conditions are given both for finding a minimum- length test sequence in polynomial time and for constructing the optimal length test sequences by this algorithm.>

A method for automated selection of test sequences from a protocol specification given in Estelle for the purpose of testing both control and data flow aspects of a protocol implementation is discussed. First, a flowgraph modeling the flow of both control and data expressed in the given specification is constructed. In the flowgraph, definitions and uses of each context variable, as well as each input and output interaction parameter employed in the specification, are identified. Based on this information, associations between each output and those inputs that influence the output are established. Test sequences are selected to cover each such association at least once. The resulting test sequences are shown to provide the capability of checking whether a protocol implementation under test establishes the desired flow of both control and data expressed in the protocol specification. The proposed method is illustrated by using the class 0 transport protocol as an example.>

The authors investigate whether maximal overlapping of protocol test subsequences can be achieved in polynomial time. They review the concepts related to FSM (finite state machine)-based test sequence generation and then define the optimal test sequence generation (OTSG) problem. It is proved that the OTSG problem is NP-complete. Therefore an efficient solution to the problem should not be expected in the general case.>

This paper describes an optimization method for reducing the length of protocol conformance test sequences by overlapping test subsequences obtained using UIO sequences. It is shown that test sequences generated by this method are substantially shorter than those generated by other methods employing UIO sequences.

Usefulness of a formalization of the specification of ISDN LAPD is demonstrated for designing and developing a comprehensive set of conformance tests. Since many protocol standards are specified in a natural language (i.e., English), a method for formalizing protocol specifications with a view to a number of validation activities, including conformance testing, is also presented. In particular, it is shown how to utilize the state-transition-oriented approach to automatically generate a major component of standard conformance test suites. The use of formalized specifications is also illustrated for verifying the specification by selective executions, and for validating conformance test cases against the specification.>