Aspects formels du génie logiciel

Cette UE approfondit l’UE "Logiciels sûrs" du M1 en abordant d’une part différents aspects de la vérification formelle, et d’autre part en complétant celle-ci par une étude de cas reposant sur des outils utilisés dans l’industrie du logiciel. 

L'enseignement se compose de deux parties.

1) La première concerne les modèles formels de la programmation, de la modélisation et de la spécification. Les styles de programmation aussi bien dans le cas séquentiel que concurrent sont abordés. L’étude des systèmes formels (munis de leur système de preuve) supports des différentes méthodes formelles de vérification et de validation complète l’étude des langages de programmation. Des exemples d’application des méthodes formelles illustrent chaque type de méthode introduite. Une expérimentation d'une méthode et d'un outil de modélisation et de preuves formelles est menée, par exemple au travers de la méthode B et de l’atelier B.

2) La seconde concerne les outils industriels de vérification formelle des logiciels. Les outils expérimentés seront par exemple la plateforme Why3 (extraction de programmes OCaml), l’outil Krakatoa de vérification de programmes Java, la plateforme Frama-C d’analyse de programmes C, etc.

-  Maîtriser les modèles formels de la programmation, de la modélisation et de la spécification.

-  Mettre en oeuvre des outils industriels de vérification formelle des logiciels.

UE Logiciels sûrs et Génie Logiciel 1 et 2 de la première année du master d’Informatique. Notions de logique.

Maîtriser le développement d’une vérification formelle d’un logiciel. Savoir s’orienter dans les différentes technologies disponibles. Comprendre les enjeux d’une vérification formelle et la pertinence de sa mise en oeuvre.