Spécifications, vérification et test (SVT)

Responsable : Philippe Dhaussy
Équipe pédagogique : Fabien Dagnat, Philippe Dhaussy, François Monin, Valérie-Anne Nicolas

Description
Les méthodes formelles deviennent un domaine important du génie logiciel, en particulier dans le cadre des logiciels critiques, temps réel, distribués et de la certification. Elles définissent des techniques de spécification et d’analyse des systèmes qui se positionnent de manière complémentaire à la simulation et au test. Le module SVT sera dédié à la problématique de la spécification et la vérification de modèles, et présentera des techniques de vérification de propriétés liées à la distribution, au parallélisme et au temps réel. Cette U.E. est une introduction à ces méthodes et à leur application pour la spécification, le développement et la preuve de logiciels. Elle aborde diverses méthodes, formalismes et outils permettant de construire des spécifications formelles de programmes ou de systèmes, et de conduire des vérifications de propriétés sur ces spécifications. Ces techniques impliquent une modélisation mathématique des systèmes à analyser, avec une sémantique formelle précise.

Durant ce cours, deux démarches essentielles sont mises en évidence. D’une part, la première concerne les méthodes interactives qui mettent en œuvre des preuves par raisonnement mécanisé. Notamment celle-ci est introduite par le biais d’une présentation de l’outil PVS, qui permet de développer des logiciels prouvés, de la spécification au code. D’autre part, la seconde démarche est supportée par des méthodes algorithmiques qui se basent sur l’exploitation de modèles représentant le système  (méthodes d’abstraction, de vérification exhaustive).

Le module est complété par une introduction à la génération automatique de séquences test.

Structure générale et contenu

• Introduction à la modélisation formelle
• Enjeux et problématique des méthodes formelles dans les cycles de développement logiciel
• Introduction à la modélisation formelle et aux formalismes de spécifications : syntaxe, sémantique, systèmes de transition, confluence, systèmes de type, inférence, correction
• Un formalisme pour la spécification de la concurrence : CCS
• Une extension pour la spécification de la mobilité : le pi-calcul
• Les langages réactifs asynchrones : SDL, UPPAAL, IF
• Logiques temporelles et temporisées
• Techniques de vérification par exploration de l’espace d’états (model checking), exemple d’utilisation du vérificateur UPPAAL
• La preuve de théorème et les assistants de preuves
• Test formel et la génération automatique de séquences de test
  

Références bibliographiques

• Alur R., Dill D., A Theory of Timed Automata, Theoretical computer Science, 126(2):183-235, 1994
• Pierce B.C., Foundational Calculi for Programming Languages, The Computer Science and Engineering Handbook, CRC Press, ed. Allen B.Tucker, 1997

Modalités d'évaluation : contrôle continu
La note finale est calculée de la façon suivante :

• un travail personnel (seul ou en binôme) sur un sujet choisi dans une liste de sujets proposés : 60%
• un quizz (2h) : 40%