Aide à la vérification de programmes concurrents par transformation de code et de spécifications
Vérifier formellement des programmes concurrents est une tâche difficile. S il existe différentes techniques pour la réaliser, très peu sont effectivement mises en oeuvre pour des programmes écrits dans des langages de programmation réalistes. En revanche, les techniques de vérification formelles de...
Gorde:
| Egile nagusia: | |
|---|---|
| Beste egile batzuk: | , , , , , , , |
| Formatua: | Thèse numérique |
| Hizkuntza: | Français |
| Argitaratua: |
2016.
|
| Gaiak: | |
| Sarrera elektronikoa: | Accès au texte intégral https://theses.univ-orleans.fr/public/2016ORLE2073_va.pdf http://www.theses.fr/2016ORLE2073/abes |
| Oharra: |
Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : École doctorale Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes (Centre-Val de Loire ; 2012-....) Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire) Autre(s) contribution(s) : Sébastien Limet (Président du jury) ; Frédéric Loulergue, Sébastien Limet, Catherine Dubois, Sylvain Conchon, Jan-Georg Smaus, Nikolaï Kosmatov, Stephan Merz, Louis Rilling (Membre(s) du jury) ; Catherine Dubois, Sylvain Conchon (Rapporteur(s)) |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | Assisted concurrent program verification by code and specification transformation |
| LEADER | 05690nam a22004577a 4500 | ||
|---|---|---|---|
| 001 | 626873 | ||
| 008 | 170904s2016 xxe ||| |||| 00| 0 fre d | ||
| 009 | PPN203842170 | ||
| 041 | 0 | |a fre |b fre |b eng | |
| 082 | |a 005.13 | ||
| 084 | |a 004 | ||
| 100 | 1 | |a Blanchard, Allan, |d 1990- | |
| 240 | 1 | 0 | |a Assisted concurrent program verification by code and specification transformation |
| 245 | 1 | 0 | |a Aide à la vérification de programmes concurrents par transformation de code et de spécifications |c Allan Blanchard ; sous la direction de Frédéric Loulergue. |
| 256 | |a Données textuelles | ||
| 260 | |c 2016. | ||
| 500 | |a Titre provenant de l'écran-titre | ||
| 500 | |a Ecole(s) Doctorale(s) : École doctorale Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes (Centre-Val de Loire ; 2012-....) | ||
| 500 | |a Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire) | ||
| 500 | |a Autre(s) contribution(s) : Sébastien Limet (Président du jury) ; Frédéric Loulergue, Sébastien Limet, Catherine Dubois, Sylvain Conchon, Jan-Georg Smaus, Nikolaï Kosmatov, Stephan Merz, Louis Rilling (Membre(s) du jury) ; Catherine Dubois, Sylvain Conchon (Rapporteur(s)) | ||
| 502 | |a Thèse de doctorat. Informatique. Orléans. 2016 | ||
| 520 | |a Vérifier formellement des programmes concurrents est une tâche difficile. S il existe différentes techniques pour la réaliser, très peu sont effectivement mises en oeuvre pour des programmes écrits dans des langages de programmation réalistes. En revanche, les techniques de vérification formelles de programmes séquentiels sont utilisées avec succès depuis plusieurs années déjà, et permettent d atteindre de hauts degrés de confiance dans nos systèmes. Cette thèse propose une alternative aux méthodes d analyses dédiées à la vérification de programmes concurrents consistant à transformer le programme concurrent en un programme séquentiel pour le rendre analysable par des outils dédiés aux programmes séquentiels. Nous nous plaçons dans le contexte de FRAMA-C, une plate-forme d analyse de code C spécifié avec le langage ACSL. Les différentes analyses de FRAMA-C sont des greffons à la plate-forme, ceux-ci sont à ce jour majoritairement dédiés aux programmes séquentiels. La méthode de vérification que nous proposons est appliquée manuellement à la vérification d un code concurrent issu d un hyperviseur. Nous automatisons la méthode à travers un nouveau greffon à FRAMA-C qui permet de produire automatiquement, depuis un programme concurrent spécifié, un programme séquentiel spécifié équivalent. Nous présentons les bases de sa formalisation, ayant pour but d en prouver la validité. Cette validité n est valable que pour la classe des programmes séquentiellement consistant. Nous proposons donc finalement un prototype de solveur de contraintes pour les modèles mémoire faibles, capable de déterminer si un programme appartient bien à cette classe en fonction du modèle mémoire cible. | ||
| 520 | |a Formal verification of concurrent programs is a hard task. There exists different methods to perform such a task, but very few are applied to the verification of programs written using real life programming languages. On the other side, formal verification of sequential programs is successfully applied for many years, and allows to get high confidence in our systems. As an alternative to dedicated concurrent program analyses, we propose a method to transform concurrent programs into sequential ones to make them analyzable by tools dedicated to sequential programs. This work takes place within the analysis framework FRAMA-C, dedicated to the analysis of C code specified with ACSL. The different analyses provided by FRAMA-C are plugins to the framework, which are currently mostly dedicated to sequential programs. We apply this method to the verification of a concurrent code taken from an hypervisor. We describe the automation of the method implemented by a new plugin to FRAMAC that allow to produce, from a specified concurrent program, an equivalent specified sequential program. We present the basis of a formalization of the method with the objective to prove its validity. This validity is admissible only for the class of sequentially consistent programs. So, we finally propose a prototype of constraint solver for weak memory models, which is able to determine whether a program is in this class or not, depending on the targeted hardware. | ||
| 538 | |a Configuration requise : un logiciel capable de lire un fichier au format : PDF | ||
| 650 | |a Logiciels |x Vérification | ||
| 650 | |a Codage | ||
| 650 | |a ACSL (langage de programmation) | ||
| 650 | |a Thèses et écrits académiques | ||
| 700 | 1 | |a Loulergue, Frédéric, |d 1973- |4 ths |4 opn | |
| 700 | 1 | |a Limet, Sébastien, |d 19..-...., |c professeur en informatique. |4 opn | |
| 700 | 1 | |a Dubois, Catherine, |d 19..-...., |c informaticienne. |4 opn | |
| 700 | 1 | |a Conchon, Sylvain, |d 1972- |4 opn | |
| 700 | 1 | |a Smaus, Jan-Georg, |c enseignant-chercheur en informatique. |4 opn | |
| 700 | 1 | |a Kosmatov, Nikolaï, |d 1975- |4 opn | |
| 700 | 1 | |a Merz, Stephan, |d 19..- |4 opn | |
| 700 | 1 | |a Rilling, Louis, |d 1980- |4 opn | |
| 710 | 2 | |a Université d'Orléans. |4 dgg | |
| 856 | 4 | |q PDF |s 1803259 |u http://www.theses.fr/2016ORLE2073/document |z Accès au texte intégral | |
| 856 | 4 | |u https://theses.univ-orleans.fr/public/2016ORLE2073_va.pdf | |
| 856 | 4 | |u http://www.theses.fr/2016ORLE2073/abes | |
| 997 | |0 626873 |1 Thèse numérique |a Ressource numérique |b INSA |b ENSA |c 0/Bibliothèque numérique/ |c 1/Bibliothèque numérique/Autre ressource numérique/ | ||