Latest News
| 04 Jan. 2010 | U3CAT will be present at the Grand Colloque STIC from 5 to 7 January in Paris (La Villette) |
| 27 Dec. 2009 | U3CAT web site is released. |
Presentation
U3CAT stands for Unification of Critical C Code Analysis Techniques. It is funded by the French National Research Agency ( Agence Nationale de la Recherche, ANR) under its 2008 ARPEGE program.
The main aim of the project is to provide embedded software developers with adequate tools allowing them to precisely state the properties that their application must meet and to statically verify that their implementation really respect them. Indeed, embedded software is increasingly prevalent in everyday life and very large applications (with hundreds of thousand lines of code when not millions) are now commonly embedded in various objects and are often used to perform critical tasks, for which a failure would result in serious economic loss or even casualties. This is in particular the case in aeronautics and in the automotive industry, where safety concerns are very high. In addition, as software grows in size, it becomes difficult to ensure that testing techniques provide an adequate coverage of all situations that may occur during the life of the system. As its name suggests, U3CAT targets C programs, which the case of the vast majority of embedded code, be it directly written in C or translated from some higher-level language (e.g. Scade).
U3CAT is centered around the main results of the 2005 RNTL CAT project, namely the Frama-C platform and the ACSL specification language.
Work packages
The main objective of U3CAT is to support wide adoption of static analysis techniques in the embedded software world. In order to reach this objective one has to drastically improve the existing tools and to ease their usage. Concretely, U3CAT will enhance, harden and promote the Frama-C framework.
The project will be divided in five technical work packages (WP), one management work package and one dissemination work package. The work packages fall either
- in the enhancement category (WP 1 Floating Point Analysis and WP 2 Temporal Properties). These work packages address the problem of the verification of properties in two specific domains that were not taken into account in the Frama-C framework but are fundamental for embedded software;
- or in the hardening category (WP 3 Combining Static Analysis Techniques, WP 4 Proof management, WP 5 Trusting Static Analysers). The methodological framework has to be hardened in the sense that whenever static analysis becomes too costly or even impossible to perform an alternative has to be available. The tools have to be hardened in the sense that the users must have evidence of their correctness;
- or in the promotion category (WP 6 Spreading Static Analysis). The Frama-C framework is Open Source software. As such, creating a community of users and a community of developers is critical for its future. Both of these communities must be actively supported to spread static analysis tools.