|
 
|
[Car09a] Test automatique de propriétés dans un atelier de développement de logiciels sûrs
Mémoire de Thèse : Soutenue le: 07 October 2009, pp. 186, pp.: Directeur: C. DuboisRapporteur 1: I. Parissis
Rapporteur 2: B. Wolff
Membre du jury: A. Gotlieb
Membre du jury: T. Hardin
Membre du jury: P. Le Gall, : Automatic test of properties in a safe software development environment,
Mots clés: test automatique, test de propriété, méta-contrainte, préservation sémantique, programmation par contraintes, programme certifié, FoCal
Résumé:
L'environnement Focal, développé conjointement par des chercheurs des
laboratoires CÉDRIC, LIP6 et de l'INRIA, permet de construire de manière
incrémentale des composants de bibliothèque avec un haut niveau de confiance et
de qualité. Un composant de bibliothèque Focal peut contenir des
spécifications, l'implantation des opérations spécifiées et des preuves que la
spécification et l'implantation sont en conformité. Les composants Focal sont
traduits en code exécutable OCaml et vérifiés par l'assistant à la preuve Coq.
Même si un développement en Focal nous assure un haut degré de confiance dans
le programme, de par une spécification formelle et les preuves de correction,
nous ne pouvons nous passer du test. Les propriétés de bas niveau, comme les
axiomes, ne sont en général pas prouvées. Focal autorise l'importation de code
non sûr au sein de code Focal certifié, ce qui peut amener à « casser » la
spécification. Finalement, le test peut être utilisé pour avoir confiance en
une implantation dont la preuve de correction n'est pas encore effectuée ou
terminée ou lorsqu'une tentative de preuve échoue, pour trouver des
contre-exemples.
Ce manuscrit présente le développement d'un outil de test intégré à Focal. La
méthodologie repose sur le test automatique de propriétés. Les jeux de test
sont définis comme des valuations des variables quantifiées de la propriété
sous test, qui satisfont les prémisses de la propriété (précondition). La
conclusion de la propriété sert d'oracle pour le test. Nous proposons deux
stratégies de recherche des jeux de test : aléatoire et par résolution de
contraintes. Pour cette dernière, nous traduisons la précondition de la
propriété en un système de contraintes. Sa résolution nous permet d'obtenir les
jeux de test recherchés. Cette méthodologie est formellement définie et nous
prouvons que les jeux de test ainsi construits satisfont la précondition.
Equipe:
sys
BibTeX
| @phdthesis { | |||
| Car09a, | |||
| title | = | "{Test automatique de propriétés dans un atelier de développement de logiciels sûrs}", | |
| author | = | "M. Carlier", | |
| year | = | 2009, | |
| pages | = | "186", | |
| address | = | "{CEDRIC Laboratory, Paris, France}", | |
| note | = | "{ Directeur: C. Dubois Rapporteur 1: I. Parissis Rapporteur 2: B. Wolff Membre du jury: A. Gotlieb Membre du jury: T. Hardin Membre du jury: P. Le Gall}", | |
| } |
