On the synthesis of adaptive tests for nondeterministic finite state machines

The paper suggests a method for synthesis of adaptive tests with guaranteed coverage for checking functioning of discrete systems whose behavior is described by nondeterministic finite state machines. In contrast to other known methods, we do not represent the complete test as a tree but list test cases one by one and check functioning of the finite state machine on each test case. The complete test detects all defective systems that are r-distinguishable from the reference system. Besides, the test detects other defective systems containing traces that are not present in the specification; but detection of all such systems that are r-compatible with the specification is not guaranteed.     

On deriving test suites for nondeterministic finite state machines with time-outs

In the paper, the non-separability relation for finite state machines with time-outs is studied. A specific feature of such machines is integer-valued delays, or time-outs, which determine how long the finite state machine will stay in one or another state if there are no input actions. If the time-out is over and no input symbol has been applied, then the TFSM state is changed according to the transition under time delay. In the paper, an algorithm for constructing a separating sequence for such finite state machines is presented. Here, the separating sequence is a timed input sequence for which sets of input sequences of the TFSM do not intersect; hence, it is sufficient to apply the separating sequence once in order to distinguish the TFSMs by their output reactions. This algorithm underlies the algorithm for construction of test suites with respect to non-separability relation in the case where the fault domain is specified by means of a mutation machine. Test suite derivation with respect to non-separability relation by way of ??TFSM to FSM?? transformation is discussed.     

On the complexity of existence of homing sequences for nondeterministic finite state machines

The paper discusses complexity of the problem of checking existence of a homing sequence for an observable complete finite state machines (FSMs). The minimum length of such a sequence for FSMs of certain class is known to be exponential in the number of the FSM states. It is shown that the problem of checking the existence of such a sequence belongs to class PSPACE.     

On state reduction of incompletely specified finite state machines

State reduction of incompletely specified finite state machines (ISFSMs) is an important task in optimization of sequential circuit design and known as an NP-complete problem. Removal of redundant states reduces the logic, because of this, chip area decreases. In addition, test generation is easier when the sequential circuit is irredundant. In this paper, we present a heuristic for state reduction of ISFSMs. The proposed heuristic is based on a branch-and-bound search technique and identification of sets of compatible states of a given ISFSM specification. We have obtained results as good as the best exact method in the literature but with significantly better run-times.     

On the structure of free finite state machines

The finite state machine U_{m, n}(M) freely generated by a set consisting of m states and n inputs subjects to the relations holding in the finite state machine M was considered by Birkhoff and Lipson in [1, 2]. In this paper, necessary and sufficient conditions for U_{m, n}(M) to consist of m disjoint copies of U_{1, n}(M) are established. The relationship between U_{1, n}(M) and the transition monoid of M, and a representation of U_{1, n}(M) as a transition monoid machine are described. The characterization of machines of type U_{1, n}(M) is in this way reduced to the characterization of finite monoids possessing a ‘universal presentation’. Some general results concerning finite semigroups and groups with a universal presentation, and precise characterizations of finite semilattices and Abelian groups admitting a universal presentation are described.     

Canonical finite state machines for distributed systems

There has been much interest in testing from finite state machines (FSMs) as a result of their suitability for modelling or specifying state-based systems. Where there are multiple ports/interfaces a multi-port FSM is used and in testing, a tester is placed at each port. If the testers cannot communicate with one another directly and there is no global clock then we are testing in the distributed test architecture. It is known that the use of the distributed test architecture can affect the power of testing and recent work has characterised this in terms of local s-equivalence: in the distributed test architecture we can distinguish two FSMs, such as an implementation and a specification, if and only if they are not locally s-equivalent. However, there may be many FSMs that are locally s-equivalent to a given FSM and the nature of these FSMs has not been explored. This paper examines the set of FSMs that are locally s-equivalent to a given FSM M. It shows that there is a unique smallest FSM χ_min(M) and a unique largest FSM χ_max(M) that are locally s-equivalent to M. Here smallest and largest refer to the set of traces defined by an FSM and thus to its semantics. We also show that for a given FSM M the set of FSMs that are locally s-equivalent to M defines a bounded lattice. Finally, we define an FSM that, amongst all FSMs locally s-equivalent to M, has fewest states. We thus give three alternative canonical FSMs that are locally s-equivalent to an FSM M: one that defines the smallest set of traces, one that defines the largest set of traces, and one with fewest states. All three provide valuable information and the first two can be produced in time that is polynomial in terms of the number of states of M. We prove that the problem of finding an s-equivalent FSM with fewest states is NP-hard in general but can be solved in polynomial time for the special case where there are two ports.     

