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.

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.