Étendre la spécification de programmes C concurrents et les vérifier par une transformation de source à source

L'utilisation croissante de systèmes informatiques critiques et l'augmentation de leur complexité rendent leur bon fonctionnement essentiel. Le model-checking logiciel permet de prouver formellement l'absence d'erreurs dans un programme. Il reste cependant limité par deux facteurs : l'explosion combinatoire et la capacité à spécifier le comportement correct d'un programme. Ces deux problèmes sont amplifiés dans le cas de programmes concurrents, à cause des différents entrelacements possibles entre les fils d'exécutions. Les assertions et les formules logiques LTL sont les deux formalismes de spécification les plus utilisés dans le cadre du model-checking logiciel. Cependant, ils sont limités dans un contexte concurrent : les assertions ne permettent pas d'exprimer des relations temporelles entre différents fils d'exécutions alors que les formules LTL utilisées par les outils actuels ne permettent pas d'exprimer des propriétés sur les variables locales et les positions dans le code du programme. Ces notions sont pourtant importantes dans le cas de programmes concurrents. Dans ce mémoire, nous établissons un formalisme de spécification visant à corriger ces limitations. Ce formalisme englobe LTL et les assertions, en permettant d'exprimer des relations temporelles sur des propositions faisant intervenir les variables locales et globales d'un programme ainsi que les positions dans le code source. Nous présentons aussi un outil permettant de vérifier une spécification exprimée dans ce formalisme dans le cas d'un programme concurrent codé en C. Notre formalisme se base sur la logique LTL. Il permet de surmonter deux des principales limitations rencontrées par les variantes de LTL utilisées par les outils de model-checking logiciel : manipuler des positions dans le code et des variables locales dans les propositions atomiques. La principale difficulté est de définir correctement dans l'ensemble du programme une proposition atomique lorsqu'elle dépend d'une variable locale. En effet, cette variable locale n'a de sens que dans une partie limitée du programme. Nous résolvons ce problème en utilisant le concept de zones de validité. Une zone de validité est un intervalle de positions dans le code source du programme dans laquelle la valeur d'une proposition atomique est définie à l'aide de sa fonction d'évaluation. Une valeur par défaut est utilisée hors de la zone de validité. Ceci permet de limiter l'utilisation de la fonction d'évaluation aux contextes où tous ses paramètres locaux sont définis.

Abstract

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 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.