Jean-Philippe COTTIN

Directeur de thèse : Patrick BELLOT
Groupe : Génie Logiciel, Projet Logiques, Langages et Spécifications
Laboratoire d'accueil : Département Informatique, TELECOM Paris
Date de soutenance prévue : décembre 1997
English version
Etude et réalisation d'un environnement de spécifications orienté vers la conception de programmes certifiés.
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.
Publications

    1996

  1. (Cottin 96a) J-P. COTTIN, De l'usage des méthodes formelles pour la spécification des protocoles de télécommunication., TELECOM Paris, Computer Science Department, internal report n. 96D002, (148 pages), Paris (France), January 1996. ( Résumé ) ( PostScript 1,1 Meg )
  2. (Bellot 96b) P. BELLOT, J-P. COTTIN, A. DEMAILLE, J. LENEUTRE, E. ZARPAS, "Démonstration automatique dans une logique des actions et de la causalité" dans JSJ'96 Premières Journées du Séminaire Junior du LIPN "Intelligence Artificielle et Applications"
  3. (Bellot 96c) P. BELLOT, J-P. COTTIN, J. LENEUTRE, B. ROBINET, E. ZARPAS, "Prolegomena of a Logic of Causality and Dynamicity", to appear in STUDIA LOGICA, 1996.
  4. (Bellot 96d) P. BELLOT, J-P. COTTIN, A. DEMAILLE, J. LENEUTRE, E. ZARPAS, "Automated deduction for protocols design" in proceedings of Third Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice.
  5. (Bellot 96e) P. BELLOT, J-P. COTTIN, A. DEMAILLE, J. LENEUTRE, E. ZARPAS, "Using a logic of actions to design protocols" in proceedings of the 5th open workshop on High speed Network, Télécom-Paris- Universität Stuttgart, March 1996.
  6. (Bellot 96g) P. BELLOT, J-P. COTTIN, A. DEMAILLE, J. LENEUTRE, E. ZARPAS, "A Logic of Actions for Imperative Program Synthesis" in proceedings of Logic Colloquium'96, LC'96, J.M. Larrazabal ed., San Sebastian (Espagne), juillet 1996.
  7. (Bellot 96h) P. BELLOT, J-P. COTTIN, A. DEMAILLE, J. LENEUTRE, E. ZARPAS, "Création d'un environnement de génération de programmes utilisant une logique des actions" in Journées ADER, GDR Programmation, Paris (France), mai 1996.
  8. (Bellot 96f) P. BELLOT, J-P. COTTIN, A. DEMAILLE, J. LENEUTRE, E. ZARPAS, "Towards Bug Free Software Engineering for Telecommunication", in proceeding of The Eighth International Conference (Joint Europe-USA Conference) on ARTIFICIAL INTELLIGENCE APPLICATIONS (EXPERSYS'96) , PARIS-MARNE LA VALLEE, France (21 - 22 October 1996)
  9. (Cottin 96b) J-P. COTTIN, A. DEMAILLE, J. LENEUTRE, E. ZARPAS, "Création d'un environnement de programmation utilisant une logique des actions", dans JDIR'96, Paris, Septembre 1996.
  10. (Bellot 96a) P. BELLOT, J-P. COTTIN, A. DEMAILLE, J. LENEUTRE, E. ZARPAS, "Logique et Synthèse de Programmes Impératifs" dans Journées du GDR Programmation, C. Paulin-Mohring ed., Orléans (France), novembre 1996.

    1995

  11. (Bellot 95e) P. BELLOT, J-P. COTTIN, J. LENEUTRE, E. ZARPAS, "Programmation par preuves avec une logique des actions", dans Journées du GDR Programmation, C. Paulin-Mohring ed., Grenoble (France), novembre 1995.     
  12. (Bellot 95c) P. BELLOT, J.P. COTTIN, J.F. MONIN,  "Développement et de validation de logiciel. Méthodes formelles", dans Techniques de l'Ingénieur - Traité Informatique, H 2 550, Dec. 1995.
  13. (Bellot 95d) P. BELLOT, J-P. COTTIN, J. LENEUTRE, E. ZARPAS,   "Méthodes formelles et protocoles, proposition pour une logique des actions et de la causalité", dans Actes des 8èmes Journées Internationales sur Le Génie Logiciel et ses Applications, EC2 ed., pp. 267-280 Paris-La Défense (France), novembre 1995.
  14. (Bellot 95h) P. BELLOT, J-P. COTTIN, A. DEMAILLE, J. LENEUTRE, E. ZARPAS, "Calcul et programmation dans une logique des actions et de la causalité", dans Séminaire ENS/ENST Modèles, Langages et Télécommunications, B. Robinet ed., Paris, septembre 1995.

    1994

  15. (Cottin 94a) J-P. COTTIN, Démonstration automatique de théorèmes en B-Logique propositionnelle, TELECOM Paris, Computer Science Department, internal report n. 94D021, Paris (France), september 1994.
Email : cottin@inf.enst.fr

index couleur dept enst mail
Page maintenue par Jean-Philippe COTTIN (cottin@inf.enst.fr) et Patrick BELLOT (bellot@inf.enst.fr)