Synthesis of finite state machines for improved state verification

Finite State Machines (FSMs) are used in diverse areas to model hardware and software systems. Verification of FSMs is essential to ensure reliability of systems. To verify that a machine is in an expected state in testing, Unique Input/Output (UIO) sequences are used. The aforementioned testing methodology requires that each state in the FSM has an UIO. However, it is possible for a given machine that few or even none of its states have an UIO sequence. This paper presents a guided heuristic algorithm for synthesizing FSMs such that each state has an UIO sequence. The states of an FSM with identical I/O labels on transitions are grouped in order to identify the states which do not possess UIO sequence. The transitions are then augmented by adding extra output terminals incrementally so that new UIO sequences are created for the states. A greedy approach is used to optimize the number of added outputs. Initially, the transitions which lead to state convergence (i.e., transitions with identical input/output labels taking a set of states to the same next state) and constrained self-loop (i.e., transitions taking a set of states either to itself or leads to state convergence) are identified since a state with only these transitions will never have a UIO sequence. Extra output terminals are added to the FSM which are used only while testing and the augmented output labels make sure that the states are neither convergent nor has constrained self-loop, thereby ensuring UIO sequence. The proposed algorithm, referred to as AUGP, was tested with a large number of FSMs including the Microelectronics Center of North Carolina (MCNC) FSM benchmarks. The augmented state transition table was used as input to a UIO computation algorithm (developed by the same authors [Ahmad I, et al. IEE Proc Comput Digital Tech 2004;151(2):131]) to check the performance of the augmentation algorithm and the tested FSMs were found to possess UIO sequence for all states.     

Active learning for extended finite state machines

We present a black-box active learning algorithm for inferring extended finite state machines (EFSM)s by dynamic black-box analysis. EFSMs can be used to model both data flow and control behavior of software and hardware components. Different dialects of EFSMs are widely used in tools for model-based software development, verification, and testing. Our algorithm infers a class of EFSMs called register automata. Register automata have a finite control structure, extended with variables (registers), assignments, and guards. Our algorithm is parameterized on a particular theory, i.e., a set of operations and tests on the data domain that can be used in guards.Key to our learning technique is a novel learning model based on so-called tree queries. The learning algorithm uses tree queries to infer symbolic data constraints on parameters, e.g., sequence numbers, time stamps, identifiers, or even simple arithmetic. We describe sufficient conditions for the properties that the symbolic constraints provided by a tree query in general must have to be usable in our learning model. We also show that, under these conditions, our framework induces a generalization of the classical Nerode equivalence and canonical automata construction to the symbolic setting. We have evaluated our algorithm in a black-box scenario, where tree queries are realized through (black-box) testing. Our case studies include connection establishment in TCP and a priority queue from the Java Class Library.     

On input-revolving deterministic and nondeterministic finite automata

We introduce and investigate input-revolving finite automata, which are (nondeterministic) finite state automata with the additional ability to shift the remaining part of the input. Three different modes of shifting are considered, namely revolving to the left, revolving to the right, and circular interchanging. We investigate the computational capacities of these three types of automata and their deterministic variants, comparing any of the six classes of automata with each other and with further classes of well-known automata. In particular, it is shown that nondeterminism is better than determinism, that is, for all three modes of shifting there is a language accepted by the nondeterministic model but not accepted by any deterministic automaton of the same type. Concerning the closure properties most of the deterministic language families studied are not closed under standard operations. For example, we show that the family of languages accepted by deterministic right-revolving finite automata is an anti-AFL which is not closed under reversal and intersection.     

Generating Conformance Tests for Nondeterministic Protocol Machines

We present a method of generating test cases from the software specifications which are modeled by nondeterministic finite state machines.It is applicable to both nondeterministic and deterministic finite state machines.When applied to deterministic machines,this method yields usually smaller test suites with full fault coverage than the existing methods that also assure full fault coverage.In particular,the proposed method can be used to test the control portion of software specified in the formal specification languages SDL or ESTELLE.     

Hierarchical finite state machines for autonomous mobile systems

This paper proposes a system architecture, related design approaches for autonomous mobile systems and guidelines for self-sufficient autonomy. Development of a tiered layout for a hybrid-state control in a series of stages as well as the integration of such a controller in the overall autonomy structure are proposed and demonstrated as part of multiple examples, including The Ohio State University participation in DARPA Urban Challenge 2007. The hierarchical layout and the iterative design methodology enable a certain level of design flexibility for the overall system and preparation for various contingencies, as illustrated on specific development cycles.     

