The paper addresses the problems of active learning and conformance testing of systems modeled by nondeterministic Mealy machines (NFSM). It presents a unified SAT-based approach originally proposed by the authors for deterministic FSMs and now generalized to partial nondeterministic machines and checking experiments. Learning a nondeterministic black box, the approach neither needs a Teacher nor uses it a conformance tester to approximate equivalence queries. The idea behind this approach is to infer from a current set of traces not one, but two inequivalent conjectures, use an input sequence distinguishing them in an output query, and update the current trace set with an observed trace to obtain a new pair of distinguishable conjectures, if possible. The classical active learning problem is further generalized by adding a nondeterministic specification FSM, which defines the solution space. The setup unifies the learning and adaptive testing problems and makes them equisolvable with the proposed approach.

No abstract available.

Automotive software has been growing in size, criticality and complexity with each new generation of vehicles. Testing at the model and code level is an important step in validating the software against various types of defects that may be introduced in the development process. Model based testing (MBT) methodology, paves a road towards automation of testing activities. Test generation is a computationally complex task, which requires efficient constraint solving techniques and some guidance from the test engineer when this task cannot be solved by a tool. At the same time, automatic tools can hardly substitute domain testing experts which can develop more effective tests or at least test fragments than any tool. This is why we believe that future test generation tools should support "tester-in-the-loop" MBT approaches. In this paper, we provide a brief report on our results in this direction.

There exists a significant body of work devoted to so-called complete tests which guarantee the detection of all the faults in a given fault domain. Several methods for generating complete tests for finite state machines (FSMs) which are based on a distinguishing sequence (DS) have been proposed. These methods even if extended to use adaptive DSs apply only to deterministic FSMs and the question arises whether they can be extended to non-deterministic FSMs to test for trace inclusion. In this paper, we generalize the notion of DS to a so-called total state separator, which is an adaptive experiment distinguishing states in any FSM that is trace included into the specification FSM. We then propose a method to test non-deterministic FSMs for trace inclusion. State separator is a key means of the proposed method, which has two phases: in the first phase, a preset test is constructed, which should be repeatedly applied to a non-deterministic implementation, thus requiring its resetting; in the second phase, the implementation is tested online and no reset is required. To the best of our knowledge, this is the first method which tests non-deterministic FSMs for the trace inclusion conformance relation, while avoiding resetting implementations to re-execute tests for transition verification.

An important step in the design of a complex system is its decomposition into a number of interacting components, of which some are given (known) and some need to be synthesized (unknown). Then a basic task in the design flow is to synthesize an unknown component that when combined with the known part of the system (the context) satisfies a given specification. This problem arises in several applications ranging from sequential synthesis to the design of discrete controllers. There are different formulations of the problem, depending on the formal models to specify the system and its components, the composition operators, and the conformance relations of the composed system versus the specification. Various behavioral models have been studied in the literature, e.g., finite state machines and automata, omega-automata, process algebras; various forms of synchronous and asynchronous (interleaving/parallel) composition have been considered; the conformance relations include language containment and equality, and notions of simulation. In this paper we give an overview of the problem (a.k.a., the unkown component problem, or submodule construction, etc.), and we focus on its reduction to solving equations over languages, as a key technology for supporting synthesis of compositional systems. We survey the state-of-art and highlight open problems requiring further investigation.

A checking sequence is a single input sequence which is able to reveal all the faults in a given fault domain. There are many methods for generating checking sequences for deterministic finite state machines (FSM), however, we are not aware of any generalization to no deterministic machines. No deterministic specifications are needed for software testing, as they describe the behavior of a wider class of reactive systems than deterministic FSMs when depending on the environment conditions, a no deterministic system is allowed to take different runs under the same input sequence. In this paper, we propose a method for constructing checking sequences when both the specification and implementations under test are modeled by no deterministic FSMs.

SUMMARY A long‐standing problem when testing from a deterministic finite state machine is to guarantee full fault coverage even if the faults introduce extra states in the implementations. It is well known that such tests should include the sequences in a traversal set which contains all input sequences of length defined by the number of extra states. This paper suggests the SPY method, which helps reduce the length of tests by distributing sequences of the traversal set and reducing test branching. It is also demonstrated that an additional assumption about the implementation under test relaxes the requirement of the complete traversal set. The results of the experimental comparison of the proposed method with an existing method indicate that the resulting reduction can reach 40%. Experimental results suggest that the additional assumption about the implementation can help in further reducing the test suite length. Copyright © 2011 John Wiley & Sons, Ltd.

