International audience

International audience

International audience

Abstract State identification is the well-known problem in the automata theory that is aimed to determining the current or initial state of a system under test and this fact is widely used in the model-based testing of software and hardware systems. When modern systems are modeled, it is necessary to take into account the timed aspects and for this reason classical Finite State Machines (FSM) are extended by clock variables. In this work, we study the homing problem for FSMs with timeouts (TFSM). For this purpose, we introduce the notion of a timed homing sequence (HS) that is different from that for classical FSMs and propose a method for checking the existence and deriving a timed HS if it exists. A proposed method is based on the FSM abstraction of a TFSM, i.e. on a classical FSM that partially describes the behavior of a corresponding TFSM and inherits many of its properties. Since timeouts allow the system to move from state to state without input impact, we define a timed HS as a sequence that sets a TFSM to a stable state where the system can stay infinitely long waiting for an input.

Homing sequence derivation for nondeterministic finite state machines (NFSMs) has important applications in software/hardware system testing and verification. Unlike prior methods based on explicit tree-based search, in this article we formulate the derivation of a preset/adaptive homing sequence in terms of quantified Boolean formula (QBF) solving. This formulation exploits compact circuit representation of NFSMs and QBF encoding of the existence condition of homing sequence for effective computation. The implicit circuit representation effectively avoids explicit state enumeration, and can be more scalable. Different encoding schemes and QBF solvers are evaluated for their suitability for the homing sequence derivation. Experiments on various computation methods and benchmarks show the generality and feasibility of a proposed approach.

Software Defined Networking (SDN) is a novel network management technology, which currently attracts a lot of attention due to the provided capabilities. Recently, different works have been devoted to testing / verifying the (correct) configurations of SDN data planes. In general, SDN forwarding devices (e.g., switches) route (steer) traffic according to the configured flow rules; the latter identifies the set of virtual paths implemented in the data plane. In this paper, we propose a novel preventive approach for verifying that no misconfigurations (e.g., infinite loops), can occur given the requested set of paths. We discuss why such verification is essential, namely, how, when synthesizing a set of data paths, other not requested and undesired data paths (including loops) may be unintentionally configured. Furthermore, we show that for some cases the requested set of paths cannot be implemented without adding such undesired behavior, i.e., only a superset of the requested set can be implemented. Correspondingly, we present a verification technique for detecting such issues of potential misconfigurations and estimate the complexity of the proposed method; its polynomial complexity highlights the applicability of the obtained results. Finally, we propose a technique for debugging and repairing a set of paths in such a way that the corrected set does not induce undesired paths into the data plane, if the latter is possible.

Abstract There has been a growing interest in defining models of automata enriched with time, such as finite automata extended with clocks (timed automata). In this paper, we study deterministic timed finite state machines (TFSMs), i.e., finite state machines with a single clock, timed guards and timeouts which transduce timed input words into timed output words. We solve the problem of equivalence checking by defining a bisimulation from timed FSMs to untimed ones and vice versa. Moreover, we apply these bisimulation relations to build the intersection of two timed finite state machines by untiming them, intersecting them and transforming back to the timed intersection. It is known that many problems like inclusion and equivalence checking are undecidable for timed automata. Our results show that TFSMs correspond to a decidable subclass of timed automata that admits a restricted form of $$\varepsilon $$ ε -transitions (i.e., timeouts) where most of the relevant problems like equivalence and intersection are decidable.

An incremental approach is proposed for deriving an adaptive Distinguishing Test Case (DTC) for a subset of states of an observable non-deterministic Finite-State Machine (FSM). The approach considers the states of the subset incrementally while checking the existence of a DTC. Experiments were conducted to assess and compare various versions of the incremental approach with respect to a non-incremental counterpart. In addition, two implementations of an efficient heuristic approach for the considered problem are proposed. The implementations are based on a special traversal of a successor tree up to certain height using some established construction rules. Experiments were conducted to assess the execution time and quality of obtained solutions for large FSMs. Moreover, we determine how often a DTC exists while varying the number of states, outputs and non-determinism of a given FSM. A complete summary of the obtained results is included.

International audience

International audience

