Currently writting/submitting

• Quantity of Resource Properties Expression and Runtime Assurance for Embedded Systems : submitted to AICCSA09
• Abstract Acceleration in Linear Relation Analysis : journal paper for FMSD submission.

Quantity of Resource Properties Expression and Runtime Assurance for Embedded Systems : accepted to AICCSA09, Rabat, Maroc

Runtime resource assurance and adaptation with Qinna framework~: a case study - RTS 2008

Even if hardware improvements have increased the performance of embedded systems in the last years, resource problems are still acute. The persisting problem is the constantly growing complexity of systems. New devices for service such as PDAs or smartphones increase the need for flexible and adaptive open software. Component-based software engineering tries to address these problems and one key point for development is the Quality of Service (QoS) coming from resource constraints. In this paper, we recall the concepts behind Qinna, a component-based QoS Architecture, which was designed to manage QoS issues, and we illustrate the developpement of a image viewer application whithin this framework. We focus on the general developpement methodology of resource-aware applications with Qinna framework, from the specification of resource constraints to the use of generic Qinna's algorithms for negociating QoS contracts at runtime.

Combining widening and acceleration in Linear Relation Analysis - SAS06

Linear Relation Analysis [cousot78,halbwach79] is one of the first, but still one of the most powerful, abstract interpretations working in an infinite lattice. As such, it makes use of a widening operator to enforce the convergence of fixpoint computations. While the approximation due to widening can be arbitrarily refined by delaying the application of widening, the analysis quickly becomes too expensive with the increase of delay. Previous attempts at improving the precision of widening are not completely satisfactory, since none of them is guaranteed to improve the precision of the result, and they can nevertheless increase the cost of the analysis. In this paper, we investigate an improvement of Linear Relation Analysis consisting in computing, when possible, the exact (abstract) effect of a loop. This technique is fully compatible with the use of widening, and whenever it applies, it improves both the precision and the performance of the analysis.

Some ways to reduce the space dimension in polyhedra computations [journal] - FMSD06

Convex polyhedra are often used to approximate sets of states of programs involving numerical variables. The manipulation of convex polyhedra relies on the so-called double description, consisting of viewing a polyhedron both as the set of solutions of a system of linear inequalities, and as the convex hull of a system of generators, i.e., a set of vertices and rays. The cost of these manipulations is highly dependent on the number of numerical variables, since the size of each representation can be exponential in the dimension of the space. In this paper, we investigate some ways for reducing the dimension: On one hand, when a polyhedron satisfies affine equations, these equations can obviously be used to eliminate some variables. On the other hand, when groups of variables are unrelated with each other, this means that the polyhedron is in fact a Cartesian product of polyhedra of lower dimensions. Detecting such Cartesian factoring is not very difficult, but we adapt also the operations to work on Cartesian products. Finally, we extend the applicability of Cartesian factoring by applying suitable variable change in order to maximize the factoring.

From Discrete Duration Calculus to Symbolic Automata - SLAP 04

The goal of this paper is to translate (fragments of) the quantified discrete duration calculus QDDC, proposed by P. Pandya, into symbolic acceptors with counters. Acceptors are written in the synchronous programming language Lustre, in order to allow available symbolic verification tools (model-checkers, abstract interpreters) to be applied to properties expressed in QDDC. We show that important constructs of QDDC need non-deterministic acceptors, in order to be translated with a bounded number of counters, and an expressive fragment of the logic is identified and translated. Then, we consider a more restricted fragment, which only needs deterministic acceptors.

Technical and Research Reports

• Resource management with Qinna framework : the remote viewer case study : Inria Technical Report number 6562, on hal server [bib].

Even if hardware improvements have increase the performance of embedded systems in the last years, resource problems are still accurate. In fact, the persisting problem is the constantly growing complexity of systems. In addition, new supports of service such as PDAs or smartphones increase the need for flexible and adaptable open software. Component-based software engineering tries to address these problems and one key point for development is the Quality of Service (QoS) coming from resource constraints. In this technical report, we recall the concepts behind Qinna, a component-based QoS Architecture, which was designed to manage QoS issues, and we illustrate the developpement of a image viewer application whithin this framework. We focus on the general developpement methodology of resource-aware applications with Qinna framework, from the specification of resource constraints to the use of generic Qinna's algorithms for negociating QoS contracts at runtime.

• Resource Properties Expression and Runtime assurance for embedded programs, using Qinna, a component-based software architecture : Inria Research report number 6565, on hal server [bib].

Designing embedded communicating systems such as PDAs, mobile phones, is getting more and more complex as the hardware performance grows. The component paradigm appears as promising mainly due to the reusability and flexibility of code, but new problems appear such as security, safety and quality of service managements, which have not been integrated in the component-based designs. In this context, a component-based software architecture, Qinna, has been designed to manage quality of service from the resource point of view. In this research report, we propose a complete formalization of resource constraints expression and management using Qinna, and illustrate on a classic case study.