Search

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.

This paper continues the study of high quality test derivation for verifying digital components which are used in various physical systems; those are sensors, data transfer components, etc. We have used logic circuits b01-b010 of the package of ITC’99 benchmarks (Second Release) for experimental evaluation which as stated before, describe digital components of physical systems designed for various applications. Test sequences are derived for detecting the most known faults of the reference logic circuit using three different approaches to test derivation. Three widely used fault types such as stuck-at-faults, bridges, and faults which slightly modify the behavior of one gate are considered as possible faults of the reference behavior. The most interesting test sequences are short test sequences that can provide appropriate guarantees after testing, and thus, we experimentally study various approaches to the derivation of the so-called complete test suites which detect all fault types. In the first series of experiments, we compare two approaches for deriving complete test suites. In the first approach, a shortest test sequence is derived for testing each fault. In the second approach, a test sequence is pseudo-randomly generated by the use of an appropriate software for logic synthesis and verification (ABC system in our study) and thus, can be longer. However, after deleting sequences detecting the same set of faults, a test suite returned by the second approach is shorter. The latter underlines the fact that in many cases it is useless to spend ‘time and efforts’ for deriving a shortest distinguishing sequence; it is better to use the test minimization afterwards. The performed experiments also show that the use of only randomly generated test sequences is not very efficient since such sequences do not detect all the faults of any type. After reaching the fault coverage around 70%, saturation is observed, and the fault coverage cannot be increased anymore. For deriving high quality short test suites, the approach that is the combination of randomly generated sequences together with sequences which are aimed to detect faults not detected by random tests, allows to reach the good fault coverage using shortest test sequences.

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.

International audience; Computationally constrained devices are devices with typically low resources / computational power built for specific tasks. At the same time, recent advances in machine learning, e.g., deep learning or hierarchical or cascade compositions of machines, that allow to accurately predict / classify some values of interest such as quality, trust, etc., require high computational power. Often, such complicated machine learning configurations are possible due to advances in processing units, e.g., Graphical Processing Units (GPUs). Computationally constrained devices can also benefit from such advances and an immediate question arises: how? This paper is devoted to reply the stated question. Our approach proposes to use scalable representations of ‘trained' models through the synthesis of logic circuits. Furthermore, we showcase how a cascade machine learning composition can be achieved by using ‘traditional' digital electronic devices. To validate our approach, we present a set of prelimin ary experimental studies that show how different circuit apparatus clearly outperform (in terms of processing speed and resource consumption) current machine learning software implementations

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.