Abstract A top-down approach is presented for checking the existence and derivation of an adaptive distinguishing test case (called also an adaptive distinguishing sequence) for a nondeterministic finite state machine (NDFSM). When such a test case exists, the method returns a canonical test case that includes all other distinguishing tests of the given complete observable NDFSM. In the second part of the paper, a constructive approach is provided for deriving a class of complete observable NDFSMs with n states, n > 2, and 2 n − n − 1 inputs such that a shortest adaptive distinguishing test case for each NDFSM in the intended class has the length (height) 2 n − n − 1. In other words, we prove the reachability of the exponential upper bound on the length of a shortest adaptive distinguishing sequence for complete observable NDFSMs while for deterministic machines the upper bound is polynomial with respect to the number of states. For constructing the intended class of NDFSMs for a given n , we propose a special linear order over all the non-empty subsets without singletons of an n -element set. The obtained tight exponential upper bound initiates further research on identifying certain NDFSM classes where this upper bound is not reachable.

International audience

International audience

International audience

This paper is devoted to study the use of 'gedanken' experiments with Finite State Machines (FSMs) for protocol passive testing optimization. We discuss how the knowledge obtained from the state identification of an implementation under test (IUT) can be utilized for effective IUT monitoring. Differently from active testing techniques, such identification is performed by only observing the IUT behavior. If the state identification is possible (at least partially), then this fact allows to reduce the number of properties (test purposes) to be checked at certain execution point(s). Correspondingly, this allows to simplify and/or accelerate, i.e. improve the monitoring process by verifying the system behavior only at critical states against the appropriate set of properties associated with a given state. The paper discusses which 'gedanken' experiments can be considered for this purpose and how they can be derived for various specifications of communication protocols. The results presented in the paper are followed by an illustrative protocol example that demonstrates the efficiency of the proposed approach.

We consider a composite system consisting of two communicating finite state machines, an embedded component and a context representing the remaining parts of the system. In this article, a method is proposed for translating a complete internal test suite defined over the unobservable alphabets of the embedded component into a complete external test suite defined over the observable external alphabets of the system, assuming that the context is fault-free. Propositions are established to verify the different steps of the proposed method and a detailed application example illustrating these steps is included.

In this paper, we present a framework for evaluating the QoE of a service that includes functional and non-functional service requirements. Non-functional requirements are classified into objective, subjective, and business parameters that affect Quality of Service (QoS), Quality of Experience (QoE), and Quality of Business (QoBiz), correspondingly. As those metrics have a strong dependency between each other, we discuss how the QoE of a web-based Over-The-Top service (OTT) can be evaluated taking into account subjective, objective and business parameters. The functional service behavior is described by an Extended Finite State Machine (EFSM) in which non-functional objective, subjective and business-related parameters are tracked using context variables and corresponding updating functions. These parameters are used to evaluate the QoE of the service. We show that the corresponding model allows to keep a track of a user-service interaction. Moreover, the model of the service integrates subjective, objective and business parameters, and thus, can be applied to the QoE evaluation of any OTT service.

The composition of two arbitrary component automata can have deadlock states. A method is proposed to minimally reduce a component automaton such that the resulting composition with the other automaton is deadlock-free. The method is applied to deriving compositionally deadlock-free solutions of automata equations over the synchronous composition.

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.

International audience

This paper presents a short survey on the quality evaluation of web services. The most popular metrics for estimating such quality and user perception of web services are Quality of Service (QoS) and Quality of Experience (QoE), which represent objective and subjective assessments correspondingly. For different types of web services, the values of QoS and QoE are measured in different ways. In this paper, we consider various definitions of QoS based on web service parameters and describe several methods for evaluating QoS and QoE. We start with experimental evaluation of QoS based on network traffic analysis and further turn to model based methods for QoS estimating. Existing relationships between different kinds of service quality evaluation are also discussed.

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.

Test derivation based on user defined faults deals with the generation of tests that check if some parts of a given specification are correctly implemented in a corresponding implementation. In this paper, we present a method for test derivation based on user defined faults for extended FSM (EFSM) specifications. Given an EFSM specification ES and a set of selected transitions of ES, the method returns a test suite that is complete with respect to output and transfer faults at the selected transitions, i.e., checks whether the selected transitions are correctly implemented in a corresponding EFSM implementation. Test derivation is based on a formally defined fault model (conformance relation and types of faults) and is guided by some conditions established for complete test derivation. To reduce test derivation efforts, we propose to use appropriate slices of the specification EFSM. The slices, on one hand, preserve the facilities of the original specification (before slicing) EFSM for traversing the selected transitions and for distinguishing their final states and on the other hand, these slices are much smaller than the given specification. Application examples and a simple case study are provided.