扰动模糊有限转换状态机

引入了扰动模糊有限转换状态机和扰动模糊有限状态机的（强）同态的概念,研究了它们的相关性质。给出了[Σ]的元素构成所有长度有限的词集上的两种同余关系,讨论商结构问题,证明了相应的所有等价类构成具有单位元的有限半群,并且这两个有限半群是同态的。给出了[Q]上容许关系及强同态的核的概念,研究了它们的相关性质。     

Incremental testing of finite state machines

The automatic generation of test suites for systems modelled as finite state machines (FSMs) is an important problem that impacts several critical applications. Known methods that automatically generate tests for FSMs, specially the W‐method and some derivations, strongly assume that the number of system states is small. If the overall number of states in the FSM specification is relatively large, such methods become difficult to use. However, often in practice, a system is defined as a combination of several subsystems, with the latter already independently designed, developed and tested. In this paper, we define the concept of combined FSMs and introduce a new method to test modular compositions of FSMs. This method allows for a new incremental testing strategy that turns the testing of new systems into a much more scalable process. As an example, we present an infinite family of naturally occurring FSM models for which our method produces exponentially more compact test suites than the W‐method. Copyright © 2012 John Wiley & Sons, Ltd.     

Reversal-bounded nondeterministic multicounter machines and complementation

It is proved that the family of languages recognized by one-way real-time nondeterministic multicounter machines with constant number of counter reversals is not closed under complementation. This solves an open problem of Wagner and Wechsung (1986).     

Fragment shaders for agent animation using finite state machines

In a previous paper we generated animated agents and their behavior using a combination of XML and images. The behavior of agents was specified as a finite state machine (FSM) in XML. We used images to determine properties of the world that agents react to. While this approach is very flexible, it can be made much faster by using the power available in modern GPUs. In this paper we implement FSMs as fragment shaders using three kinds of images: world space images, agent space images and FSM table images. We show a simple example and compare performance of CPU and GPU implementations. Then we examine a more complex example involving more maps and two types of agents (predator–prey). Furthermore we explore how to render agents in 3D more efficiently by using a variation on pseudoinstancing.     

On conditions for defining a closed cover to verify progress forcommunicating finite state machines

The closed-cover technique for verifying progress for two communicating finite-state machines exchanging messages over two lossless, FIFO channels is considered. The authors point out that the definition of a closed cover in M.G. Gouda (ibid., vol.SE-10, no.6, p.846-55, Nov. 1984) may be too restrictive, while that in M.G. Gouda and C.K. Chang (ACM Trans. Prog. Lang., vol.8, no.1, p.154-82, Jan. 1986) is not correct. They then show how a condition of the closed-cover definition can be modified to relax restriction to various degrees. They also discuss the similarities and relationship between the structural partition technique and the closed-cover technique     

Structural transformations of probabilistic finite state machines

Probabilistic finite state machines have recently emerged as a viable tool for modelling and analysis of complex non-linear dynamical systems. This paper rigorously establishes such models as finite encodings of probability measure spaces defined over symbol strings. The well known Nerode equivalence relation is generalized in the probabilistic setting and pertinent results on existence and uniqueness of minimal representations of probabilistic finite state machines are presented. The binary operations of probabilistic synchronous composition and projective composition, which have applications in symbolic model-based supervisory control and in symbolic pattern recognition problems, are introduced. The results are elucidated with numerical examples and are validated on experimental data for statistical pattern classification in a laboratory environment.     

Formal testing from timed finite state machines

In this paper we present a formal methodology to test both the functional and temporal behaviors in systems where temporal aspects are critical. We extend the classical finite state machines model with features to represent timed systems. Our formalism allows three different ways to express the timing requirements of systems. Specifically, we consider that time requirements can be expressed either by means of fix time values, by using random variables, or by considering time intervals. Different implementation relations, depending on both the interpretation of time and on the non-determinism appearing in systems, are presented and related. We also study how test cases are defined and applied to implementations. Test derivation algorithms, producing sound and complete test suites, are also presented. That is, by deriving these test suites we relate the different notions of passing tests and the different implementation relations. In other words, for a given correctness criterion, a system represents an appropriate implementation of a given model if and only if the system successfully passes all the test belonging to the derived test suite.