Automates finis pour la fiabilité logicielle et l'analyse d'accessibilité

• Main Author: Heam, Pierre-Cyrille
• Language: FRE
• Published: Université de Franche-Comté 2009
• Subjects: [INFO] Computer Science; [INFO:INFO_SE] Computer Science/Software Engineering; automates finis; vérification; test
• Online Access: http://tel.archives-ouvertes.fr/tel-00432301; http://tel.archives-ouvertes.fr/docs/00/43/23/01/PDF/HDRpch.pdf; http://tel.archives-ouvertes.fr/docs/00/43/23/01/ANNEX/remer.pdf

La fiabilité des logiciels est un facteur critique de notre société~: toute panne, tout bogue, tout dysfonctionnement, perturbe la bonne marche de nos activités avec parfois des conséquences humaines, financières ou morales importantes. Contrairement à d'autres domaines industriels plus anciens, la démarche qualité en informatique n'en est encore qu'à ses débuts. Il est couramment convenu comme normal qu'un ordinateur perde un fichier ou que l'installation d'un nouveau logiciel en rende un autre inutilisable. Cependant, dans des domaines précis (banque, systèmes embarqués, médecine, etc.), dits critiques, on ne peut se permettre d'avoir un système défaillant~: une phase importante du développement logiciel est celle de la validation durant laquelle le système est analysé afin de garantir qu'il respecte certaines exigences de fiabilité. Cette phase de validation fait appel à deux approches complémentaires, le test et la vérification. Les travaux présentés dans cette habilitation concernent majoritairement la verification par la technique dite de "model-checking". Une première partie montre des techniques originales pour la vérification de protocoles de sécurité. D'autres travaux, plus théoriques, portent sur l'accélération de relations de semi-commutation ainsi que sur la vérification de propriétés non fonctionnelles. Enfin, des résultats sur la génération aléatoire de structures complexes sont développés dans le contexte du test à partir de modèles et du test de performances.