Abstract Formal methods have been successfully used to develop advanced test generation techniques. While various test generation tools and test coverage criteria have been proposed, their adoption in industrial practice remains fragmented. This paper presents , a novel open-source toolset for testing C programs, which aims to facilitate the industrial application of diverse testing technologies by integrating them within a single framework. offers a comprehensive set of testing services, ranging from the specification of test objectives for selected test coverage criteria, through test case generation and the detection of uncoverable objectives, to the measurement of the resulting coverage. It integrates a rich set of analyzers: the fuzzer , the model-checker , the dynamic symbolic execution tool , and the static analyzer for detecting uncoverable test objectives. These analyzers enrich each other’s results through a shared store of test objectives and a shared corpus of test cases. Particular attention is paid to the careful handling of runtime errors and initialization functions, which are essential for industrial applications. Initial experiments confirm the benefits of the proposed toolset.

Several general search techniques such as genetic programming and simulated annealing have recently been investigated for synthesising programs from specifications of desired objective behaviours. In this context, these techniques explore the space of all candidate programs by performing local changes to candidates selected by means of a measure of their fitness w.r.t the desired objectives. Previous performance results advocated the use of simulated annealing over genetic programming for such problems. In this paper, we investigate the application of these techniques for the computation of deterministic strategies solving symbolic Discrete Controller Synthesis (DCS) problems, where a model of the system to control is given along with desired objective behaviours. We experimentally confirm that relative performance results are similar to program synthesis, and give a complexity analysis of our simulated annealing algorithm for symbolic DCS.

The ever growing complexity of software systems has led to the emergence of automated solutions for their management. The software assigned to this work is usually called an Autonomic Management System (AMS). It is ordinarily designed as a composition of several managers, which are pieces of software evaluating the dynamics of the system under management through measurements (e.g., workload, memory usage), taking decisions, and acting upon it so that it stays in a set of acceptable operating states. However, careless combination of managers may lead to inconsistencies in the taken decisions, and classical approaches dealing with these coordination problems often rely on intricate and ad hoc solutions. To tackle this problem, we take a global view and underscore that AMSs are intrinsically reactive, as they react to flows of monitoring data by emitting flows of reconfiguration actions. Therefore we propose a new approach for the design of AMSs, based on synchronous programming and discrete controller synthesis techniques. They provide us with high-level languages for modeling the system to manage, as well as means for statically guaranteeing the absence of logical coordination problems. Hence, they suit our main contribution, which is to obtain guarantees at design time about the absence of logical inconsistencies in the taken decisions. We detail our approach, illustrate it by designing an AMS for a realistic multi-tier application, and evaluate its practicality with an implementation.

In embedded systems, controlling a shared resource like a bus, or improving a property like power consumption, may be hard to achieve when programming device drivers individually. In this article, we propose a global resource control approach, based on a centralized view of the devices' states. The solution we propose operates on the hardware/software interface. It involves a simple adaptation of the application level, to communicate with the hardware via a control layer . The control layer itself is built from a set of simple automata: the device drivers, whose states correspond to functional or power consumption modes, and a controller to enforce global properties. All these automata are programmed using a synchronous language, and compiled into a single piece of C code. We take as example the node of a sensor network. We explain the approach in details, demonstrate its use and benefits with an event-driven or multithreading operating system, and draw guidelines for its use in other contexts.

In embedded systems, controlling a shared resource like the bus, or improving a property like power consumption, may be hard to achieve when programming device drivers individually. There is a need for global resource control, taking decisions based on a centralized view of the devices' states. In this paper, we study power consumption in sensor networks, where the nodes are small embedded systems powered by batteries. We concentrate on the hardware/software architecture of a node, where significant gains can be achieved by controlling the consumption modes of the various devices globally. The architecture we propose involves a simple adaptation of the application level, to communicate with the hardware via a control layer. The control layer itself is built from a set of simple automata: the drivers of the devices, whose states correspond to power consumption modes, and a controller that enforces global properties. All these automata are programmed using a synchronous language, whose compiler performs static scheduling and produces a single piece of C code. We explain the approach in details, demonstrate its use with either Contiki or a traditional multithreading operating system, and report on our experiments.