The paper addresses the problem of designing a component that combined with a known part of a system, called the context FSM, is a reduction of a given specification FSM. We study compositionally progressive solutions of synchronous FSM equations. Such solutions, when combined with the context, do not block any input that may occur in the specification, so they are of practical use. We show that if a synchronous FSM equation has a compositionally progressive solution, then the equation has the largest compositionally progressive solution. We provide an algorithm to compute the largest compositionally progressive solution that splits states of the largest solution and then removes those inducing a non-progressive composition.

Abstract Several authors have studied the relationships between non‐deterministic finite state machines (FSMs). These relationships can be used, for example, for deriving conformance tests from specifications represented by FSMs. In this paper, the separability relation between FSMs is studied. In particular, an algorithm is presented that derives a shortest separating sequence of two non‐deterministic FSMs. Given FSMs S with n states and T with m states, it is shown that the upper bound on the length of a shortest separating sequence is 2mn−1. Moreover, the upper bound is shown to be reachable. However, according to the conducted experiments, on average, the length of a shortest separating sequence of FSMs S and T states is less than mn and the existence of a separating sequence significantly depends on the number of non‐deterministic transitions in these FSMs. The proposed algorithm can also be used for deriving a separating sequence of two different states of a single FSM or for deriving a separating sequence of three or more FSMs. Copyright © 2007 John Wiley & Sons, Ltd.

A class of discrete event synthesis problems can be reduced to solving language equations, F /spl middot/ X /spl sube/ S, where F is the fixed component and S the specification. Sequential synthesis deals with FSMs when the automata for F and S are prefix closed. and are naturally represented by multi-level networks with latches. For this special case, we present an efficient computation, using partitioned representations, of the most general prefix-closed solution of the above class of language equations. The transition and the output relations of the FSMs for F and S in their partitioned form are represented by the sets of output and next state functions of the corresponding networks. Experimentally, we show that using partitioned representations is much faster than using monolithic representations, as well as applicable to larger problem instances.

The development of test cases is an important issue for testing software, communication protocols and other reactive systems. A number of methods are known for the development of a test suite based on a formal specification given in the form of a finite state machine. Well-known methods are called the W, Wp, UIO, UIOv, DS, H and HIS test derivation methods. These methods have been extensively used by research community in the last years; however no proper comparison has been made between them. In this paper, we experiment with these methods to assess their complexity, applicability, completeness, fault detection capability, length and derivation time of their test suites. The experiments are conducted on randomly generated specifications and on a realistic protocol called the simple connection protocol.

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.

The development of appropriate test cases is an important issue for conformance testing of protocol implementations and other reactive software systems. A number of methods are known for the development of a test suite based on a specification given in the form of a finite state machine. In practice, the system requirements evolve throughout the lifetime of the system and the specifications are modified incrementally. We adapt four well-known test derivation methods, namely, the HIS, W, Wp, and UIOv methods, for generating tests that would test only the modified parts of an evolving specification. Some application examples and experimental results are provided. These results show significant gains when using incremental testing in comparison with complete testing, especially when the modified part represents less than 20 percent of the whole specification.

The paper is devoted to the problem of reducing component machines of the synchronous FSM composition. The problem is considered as the problem of FSM equation solving. The complexity of an FSM equation significantly depends on the level of our optimization. We show that sometimes it is more effective to solve not a single equation but a system of equations.

Abstract Testing a component embedded into a complex system, in which all other components are assumed fault‐free, is known as embedded testing. This paper proposes a method for minimizing a test suite to perform embedded testing. The minimized test suite maintains the fault coverage of the original test suite with respect to faults within the embedded component. The minimization uses the fact that the system is composed of a fault‐free context and a component under test, specified as communicating, possibly non‐deterministic finite state machines (FSMs). The method is illustrated using an example of telephone services on an intelligent network architecture. Other applications of the proposed approach for testing a system of communicating FSMs are also discussed. Copyright © 2003 John Wiley & Sons, Ltd.

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.