In this paper, we consider a classical problem of complete test generation for deterministic finite-state machines (FSMs) in a more general setting. The first generalization is that the number of states in implementation FSMs can even be smaller than that of the specification FSM. Previous work deals only with the case when the implementation FSMs are allowed to have the same number of states as the specification FSM. This generalization provides more options to the test designer: when traditional methods trigger a test explosion for large specification machines, tests with a lower, but yet guaranteed, fault coverage can still be generated. The second generalization is that tests can be generated starting with a user-defined test suite, by incrementally extending it until the desired fault coverage is achieved. Solving the generalized test derivation problem, we formulate sufficient conditions for test suite completeness weaker than the existing ones and use them to elaborate an algorithm that can be used both for extending user-defined test suites to achieve the desired fault coverage and for test generation. We present the experimental results that indicate that the proposed algorithm allows obtaining a trade-off between the length and fault coverage of test suites.

In testing from a Finite State Machine (FSM), the generation of test suites which guarantee full fault detection, known as complete test suites, has been a long-standing research topic. In this paper, we present conditions that are sufficient for a test suite to be complete. We demonstrate that the existing conditions are special cases of the proposed ones. An algorithm that checks whether a given test suite is complete is given. The experimental results show that the algorithm can be used for relatively large FSMs and test suites.

We present an approach to the inference of automata models of Web-based business applications using only execution traces recording the externally observable behavior of such applications. The proposed approach yields behavioral models representing both the control flow of an application and the data variations corresponding to different types of users. We also describe how the obtained models allow the use of verification techniques like model checking in the validation phase using a case study featuring a travel reservation agency.

Test case prioritisation aims at finding an ordering which enhances a certain property of an ordered test suite. Traditional techniques rely on the availability of code or a specification of the program under test. In this paper, we propose to use string distances on the text of test cases for their comparison and elaborate a prioritisation algorithm. Such a prioritisation does not require code and can be useful for initial testing and in cases when code is difficult to instrument. We also briefly report on preliminary results of an experiment where the proposed prioritisation technique was compared with random permutations and four classical string distance metrics were evaluated.

Abstract This paper introduces a method to cover transitions of a concurrent system under test through a context consisting of infinite‐capacity queues. Concurrent systems have many important applications, but they are very difficult and expensive to test. One of the difficulties in testing concurrent systems is caused by the fact that queues in the test context can distort the behaviour of a concurrent system under test and can cause state explosion in test derivation. The proposed method derives transition covering tests directly from the specification of a concurrent system, not its composition with queues. As transition coverage is an important industrial metric of test quality, the results of the paper have practical applications. A case study is presented to illustrate one of the applications. Copyright © 2008 John Wiley & Sons, Ltd.

Quality assurance of Web applications is usually an informal process. Meanwhile, formal methods have been proven to be reliable means for the specification, verification, and testing of systems. However, the use of these methods requires learning their mathematical foundations, including temporal logics. Specifying properties using temporal logic is often complicated even to experts, while it is a daunting and error prone task for non-expert users. To assist web developers and testers in formally specifying web related properties, we elaborate a library of web specification patterns. The current version of the library of 119 functional and non-functional patterns is a result of scrutinizing various resources in the field of quality assurance of Web Applications, which characterize successful web application using a set of standardized attributes.

Abstract A formal framework for the analysis of execution traces collected from distributed systems at run-time is presented. We introduce the notions of event and message traces to capture the consistency of causal dependencies between the elements of a trace. We formulate an approach to property testing where a partially ordered execution trace is modeled by a collection of communicating automata. We prove that the model exactly characterizes the causality relation between the events/messages in the observed trace and discuss the implementation of this approach in SDL, where ObjectGEODE is used to verify properties using model-checking techniques. Finally, we illustrate the approach with industrial case studies.

By testing a concurrent system through queues, we seek a conclusive answer to whether a given transition of the specification of the system is executed. We define transition coverage through queues and find testing strategies to cover the transition in question with and without fairness, respectively.

We consider a formal framework for property verification of web applications using Spin model checker. Some of the web related properties concern all states of the model, while others - only a proper subset of them. To be able to discriminate states of interest in the state space, we solve the problem of property specification in LTL over a subset of states of a system under test while ignoring the valuation of the properties in the rest of them. We introduce specialized operators that facilitate specifying properties over propositional scopes, where each scope constitutes a subset of states that satisfy a propositional logic formula. Using the proposed operators, the user can specify web properties more concisely and intuitively. We illustrate the proposed solution in specifying properties of web applications and discuss other potential applications.

