Search

The paper is devoted to the problem of optimization of discrete multi-module systems. The proposed optimization is based on iterative component-wise optimization. This approach has established itself as a promising approach due to its good scalability. We consider a technique that is based on the use of the so-called “don’t care” input sequences of the component, i.e. sequences that cannot appear at the input of a component under optimization in the composition and for this purpose, windows with sequential networks are selected. Preliminary experimental results illustrate that a proposed approach for the component-wise iterative optimization is effective for FSM networks when components are optimized for the further FPGA implementation.

Part 5: Short Contributions; International audience; Deriving tests with guaranteed fault coverage by FSM-based test methods is rather complex for systems with a large number of states. At the same time, formal verification methods allow to effectively process large transition systems; in particular, SMT solvers are widely used to solve analysis problems for finite transition systems. In this paper, we describe the known necessary and sufficient conditions of completeness of test suites derived by FSM-based test methods via the first-order logic formulas and use an SMT solver in order to check them. In addition, we suggest a new sufficient condition for test suite completeness and check the corresponding first-order logic formula via the SMT solver. The results of computer experiments with randomly generated finite state machines confirm the correctness and efficiency of a proposed approach.

In this paper, we use a window approach when optimizing Finite State Machine (FSM) components of a multi module system. Given a window with a loop-free binary composition of complete deterministic FSMs, we construct a partial FSM for the tail component FSM such that any reduced form of this partial FSM can replace the tail component preserving the composition behaviour. There are a number of cases when using a partial network equivalent instead of the initial component FSM allows to simplify the corresponding logic circuit with respect to the number of gates and path length between primary inputs and outputs.

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.

In this paper, an approach to test synthesis based on a logic circuit model for microcontroller based physical systems is described. The formal model of the logic circuit is used to describe the behavior of discrete systems with a finite number of transitions. A model of a higher level of abstraction is a Finite State Machine (FSM) and its modifications, for example, a timed Finite State Machine (TFSM). These formal models are used to synthesize complete test suites for discrete systems with respect to a given fault model. A fault model based on three popular faults in logic circuits is often used to derive complete test suites for logic circuits. According to a previous experimental result, such complete test suites can detect a large number of output faults in the corresponding FSM. The advantage of the logic circuit model is scalability, which allows building tests with sufficiently high fault coverage, in the case when the FSM of the system under test has a large number of states and the test synthesis process becomes difficult. The paper describes the application of this approach to the microcontroller based system of a switching generator, whose behavior is described by a TFSM. The number of states of corresponding FSM abstraction increases significantly so an FSM based test derivation process becomes more complex.

Testing of digital circuits is very important, especially for guaranteeing the correct and reliable functioning of electronic devices. One of the possibilities for deriving high quality test suites is using test generation methods for a corresponding Finite State Machine simulating the circuit behavior. In this paper, we estimate the number of implementation states whenever a circuit mutant is introduced. Experimental evaluation is performed for three types of mutants, namely Single Stuck-At Fault Mutants, Single Bridge Fault Mutants, and Hardly Detectable Fault Mutants. Experiments with the ITC'99 benchmarks (second release) show that in most cases the injection of a fault does not increase the number of states. Moreover, whenever the number of states is increased, the increment is on average 20%. Given this increment, we perform the experiments to showcase that for testing circuits with guaranteed fault coverage with respect to the listed faults, one can apply the W-method with the upper bound m = 1.2n states, for n states in the specification (circuit) FSM.

Many devices of controlling parts of physical systems are implemented on the basis of microcontrollers. Such critical systems are needed to be tested thoroughly. This paper contains experimental results on testing controlling parts of laser based physical systems. We consider generators of synchronizing pulses for controlling important parts of the laser system. Test derivation is performed using the model of a timed transition system with finite number of states. We then generate a number of mutants for a microcontroller part and the performed experiments clearly show that timed Finite State Machine based test suites have a good quality as they allow to detect most frequently occurring faults in considered systems.

Testing digital circuits is crucial for guaranteeing the correct and reliable functioning of electronic devices. Deriving high quality test suites to check the correctness of such devices is an important task. To estimate the quality of a test suite, a common approach is to simulate faults in a given circuit specification and to assess the fault coverage of the test suite. In this paper, we propose to use test suites derived at a high abstraction level, i.e. using Finite State Machines (FSMs), and to assess its fault coverage for three different types of faults. Those are single stuck-at faults, ‘bridge’ faults, and hardly detectable faults, which slightly modify the behavior of a single circuit gate. A set of tools was developed for this reason, and experimental results were obtained for a set of ITC'99 benchmarks (Second Release). The fault coverage for the proposed approach is over 90% in most of the cases.