3-Abstract.tex

% Abstract
%
%   Résumé de la recherche écrit en anglais sans être
% une traduction mot à mot du résumé écrit en français.

\chapter*{ABSTRACT}\thispagestyle{headings}
\addcontentsline{toc}{compteur}{ABSTRACT}
%
\begin{otherlanguage}{english}

Critical programs and IT systems are more and more broadly used. Simultaneously,
their complexity increase. More than ever, it is crucial to ensure their
correctness. Software model-checking is a verification technique that allows to
formally prove the absence of errors in a program. However, it faces two main
issues: combinatorial explosion and the ability to specify the correct behavior
of a program. These issues are amplified for concurrent programs because of the
interleaving between threads. Assertions and LTL formulas are the most used
specification formalism for software model-checking. However they are
restricted in a concurrent context. On the one hand, it is not possible to
express temporal relations between threads or events of the program using only
assertions. On the other hand, LTL formulas that are supported by the main
software model-checkers does not allow to use local variables and program
locations, whereas program locations are often a convenient way to check the
synchronization between threads.

In this report, we establish a specification formalism aiming to overcome these
issues. This formalism is a superset of both LTL and assertions. It allows to
express propositions that use global and local variables and propositions, and to
build temporal relations on these propositions. Then, we introduce a tool
allowing to check for the correctness of concurrent C programs specified with
the formalism we introduce.

Our formalism is based on the LTL logic. It tackles the problems of code location
manipulation in specification and the use of local variable
in atomic propositions. The main difficulty is to properly define an atomic
proposition in the whole program when it depends on a local variable, as the
local variable is defined only in part of the program. We solve this issue using
the concept of \emph{validity area}. A validity area is an interval of code
locations in which the value of an atomic proposition is computed using its
evaluation function. A default value is used out of the validity area. Hence, it
is possible to limit the use of the evaluation function to the lexical contexts
where all local parameters are defined.

We developed a tool named \texttt{baProduct} to verify concurrent C programs
specified using our formalism. This tool implements a source to source
transformation and calls backend model-checkers to perform verification tasks.
This architecture greatly simplifies the development of the tool and supports a
variety of model-checkers in backend. It allows us to take advantage of the
optimization of state-of-the-art model-checkers and to compare their
performances when used in combination with our tool.
We base the source to source transformation upon the implementation in C of the
Büchi automaton associated with the specification. We build the product of this
automaton with the source code of the system.

Afterward, we apply \texttt{baProduct} on a set of tests. We evaluate its
performances using two model-checkers as backend, CBMC and ESBMC. We get better
performances with CBMC due to difference in the way these tools handle
concurrency. The tests confirm it is possible to conveniently specify properties
(such as mutual exclusion properties) that are difficult to express using only
assertions or a more classical version of LTL, without manual modifications of
the source code. We also demonstrate that our transformation successfully reduces
the problem of verification of LTL properties to the verification of
assertions for finite traces. However, our tool faces some limitations. It is
currently restricted to finite traces. Moreover, this version does not
implement any reduction method, which reduces its performances.

\end{otherlanguage}