Module DR : Spécification par modèles et développement rigoureux

Module DR : Spécification par modèles et développement rigoureux

Equipe pédagogique :

Didier Bert, Marie-Laure Potet, Yann Rouzaud

Volume :

24h.

Spécialité :

S&L

Ce module propose une présentation des méthodes formelles permettant une modélisation des données et une spécification axiomatique des programmes. Il est une introduction aux principales méthodes de spécification utilisées dans les milieux académiques et industriels. Il donne surtout la possibilité d'approfondir une technique particulière qui assure le développement correct depuis la spécification de haut niveau jusqu'au code exécutable. Ce module permet d'acquérir une compétence d'expert dans le domaine et de poursuivre des recherches en thèse sur le sujet. Des contacts sont possibles avec les groupes de recherche et les industriels qui utilisent cette méthode avec succès.

• Introduction aux méthodes VDM, Z et B. Principes généraux de la spécification par modèles.
• Etude de la méthode B. Notions de machines abstraites, état, invariant, substitutions généralisées.
• Théorie des substitutions généralisées. Préservation de l'invariant, obligations de preuve. Terminaison, faisabilité.
• Développement par raffinement. Correction d'un raffinement.
• Raffinement et implémentation, modularité, liens entre modules.
• Approfondissement de la notion de raffinement.
• Systèmes abstraits. Etude système d'un projet.

Toutes les étapes sont illustrées d'exemples. Possibilité d'utilisation de l'atelier B pour des expérimentations.

Module DR : Spécification par modèles et développement rigoureux