Combination methods for software verification = Méthodes de combinaison pour la vérification de logiciels

Daniele Zucchelli

Description

Sous la direction de Italie) Università degli studi (Milan, Michaël Rusinowitch, Silvio Ghilardi, Silvio Ranise
Thèse soutenue le 22 janvier 2008: Nancy 1
Cette thèse est consacrée au développement de méthodes formelles pour la vérification de logiciels. Parmi les techniques les plus utilisées dans ce contexte, il y en a deux qui permettent une spécification rigoureuse de toutes les exécutions possibles d'un système et le contrôle des bogues cachés. D'un côté, la correction d'un programme peut être garantie en démontrant l'insatisfiabilité d'une formule modulo une théorie qui axiomatise les types de données impliqués; de l'autre côté, les techniques de model-checking sont utilisées pour certifier que toute exécution possible du système satisfait les propriétés désirées. Les contributions de cette thèse sont les suivantes. Dans un premier temps, nous donnons un résultat de décidabilité pour la satisfiabilité de contraintes pour des extensions intéressantes de la théories des tableaux. Ensuite, nous avons obtenu des résultats dans le prolongement de Manna et Pnueli qui ont montré qu'un mélange de la logique du premier ordre et de la logique temporelle linéaire suffit pour énoncer les problèmes de vérification pour la classe des systèmes réactifs. Ainsi, nous nous inspirons de la récente littérature sur la combinaison des procédures de décision pour établir des résultats de décidabilité et d'indécidabilité pour le problème de satisfiabilité pour des logiques permettant d'intégrer du raisonnement modulo des théories du premier ordre dans un cadre temporel. Les résultats qu'on obtient pour la logiques temporelle linéaire sont ensuite généralisés au cas où le flux temporel est décrit par une logique dont le problème de la satisfiabilité relativisée est décidable. Notre dernière contribution est la décidabilité du problème du model-checking pour le flux temporel linéaire, sous des hypothèses appropriées concernant les théories du premier ordre impliquées. La preuve de ce résultat indique qu'on pourrait employer avec succès des Solveurs Modulo des Théories dans les applications du model-checking aux systèmes ayant un nombre infini d'états.
-Méthodes de Combinaison
The thesis is devoted to the development of formal methods for software verification. Indeed, two are among the most widespread techniques that allow to rigorously specify the possible executions of a system and check whether it contains bugs. On the one hand, correctness of a program can be guaranteed by showing the unsatisfiability of a formula modulo a theory which usually axiomatizes the involved datatypes; on the other hand, model checking techniques are used to certify that every possible run of the system satisfies the desired properties. The contributions of the thesis are the following: First of all, we give decidability result for the constraint satisfiability problem for interesting extensions of the theory of arrays. Secondly, along the lines of Manna and Pnueli, who have shown how a mixture of first-order logic and linear time temporal logic is sufficient to state verification problems for the class of reactive systems, we draw on the recent literature about combination of decision procedures to give decidability and undecidability results for the satisfiability problem for logics that allow to plug reasoning modulo first-order theories into a temporal setting. The results obtained in the case of linear flows of time are then generalized to temporal and modal logics whose relativized satisfiability problem is decidable. The last contribution is the decidability of the model checking problem for linear flows of time under suitable hypothesis over the first-order theories involved. The proofs of the decidability results suggest that efficient Satisfiability Modulo Theories solvers might be successfully employed in the model checking of infinite-state systems.
Source: http://www.theses.fr/2008NAN10006/document

Informations

• Publié par: Thesee
• Nombre de lectures: 21
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

AVERTISSEMENT

Ce document est le fruit d'un long travail approuvé par le
jury de soutenance et mis à disposition de l'ensemble de la
communauté universitaire élargie.

Il est soumis à la propriété intellectuelle de l'auteur. Ceci
implique une obligation de citation et de référencement lors
de l’utilisation de ce document.

Toute contrefaçon, plagiat, reproduction illicite encourt une
poursuite pénale.


➢ Contact SCD Nancy 1 : [e-mail]




LIENS


Code de la Propriété Intellectuelle. articles L 122. 4
Code de la Propriété Intellectuelle. articles L 335.2- L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm `UNIVERSITADEGLISTUDIDIMILANO
`FACOLTA DI SCIENZE MATEMATICHE, FISICHE E NATURALI
Dipartimento di Scienze dell’Informazione
DOTTORATO DI RICERCA IN INFORMATICA
XX CICLO
Settore scientifico-disciplinare INF/01
Combination Methods
for Software Verification
Tesi di Dottorato di Ricerca di:
Daniele Zucchelli
Relatori:
Prof. Silvio Ghilardi
¨Dr. Michael Rusinowitch
Correlatore:
Dr. Silvio Ranise
Coordinatore del Dottorato:
Prof. Vincenzo Piuri
ANNO ACCADEMICO 2006/2007´D´epartement de formation doctorale en informatique Ecole doctorale IAEM Lorraine
UFR STMIA
M´ethodes de Combinaison
pour la V´erification de Logiciels
`THESE
pr´esent´ee et soutenue publiquement le 22 janvier 2008
pour l’obtention du
Doctorat de l’universit´e Henri Poincar´e – Nancy 1
(sp´ecialit´e informatique)
par
Daniele Zucchelli
Composition du jury
Pr´esident : Didier Galmiche
Rapporteurs : Alessandro Armando Professeur `a l’Universit´e de Genova, Italie
Ahmed Bouajjani Professeur a` l’Universit´e Paris 7, France
Alessandro Cimatti Chercheur a` l’ITC, Italie
Andreas Herzig Directeur de Recherche au CNRS, France
Examinateurs : Didier Galmiche Professeur `a l’Universit´e Henri Poincar´e, France
Directeurs : Silvio Ghilardi Professeur `a l’Universit´e de Milano, Italie
Silvio Ranise Charg´e de Recherche a` l’INRIA Lorraine, France
Micha¨el Rusinowitch Directeur de Recherche a` l’INRIA Lorraine, France
Laboratoire Lorrain de Recherche en Informatique et ses Applications — UMR 7503Abstract
The thesis is devoted to the development of formal methods for software verification.
Indeed, two are among the most widespread techniques that allow to rigorously specify the
possible executions of a system and check whether it contains bugs. On the one hand, the
correctness of a program can be guaranteed by showing the unsatisfiability of a formula
modulo a theory which usually axiomatizes the involved datatypes; on the other hand, the
model checking techniques are used to certify that every possible run of the system satisfies
the desired properties. The contributions of the thesis are the following: First of all, we
give a decidability result for the constraint satisfiability problem for interesting extensions
of the theory of arrays. Secondly, along the lines of Manna and Pnueli, who have shown
how a mixture of first-order logic and linear time temporal logic is sufficient to state the
verificationproblemsfortheclassofreactivesystems,wedrawontherecentliteratureabout
the combination of decision procedures to give decidability and undecidability results for
the satisfiability problem for logics that allow to plug reasoning modulo first-order theories
into a temporal setting. The results obtained in the case of linear flows of time are then
generalized to the temporal and modal logics whose relativized satisfiability problem is
decidable. The last contribution is the decidability of the model checking problem for linear
flows of time under suitable hypothesis over the first-order theories involved. The proofs of
the decidabilityresults suggestthat efficient Satisfiability Modulo Theoriessolversmight be
successfully employed in the model checking of infinite-state systems.
Keywords: Combination Methods, Model Checking, Decision Procedures.
R´esum´e
Cette th`ese est consacr´ee au d´eveloppement de m´ethodes formelles pour la v´erification
de logiciels. Parmi les techniques les plus utilis´ees dans ce contexte, il y en a deux qui
permettent une sp´ecification rigoureuse de toutes les ex´ecutions possibles d’un syst`eme et
le contrˆole des bogues cach´es. D’un cˆot´e, la correction d’un programme peut ˆetre garantie
en d´emontrant l’insatisfiabilit´e d’une formule modulo une th´eorie qui axiomatise les types
de donn´ees impliqu´es; de l’autre coˆt´e, les techniques de model-checking sont utilis´ees pour
certifier que toute ex´ecution possible du syst`eme satisfait les propri´et´esd´esir´ees.Les contri-
butions de cette th`ese sont les suivantes. Dans un premier temps, nous donnons un r´esultat
de d´ecidabilit´e pour la satisfiabilit´e de contraintes pour des extensions int´eressantes de la
th´eories des tableaux. Ensuite, nous avons obtenu des r´esultats dans le prolongement de
Manna et Pnueli qui ont montr´e qu’un m´elange de la logique du premier ordre et de la
logique temporelle lin´eaire suffit pour ´enoncer les probl`emes de v´erification pour la classe
des syst`emes r´eactifs. Ainsi, nous nous inspirons de la r´ecente litt´erature sur la combinai-
son des proc´edures de d´ecision pour ´etablir des r´esultats de d´ecidabilit´e et d’ind´ecidabilit´e
pour le probl`eme de satisfiabilit´e pour des logiques permettant d’int´egrer du raisonnement
modulo des th´eories du premier ordre dans un cadre temporel. Les r´esultats qu’on obtient
pour la logiques temporelle lin´eaire sont ensuite g´en´eralis´es au cas ou` le flux temporel est
d´ecrit par une logique dont le probl`eme de la satisfiabilit´e relativis´ee est d´ecidable. Notre
derni`ere contribution est la d´ecidabilit´e du probl`eme du model-checking pour le flux tem-
porel lin´eaire, sous des hypoth`eses appropri´ees concernant les th´eories du premier ordre
impliqu´ees. La preuve de ce r´esultat indique qu’on pourrait employer avec succ`es des Sol-
veurs Modulo des Th´eories dans les applications du model-checking aux syst`emes ayant un
nombre infini d’´etats.
Mots cl´es : M´ethodes de Combinaison, Model Checking, Proc´edures de D´ecisions.Contents
´R´esum´e Etendu vii
Introduction xvii
The Context . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xviii
The Satisfiability Problem . . . . . . . . . . . . . . . . . . . . . . . . xix
Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xxi
Our Contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xxvi
Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xxix
1 Non-Disjoint Combination 1
1.1 Formal preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.1.1 First-Order Logic . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.1.2 Disjoint Combination . . . . . . . . . . . . . . . . . . . . . . 4
1.1.3 Basic Facts in Model Theory . . . . . . . . . . . . . . . . . . 6
1.2 Compatible Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.2.1 Locally Finite Theories . . . . . . . . . . . . . . . . . . . . . 9
1.2.2 Noetherian Theories . . . . . . . . . . . . . . . . . . . . . . . 10
1.3 Combination Results for Non-Disjoint Theories . . . . . . . . . . . . 14
1.3.1 The Locally Finite Case . . . . . . . . . . . . . . . . . . . . . 15
1.3.2 The Noetherian Case . . . . . . . . . . . . . . . . . . . . . . . 17
1.3.3 Interesting Properties . . . . . . . . . . . . . . . . . . . . . . 22
1.3.4 Mathematical Remarks . . . . . . . . . . . . . . . . . . . . . 27
1.4 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1.5 The Theory of a Free Unary Function Symbol . . . . . . . . . . . . . 34
1.6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
2 Satisfiability in Temporal and Modal Logics 43
2.1 Temporalizing a First-Order Theory . . . . . . . . . . . . . . . . . . 44
2.1.1 Recursive Enumerability of the Validity Problem . . . . . . . 48
2.1.2 Some Classes of Data-Flow Theories and Further Assumptions 49
2.2 Undecidability of the Satisfiability Problem . . . . . . . . . . . . . . 51
2.3 Decidability and Locally Finite Data-Flow Theories . . . . . . . . . 52
2.3.1 Propositional Linear Time Temporal Logic . . . . . . . . . . 53
vvi Contents
2.3.2 Eager Reduction to Propositional LTL-Satisfiability . . . . . 54
2.3.3 A Lazy Tableau Procedure . . . . . . . . . . . . . . . . . . . 59
2.4 Decidability and Noetherian Compatible Data-Flow Theories . . . . 61
2.5 Extensions to Abstract Temporal Logics . . . . . . . . . . . . . . . . 66
2.6 Conclusions and Related Work . . . . . . . . . . . . . . . . . . . . . 69
3 Model Checking 71
3.1 LTL-System S