Génération efficace de grands espaces d'états

Garantir la fiabilité des systèmes informatiques exige des moyens de vérification rigoureux. Le model checking est une technique de vérification dont l intérêt majeur est l automatisation, et donc la facilité d utilisation pour les ingénieurs. La récente attribution du prix Turing aux créateurs de cette technique atteste de sa viabilité.Le model checking explore exhaustivement les modèles analysés. Cela amène un problème majeur : l explosion combinatoire liée aux espaces d'états des grands systèmes. Depuis plus de vingt ans, de nombreuses solutions ont été proposées pour repousser cette limite de taille afin d être capable de traiter des espace d états toujours plus grands dont les tailles peuvent atteindre très rapidement les 10^400 éléments.Les travaux présentés ici proposent deux types de solutions pour traiter plus efficacement de plus grands espaces d états. La première s'appuie sur les ressources de calcul parallèle des machines multi-processeurs,omniprésentes aujourd hui, et des grappes de calcul. La deuxième propose de traiter plus efficacement les diagrammes de décision en automatisant la technique dite de saturation, dont l efficacité empiriquement montrée est très difficile à atteindre manuellement.PARIS-BIUSJ-Mathématiques rech (751052111) / SudocSudocFranceF