Etude et réalisation d'un environnement de spécifications orienté vers la conception de programmes certifiés.
Auteur : Jean-philippe Cottin
Thèse de l'ENST
Département Informatique
Laboratoire d'accueil : ENST
Résumé :
Le but de cette thèse est de rechercher des outils de spécifications
adaptés aux programmes du domaine des télécommunications, à
l'extraction automatique de programmes prouvés exacts et à une
réalisation informatique des processus de spécification et
d'extraction automatique de programmes prouvés corrects. Ces outils
devront être capables d'exprimer des notions telles que le
parallélisme, la séquentialité, la dépendance causale, la consommation
de ressources, la communication, etc. La thèse proposera une
réalisation de ces outils.
Plusieurs outils utilisant des méthodes formelles telles que LDS,
Estelle, Lotos, SPIN, Z, ... peuvent effectuer une vérification sur l'
objet formalisé ou une génération de tests. Nous désirons augmenter
les bénéfices apportés par les techniques de description formelles en
utilisant un tout nouveau moyen de spécifier et de vérifier un
programme. C'est ainsi que nous avons travaillé sur une logique des
actions basée sur la logique linéaire: l'Omega logique.
Notre but est de créer des programmes certifiés à partir de
spécifications écrites en SDL et de les traduire dans notre logique.
Etude et réalisation d'un environnement de spécifications orienté vers la conception de programmes certifiés. 
