Objectifs de l’enseignement
Les différentes méthodes formelles de spécification.
Connaissances préalables recommandées
Théorie des langages et génie logiciel 1, 2
Contenu de la matière :
- Introduction à certaines notations formelles pour décrire les exigences et les spécifications de systèmes logiciels
- Méthodes pour les systèmes séquentiels (tel que le langage Z ou la notation de Mills) et pour les systèmes concurrents et réactifs (tels que les machines d’états et les réseaux de Petri avec certaines extensions concernant les données)
- Utilisation des méthodes formelles pour l’analyse des propriétés et du fonctionnement des systèmes au niveau de la spécification, de la conception ou de l’implantation.
Mode d’évaluation : 60% examen et 40% travail personnel
Références
- R Abrial, the spécification language Z, Technical report, Oxford programming Research group, 1980.
- A. Bergstra, J. Heering et R Klint, Algebraic spécification, Addison-Wesley, Reading (Mass.),1989.
- Habries, Introduction à la spécification, Masson, paris 1993.
- Derrick and E. Boiten. Refinement in Z and Object-Z. Springer, 2001.
- Guttag and J. Horning. Larch : Languages and Tools for Formal Specification. Springer-Verlag, 1993.
H. HABRIAS, Introduction à la spécification, Masson, 1993
