Accelerated Invariant Generation for C Programs with Aspic and C2fsm - TAPAS 2010 (with P. Feautrier)

In this paper, we present Aspic, an automatic polyhedral invariant generation tool for flowcharts programs. Aspic implements an improved Linear Relation Analysis on numeric counter automata. The "accelerated" method improves precision by computing locally a precise overapproximation of a loop without using the widening operator. C2fsm is a C preprocessor that generates automata in the format required by Aspic. The experimental results show the performance and precision of the tools.

Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs - SAS 2010 (with C. Alias, A. Darte, P. Feautrier)

Proving the termination of a flowchart program can be done by exhibiting a ranking function, i.e., a function from the program states to a well-founded set, which strictly decreases at each program step. A standard method to automatically generate such a function is to compute invariants for each program point and to search for a ranking in a restricted class of functions that can be handled with linear programming techniques. Previous algorithms based on affine rankings either are applicable only to simple loops (i.e., single-node flowcharts) and rely on enumeration, or are not complete in the sense that they are not guaranteed to find a ranking in the class of functions they consider, if one exists. Our first contribution is to propose an efficient algorithm to compute ranking functions: It can handle flowcharts of arbitrary structure, the class of candidate rankings it explores is larger, and our method, although greedy, is provably complete. Our second contribution is to show how to use the ranking functions we generate to get upper bounds for the computational complexity (number of transitions) of the source program. This estimate is a polynomial, which means that we can handle programs with more than linear complexity. We applied the method on a collection of test cases from the literature. We also show the links and differences with previous techniques based on the insertion of counters.

Qinna: a component-based framework for runtime safe resource adaptation of embedded systems (Journal Version SCPE 2009) with JP Babau

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, which increase the need for reusable developpement framework and pieces of code. In the case of PDAs and smartphones, in addition to classical needs (safety, security), developers must deal with quality of service (QoS) constraints , such as resource management. Qinna was designed to face with these problems. In this paper, we propose a complete framework to express ressource constraints during the developpement process. We propose a component-based architecture, which generic components and algorithms, and a developpement methodology, to manage QoS issues while developing an embedded software. The obtained software is then able to automatically adapt his behaviour to the physical resources, thanks to << degraded modes>>. We illustrate the methodology and the use of Qinna within a case study.

Quantity of Resource Properties Expression and Runtime Assurance for Embedded Systems - AICCSA09 (with J.P. Babau)

Recent work on component-based software design has proved the need of resource-accurate development of embedded software. In the more specific cases of mobile systems, the developer also needs tools to facilitate the adaptation of functionalities to resources (lack of memory or bandwidth, \etc), and also to evaluate the performance w.r.t. the resource issues. As we want to design and develop at the same time the application and its resource controllers, we chose to use Qinna, which was designed to manage resource issues (specification, contractualization, management) during the development process of such an application. We propose a complete formalization of the resource constraints specification, through the use of a variant of the event-based logics, MEDL and PEDL introduced in \cite{lee99runtime}. Qinna then automatically performs the runtime resource assurance. We illustrate this work in a case study.

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

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 (with N. Halbwachs)

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 (with N. Halbwachs and D. Merchat)

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 (with N. Halbwachs and P. Raymond)

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

• Abstract Interpretation in Linear Relation Analysis (extended version): LIFL Research Report, with P. Schrammel on HAL
• Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction : with P. Feautrier and A. Gamatié, LIFL research Report, on HAL
• Interface graphique de simulation de processus communicants : with JM Vincenti and C. Alias, LIFL technical Report (fr), PDF
• Abstract interpretation to improve precision of Linear Relation Analysis: Verimag Research Report TR-2010-03, with N. Halbwachs [bib], [pdf].
• Formally Tracing Back executions From an Analysis Tool Back to a Domain Specific Modeling Language's Operational Semantics : Inria Research Report number 7423, with V. Rusu and B. Combemale on hal.
• Bounding the Computational Complexity of Flowchart Programs with Multi-dimensional Rankings : Inria Research Report number 7235, with C. Alias, A. Darte and P. Feautrier on hal server [bib].
Same topic as RR7037, but more details about implementation and case studies. The previous one is more about proofs.
• Program Termination and Worst Time Complexity with Multi-Dimensional Affine Ranking Functions : Inria Research Report number 7037 with with C. Alias, A. Darte, P. Feautrier and C. Quinson on hal server [bib].

A standard method for proving the termination of a flowchart program is to exhibit a ranking function, i.e., a function from the program states to a well-founded set, which strictly decreases at each program step. Our main contribution is to give an efficient algorithm for the automatic generation of multi-dimensional affine nonnegative ranking functions, a restricted class of ranking functions that can be handled with linear programming techniques. Our algorithm is based on the combination of the generation of invariants (a technique from abstract interpretation) and on an adaptation of multi-dimensional affine scheduling (a technique from automatic parallelization). We also prove the completeness of our technique with respect to its input and the class of rankings we consider. Finally, as a byproduct, by computing the cardinal of the range of the ranking function, we obtain an upper bound for the computational complexity of the source program, which does not depend on restrictions on the shape of loops or on program structure. This estimate is a polynomial, which means that we can handle programs with more than linear complexity. The method is tested on a large collection of test cases from the literature. We also point out future improvements to handle larger programs.

• Resource management with Qinna framework : the remote viewer case study : Inria Technical Report number 6562, with J.P. Babau 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, with J.-P. babau, 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.