Model-based testing of event systems can take advantage of considering abstractions rather than explicit models, for controlling their size. A test is then a connected and reachable event sequence. This paper reports on experiments made when adapting for event systems two known under-approximation techniques of predicate tri-modal (may, must+, must-) abstractions. We first instantiate all the abstract may transitions, preferably as reachable instances. Second, we complete this under-approximation with instantiations of Ball chains, i.e. sequences in the shape of must-*may.must+* transitions, as such sequences are guaranteed to have connected instantiations. We present a backward symbolic instantiation algorithm for connecting these two under-approximations. We experimentally address the question of their complementarity. Surprisingly, our results show that Ball chains have not enhanced the coverage already achieved by the first step of may-transitions instantiation. However, it has enhanced the number of test steps by prolonging the already existing tests.

SUMMARY Developing efficient and automatic testing techniques is one of the major challenges faced by the software validation community. Recent work by A. Deniseet al.shows how to draw traces uniformly at random for testing large systems modelled by finite automata. Because finite automata are strong abstractions of systems, many test cases generated following this approach may be unconcretizable, that is, they do not correspond to any concrete execution of the system under test. In this paper, this problem is tackled by extending the approach to pushdown systems that can encode either a stack data structure or the call stack. The method is based on context‐free grammars and related algorithms, and relies on combinatorial techniques to guarantee the uniformity of generated traces. In addition, the combination of coverage criteria with random testing is investigated to benefit from both approaches for evaluating the quality of the test suites. The application of the random approach is illustrated within both structural and model‐based testing contexts. Copyright © 2014 John Wiley & Sons, Ltd.

Many verification problems can be reduced to a satisfiability problem modulo theories. For building satisfiability procedures the rewriting-based approach uses a general calculus for equational reasoning named paramodulation. Schematic paramodulation, in turn, provides means to reason on the derivations computed by paramodulation. Until now, schematic paramodulation was only studied for standard paramodulation. We present a schematic paramodulation calculus modulo a fragment of arithmetics, namely the theory of Integer Offsets. This new schematic calculus is used to prove the decidability of the satisfiability problem for some theories equipped with counting operators. We illustrate our theoretical contribution on theories representing extensions of classical data structures, e.g., lists and records. An implementation within the rewriting-based Maude system constitutes a practical contribution. It enables automatic decidability proofs for theories of practical use.

Component-based development is a commonly used technique to build complex systems. In order to satisfy specific requirements, adaptation policies provide a solution to dynamically reconfigure the component model with relation to its environment. This paper is dedicated to Fractal components assembling with a special emphasis on their reconfiguration. We introduce event-based adaptation policies to reconfigure Fractal components. The challenge is to build trustworthy systems and to simulate their executions when considering both functional and non-functional requirements. The contributions are illustrated on an example of an autonomous vehicle location system. Implementation details are given.

In this paper, we present a refinement verification for a class of parameterized systems. These systems are composed of an arbitrary number of similar processes. As in (Abdulla et al., 199) we represent the states by regular languages and the transitions by transducers over regular languages. If we can compute a symbolic model by acceleration of the actions, then we can also verify a refinement relation R between the symbolic models. We show that, under some conditions, if R is verified between two symbolic models, then refinement is verified between concrete parameterized systems. Then, we can take advantage of the property (safety and PLTL properties) preservation by refinement for their verification.