Application de techniques de preuve assistée pour la spécification, la vérification et le test / présenté par Davy Rouillard ; sous la dir. de Richard Castanet

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Logiciels -- Vérification

Méthodes formelles (informatique)

Théorie de la démonstration

Automates mathématiques, Théorie des

Castanet, Richard (1943-....) (Directeur de thèse / thesis advisor)

Université Bordeaux-I (1971-2013) (Organisme de soutenance / degree-grantor)

Relation : Application de techniques de preuve assistée pour la spécification, la vérification et le test / Davy Rouillard / Grenoble : Atelier national de reproduction des thèses , 2002

Résumé / Abstract : Les méthodes formelles ont pour objectif d'augmenter le niveau de confiance que l'on peut avoir en un système informatique, en proposant des techniques d'analyse dont les fondements sont mathématiques. Traditionnellement, ces méthodes sont classées en trois grandes familles : le model-checking, la preuve interactive et le test. Ce mémoire décrit le développement d'un environnement formel qui autorise à la fois une activité de vérification et dont l'objectif est permettre l'étude de systèmes complexes modélisés sous la forme d'automates. Cet environnement prend la forme d'un ensemble de théories Isabelle/HOL dont la racine est formée par la formalisation des systèmes de transitions et leur comportements. Plusieurs mécanismes de preuve sont présentés et il est mit en évidence l'importance du mécanisme de réécritures. Nous nous intéressons également à une nouvelle approche du test qui consiste à envisager la création d'un test comme la démonstration d'un énoncé.