Search

Finite State Machines (FSMs) are widely used for analysis and synthesis of hardware designs. In particular FSM can be used to specify and optimize sequential circuits. The number of gates of a circuit influences different aspects of the circuit (operation speed, latency, energy consumption, size, etc.), therefore the circuit’s gates number minimization is an actual problem. In this paper we suggest an approach of sequential circuit optimization by selecting an initial state of a specification FSM which allows to get a circuit with a defined optimization requirement. We experimented in order to estimate the benefit of our optimization approach and the length of rebuild/modified test suites.

In this paper, we consider checking the robustness of web services using the model of finite state automata and analyzing the solvability of an automaton equation over the concatenation operator. The paper contains the procedure for constructing the largest solution for a solvable automata equation, since a solution to the equation describes a malicious input. Experimental results have shown that this approach can be effective when checking the robustness of web services.

Timed automata and timed finite state machins (TFSMs) have been proposed to represent more accurately the behaviour of systems in continuous time. Recently, we introduced a model of TFSMs that extends the expressive power of FSMs by introducing a single clock, timed guards which restrict when the input/output transitions may happen, and timeouts on the transitions. We derived an abstraction procedure to convert a TFSM into an equivalent untimed FSM. Here, we extend the model with output timeouts and derive a minimal form for deterministic TFSMs that reduces the number of states, the number of transitions and the timeout values at each state.

In this paper, tools that automate tests conversion are presented. Tests for Java implementations are derived based on formal models. To apply these tests to Java implementations tests should be converted into an appropriate form for the Java programs. In this paper, JUnit is used. The experiments confirm the feasibility of developed tools.

The paper considers the problem of deriving a cascade parallel composition of timed finite state machines (TFSMs). It can be reduced to a step-by-step derivation of a binary parallel composition. It is known that if each component of the binary parallel composition is a TFSM with constant output delays, then the composition can result in a TFSM with an infinite set of output delays given by a finite set of linear functions. Therefore, the problem of deriving a cascade composition of TFSMs with constant output delays is reduced to deriving a series of binary parallel compositions of TFSMs with output delays given either as constants or as a set of linear functions. In this paper, we refine the definition of the TFSM with particular attention to the description of the output delay. BALM-II is used as an instrument for deriving the composition. Therefore, we consider the transition from a TFSM with output delays given as a set of linear functions to the corresponding automaton. We propose a new procedure for deriving an automaton. Unlike the known procedure, it does not require subsequent determinization of the derived automaton. In addition, we provide a step-by-step description of how to derive the composition of the corresponding automata using BALM-II, discuss the procedure of reverse transformation from the automaton of the composition to the TFSM, and note some aspects associated with the composition of TFSMs with output delays as a set of linear functions. An example that illustrates the derivation of the cascade parallel composition of TFSMs is given.

In this paper, we address the problem of deriving test suites for checking components of interacting finite state machines with timed guards (TFSMs). Given a component TFSM, a corresponding test is derived for the composition of TFSMs under the assumption that all other components are fault-free.

In this paper we consider two properties of timed automata, which help to reduce their complexity. We understand complexity as the number of time variables associated with a given timed automaton. The first property concerns redundant time variables and the second — timed automata composition.

In this paper we address the problem of deriving test suites for a system of interacting Finite State Machines (FSMs) with timed guards. We first show that unlike the general composition of timed automata, the composition of timed FSMs can be derived without uniting time variables of components and still can be described by an FSM that has a single time variable. We then discuss how tests with the guaranteed fault coverage can be derived for such composition. A simple composition example illustrates an idea behind the approach.

This paper is devoted to the generation of distinguishing experiments with completely specified timed finite state machines. It is shown, in particular, that two completely specified nondeterministic finite state machines can be distinguished by a multiple preset experiment if and only if these finite state machines are not equivalent. Two finite state machines can be distinguished by a simple adaptive experiment if and only if they are r-distinguishable, i.e., have no common completely specified reduction. The corresponding adaptive experiment is described by a special timed finite state machine. The procedure for constructing such an r-distinguishing timed finite state machine is proposed.

In this paper we describe software tool «FSMTest-1.0» that was developed by group of authors from the department of Computer science of Tomsk State University. The tool contains implementations of well-known and original test suites generation methods for different models with finite numbers of transitions. The main contribution of our tool is that it derives test suites with the guaranteed fault coverage.

This paper is devoted to the problem of an observable form for a given Timed Finite State Machine. This problem, together with the problem of the number of states in the observable form, has theoretical value, since it shows the way to build an observable form, and answers the question, does an observable form exist for any TFSM. Also it has a practical use in testing, since Finite State Machine methods of test generation rely on the fact that specification of a system is an observable FSM and those methods are intended to be applied for TFSMs.

Conformance testing with the guaranteed fault coverage is based on distinguishing faulty system implementations from the corresponding system specification. We consider timed systems modeled by timed possibly non-deterministic finite state machines (TFSMs) and propose algorithms for distinguishing two TFSMs. In particular, we present a preset algorithm for separating two separable TFSMs and an adaptive algorithm for r -distinguishing two possibly non-separable TFSMs. The proposed techniques extend existing methods for untimed non-deterministic FSMs by dealing with the fact that unlike untimed FSMs in general, a TFSM has an infinite number of timed inputs. Correspondingly we state that the upper bounds on the length of distinguishing sequences are the same as for untimed FSMs.

In this paper, we describe a software tool for optimizing the path length from primary inputs to primary outputs as well as the number of gates in digital circuits. A frame for optimization is extracted from a digital circuit the extracted frame is divided into two parts and the maximum flexibility for each part is determined by the largest solution to an appropriate FSM equation. We check whether one or some output functions of each part can be replaced by a simple function of two primary input variables that can be implemented as a single gate, while preserving the behavior of the overall fragment. A developed software package can deal with digital circuits which have around 500 gates, and 40 primary inputs and outputs. Experiments were performed for a pack of benchmarks that were first resynthesised by ABC tool [1]. Our results show that the developed package can improve around 15% of benchmarks.

The paper addresses the problem of the relationship between tests with the guaranteed fault coverage which are derived from two models of finite transition systems: LTS with inputs and outputs and input/output FSM. On one hand, there are well developed methods for deriving such finite tests against FSM while the model of input/output LTSs lacks such methods. On the other hand, almost all FSM-based methods return preset test suites and there are no good FSM-based methods for deriving adaptive tests. For deriving adaptive tests, it is worth to use LTS model where all the methods return adaptive test suites. We propose the transformation between two models and show how a complete test suite with respect to one model can be transformed into a complete test suite with respect to another model.