Les méthodes formelles consistent à effectuer la conception détaillée d’un logiciel sous la rigueur méthématique ; la conception détaillée ainsi produite permettant d'établir des preuves formelles, c’est-à-dire des démonstrations mathématiques qu’un composant logiciel donné est absolument conforme aux exigences dont le concepteur lui a donné la responsabilité. Les gains en fiabilité, en sûreté, mais aussi en efficacité du développement, sont importants. Un investissement en compétences, outils, ainsi qu’un changement de culture, sont nécessaires.

1. Objectifs
2. Public concerné
3. Programme
4. Bilan et suites envisageables
5. Tarifs

1. Objectifs

• Présenter :
  • un panorama des méthodes formelles ;
  • l’exemple de la Méthode B ;
  • quelques bases théoriques (les 3 niveaux Règle_d’Inférence-Séquent-Prédicat, les différences logiques, la correspondance de Curry-Howard, …) ;
  • l’inférence de type ;
  • l’architecture d’un AGL formel ;
  • la connexion naturelle entre l’approche formelle et l’Ingénierie Dirigée par les Modèles ;
  • la supériorité de la preuve sur le test (ou de la preuve formelle sur la preuve empirique).
• Effectuer, sur la base d’un cas concret présenté par l’auditoire, une spécification formelle, jusqu’aux preuves.

2. Public concerné

• DSI
• Directeurs de Projets
• Chefs de Projets
• Architectes
• Responsables de Développement
• Concepteurs / Modélisateurs

3. Programme

• Journée n°1
  • Matin
    • Différence entre syntaxe et sémantique.
    • Introduction à la sémantique des langages de programmation : présentation succinte des sémantiques opérationnelle, dénotationnelle, et axiomatique.
    • Que signifie “absence de bugs” ?
  • Après-midi
    • Présentation de la sémantique opérationnelle (Systèmes de transitions, etc.).
    • Présentation de la sémantique dénotationnelle (Lambda-calcul, Lambda-calcul typé, Théorie des types, etc.).
• Journée n°2
  • Matin
    • Présentation de la sémantique axiomatique (logiques (classique, intuitionniste, linéaire), prédicats, séquents, règles d’inférence, axiome, théorème, preuve, etc.).
    • Présentation de la correspondance de Curry-Howard.
    • Présentation de l’alliance naturelle qu’il y a entre l’Ingénierie Dirigée par les Modèles (voir notre séminaire sur le sujet), et les méthodes formelles.
    • Définition, avec l’auditoire, d’un cas pratique pour le travail de l’après-midi.
  • Arpès-midi
    • Étude de cas, sur la base du cas proposé dans la matinée : spécifications et raffinages dans les trois sémantiques.
    • Discussion générale.

4. Bilan et suites envisageables

• Étude d’opportunité, éventuellement poussée jusqu’au plan d’affaire, de l'évolution de votre solution d’Ingénierie Dirigée par les Modèles vers le formel, sous la forme d’une prestation de Conseil en Modélisation.

5. Tarifs

• 2.000 € H.T.