Introduction aux Méthodes Formelles
LE développement de programmes sûrs exempts d’erreurs s’avère, depuis quelques années, incontournable. Par exemple, les programmes embarqués dans des avions, fusées, dans les voitures ou même dans des appareils domestiques peuvent, s’ils ont des bogues, être la cause de perte de vies humaines, compromettre les objectifs d’un projet important ou conduire à des faillites financières d’entreprises. Tous ces problèmes ont poussé à mettre au point et proposer des approches qui garantissent la construction des programmes répondant rigoureusement aux spécifica- tions imposées et validées ensuite par des méthodes mathématiques. Les méthodes formelles de validation des programmes ont constituées une des approches la plus appropriée pour la validation des propriétés des programmes. L’idée, qui s’est révèlée particulièrement fructueuse, a été celle de considérer que l’activité de programmer ne diffère pas de celle de prouver formellement des propriétés. Construire un programme revient, alors, tout simplement à prouver la cohérence de sa spécification. La garantie de sûreté sera donc assurée par la preuve mathématique de la spécification de l’application à développer. L’etude du λ -calcul et de la théorie des types a permis de construire des systèmes et des assistants de preuve qui offrent la possibilité d’une part, de valider de façon rigoureuse des spécifications et des propriétés de programmes et d’autre part, permettre l’extraction automatique de programme à partir de la preuve de sa spécification. L’objectif de ce cours, prodigué aux étudiants de Master 2 informatique, est de les initier à ces techniques fort utiles pour ceux qui souhaitent approfondir leurs connaissances de ce domaine qui suscite de plus en plus d’interêts chez les chercheurs et aussi les industriels (voir [10]). Nous avons aussi estimé utile, après avoir introduit le λ -calcul et les différents systèmes de types, de présenter une introduction succincte de l’assistant de preuve Coq. Deux exemples illustrent aussi comment utiliser ce système pour les spécifications et l’extraction des programmes. Aucun prérequis n’est exigé pour aborder les notions abordées dans ce cours, excepté des connaissances élémentaires en logique. Il est accessible aux étudiants de licence informatique ou de mathématiques. Il peut aussi intéresser les enseignants curieux ou souhaitant s’initier aux assistants de preuve qui prennent,actuellement, une place très importante dans les domaines de l’informatique et aussi des mathématiques.
Autres livres de : M Mezghiche
Livres dans la même catégorie
Avis des lecteurs
Aucun avis pour le moment.