Utilisation du système coq pour spécifier un système de transition, modelisant un système physique ainsi que ses propriétés d’accessibilité et de vivacité.
Loading...
Date
2016
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Université Mouloud Mammeri
Abstract
Les méthodes formelles ont considérablement évolué, depuis les études de Floyd, Hoare et plusieurs autres pionniers, une tendance de cette évolution fut l’étude de méthodes formelles pour la spécification de systèmes physique de plus en plus complexe .Soit de la vérification de programmes vers la spécification de systèmes. Dans ce mémoire nous allons utiliser les méthodes formelles pour spécifier un système de transition, modélisant un système physique, ainsi que ses propriétés d’accessibilité et de vivacite, en utilisant l’assistant de preuve Coq. Pour pouvoir spécifier ce système dans l’assistant de preuve coq, il est impératif d’étudier le fonctionnement de base de ce dernier, dans un premier temps nous avons commencé par étudier la logique du lambda calcul, le calcul des constructions inductives qui est un formalisme intéressant pour servir de base à la programmation fonctionnelle ainsi qu’aux assistants de preuve.
Description
114 f. : ill. ; 30 cm. (+ CD-Rom)
Keywords
Lambda calcul, Calcul des constructions inductives, Système Coq, Système de transition, Spécification formelle
Citation
Conduite De Projets Informatiques