This paper addresses the problem of test generation from partially specified deterministic finite state machines (FSMs) that may have indistinguishable states and, thus, are not necessarily reduced (minimized). The known methods for checking experiments that are based on state identification are not applicable to unreduced machines. We propose the so-called state-counting approach that is directly applicable to unreduced FSMs. The approach generalizes the idea of state identification in test generation methods for deterministic machines.

We investigate the problem of configuration verification for the extended FSM (EFSM) model. This is an extension of the FSM state identification problem. Specifically, given a configuration ("state vector") and an arbitrary set of configurations, determine an input sequence such that the EFSM in the given configuration produces an output sequence different from that of the configurations in the given set or at least in a maximal proper subset. Such a sequence can be used in a test case to confirm the destination configuration of a particular EFSM transition. We demonstrate that this problem could be reduced to the EFSM traversal problem, so that the existing methods and tools developed in the context of model checking become applicable. We introduce notions of EFSM projections and products and, based on these notions, we develop a theoretical framework for determining configuration-confirming sequences. The proposed approach is illustrated on a realistic example.

The problem of designing a component that, combined with a known part of a system, conforms to a given overall specification arises in several applications ranging from logic synthesis to the design of discrete controllers. We cast the problem as solving abstract equations over languages. Language equations can be defined with respect to several language composition operators such as synchronous composition, /spl middot/, and parallel composition, /spl square/; conformity can be checked by language containment. In this paper, we address parallel language equations. Parallel composition arises in the context of modeling delay-insensitive processes and their environments. The parallel composition operator models an exchange protocol by which an input is followed by an output after a finite exchange of internal signals. It abstracts a system with two components with a single message in transit, such that at each instance either the components exchange messages or one of them communicates with its environment, which submits the next external input to the system only after the system has produced an external output in response to the previous input. We study the most general solutions of the language equation A/spl square/X/spl sube/C, and define the language operators needed to express them. Then we specialize such equations to languages associated with important classes of automata used for modeling systems, e.g., regular languages and FSM languages. In particular, for A/spl square/X/spl sube/C, we give algorithms for computing: the largest FSM language solution, the largest complete solution, and the largest solution whose composition with A yields a complete FSM language. We solve also FSM equations under bounded parallel composition. In this paper, we give concrete algorithms for computing such solutions, and state and prove their correctness.

A previous ACM TOSEM article of Ph. Bernhard (“A Reduced Test Suite of Protocol Conformance Testing,” ACM Transactions on Software Engineering and Methodology, Vol. 3, No. 3, July 1994, pages 201-220) describes three new versions of the so-called W-method for solving the protocol-testing problem, i.e., solving the Mealy machine equivalence problem. The author claims that these versions all have the same fault detection capability as the original W-method. In this correspondence we prove that the results of that article are incorrect.

It is shown in this paper that the problem of deciding if a test suite generated from a finite state machine provides complete fault coverage can be converted into the problem of minimizing the test tree representing the test suite. A fault coverage analysis procedure, capable of deciding if a given test suite provides complete fault coverage in respect to a given FSM specification, is then developed. The core of this procedure is a state minimization procedure developed specifically for the class of FSMs whose graphic representations are trees. The fault coverage analysis procedure can cope with partially specified FSM specifications which need not be reduced and faults that increase the number of states up to a chosen upper bound. Two necessary and one sufficient conditions, which in some cases may simplify the fault coverage analysis, are also presented.>

Communication protocols are the rules that govern the communication between the different components within a distributed computer system. Since protocols are implemented in software and/or hardware, the question arises whether the existing hardware and software testing methods would be adequate for the testing of communication protocols. The purpose of this paper is to explain in which way the problem of testing protocol implementations is different from the usual problem of software testing. We review the major results in the area of protocol testing and discuss in which way these methods may also be relevant in the more general context of software testing.

Presents a method of generating test sequences for concurrent programs and communication protocols that are modeled as communicating nondeterministic finite-state machines (CNFSMs). A conformance relation, called trace-equivalence, is defined within this model, serving as a guide to test generation. A test generation method for a single nondeterministic finite-state machine (NFSM) is developed, which is an improved and generalized version of the Wp-method that generates test sequences only for deterministic finite-state machines. It is applicable to both nondeterministic and deterministic finite-state machines. When applied to deterministic finite-state machines, it yields usually smaller test suites with full fault coverage than the existing methods that also provide full fault coverage, provided that the number of states in implementation NFSMs are bounded by a known integer. For a system of CNFSMs, the test sequences are generated in the following manner: a system of CNFSMs is first reduced into a single NFSM by reachability analysis; then the test sequences are generated from the resulting NFSM using the generalized Wp-method.>