Contributions à la vérification et à la validation efficaces fondées sur des modèles

Aloïs Dreyfus 1, 2
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Résumé : Les travaux de cette thèse contribuent au développement de méthodes automatiques de vérification et de valida-tion de systèmes informatiques, à partir de modèles. Ils sont divisés en deux parties : vérification et générationde tests.Dans la partie vérification, pour le problème du model-checking régulier indécidable en général, deux nouvellestechniques d’approximation sont définies, dans le but de fournir des (semi-)algorithmes efficaces. Des sur-approximations de l’ensemble des états accessibles sont calculées, avec l’objectif d’assurer la terminaison del’exploration de l’espace d’états. Les états accessibles (ou des sur-approximations de cet ensemble d’états)sont représentés par des langages réguliers, ou automates d’états finis. La première technique consiste à sur-approximer l’ensemble des états atteignables en fusionnant des états des automates, en fonction de critèressyntaxiques simples, ou d’une combinaison de ces critères. La seconde technique d’approximation consisteaussi à fusionner des états des automates, mais à l’aide de transducteurs. De plus, pour cette seconde technique,nous développons une nouvelle approche pour raffiner les approximations, qui s’inspire du paradigme CEGAR(CounterExample-Guided Abstraction Refinement). Ces propositions ont été expérimentées sur des exemplesde protocoles d’exclusion mutuelle.Dans la partie génération de tests, une technique qui permet de combiner la génération aléatoire avec un critèrede couverture, à partir de modèles algébriques (des grammaires algébriques, des automates à pile) est définie.Générer les tests à partir de ces modèles algébriques (au lieu de le faire à partir de graphes) permet de réduirele degré d’abstraction du modèle et donc de générer moins de tests qui ne sont pas exécutables dans le systèmeréel. Ces propositions ont été expérimentées sur la grammaire de JSON (JAvaScript Object Notation), ainsi quesur des automates à pile correspondant à des appels de fonctions mutuellement récursives, à une requête XPath,et à l’algorithme Shunting-Yard.
Type de document :
Thèse
Systèmes et contrôle [cs.SY]. Université de Franche-Comté, 2014. Français. 〈NNT : 2014BESA2076〉
Liste complète des métadonnées

Littérature citée [89 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01090759
Contributeur : Abes Star <>
Soumis le : jeudi 19 octobre 2017 - 10:15:41
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : samedi 20 janvier 2018 - 14:17:15

Fichier

these_A_DREYFUS_Alois_2014.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : tel-01090759, version 2

Citation

Aloïs Dreyfus. Contributions à la vérification et à la validation efficaces fondées sur des modèles. Systèmes et contrôle [cs.SY]. Université de Franche-Comté, 2014. Français. 〈NNT : 2014BESA2076〉. 〈tel-01090759v2〉

Partager

Métriques

Consultations de la notice

113

Téléchargements de fichiers

43