Module II.2409

II.2409 Approches Formelles (2,5 crédits)

Niveau : Avancé
Responsable : Olivier Hermant
Déroulement : 4 * 3h de cours/TD, 4 * 3h de cours/TP
Evaluation : Projets (40%), TP (10%) et Examen (50%)

Contexte

Les langages de programmation classiques ne permettent pas d’affirmer qu’un programme sera sans bug lors de son exécution. Même les techniques de tests les plus avancées peuvent laisser passer des défauts car la combinatoire entre les valeurs des variables et les chemins d’exécutions est trop importante. Les méthodes formelles apportent des solutions à ce problème pour une certaine classe d’applications. En particulier, les applications critiques comme les cœurs transactionnels de systèmes bancaires, les logiciels de pilotage de fusées, d’avions ou de métro nécessitent l’utilisation de ces méthodes où il est possible de prouver mathématiquement que le programme s’exécutera tel qu’attendu.

Objectifs

Compétences

Assurer la sûreté de fonctionnement et la fiabilité d’applications conçues pour des systèmes critiques. Le module initie à la modélisation des programmes selon des méthodes formelles ascendantes ou descendantes avec une granularité adaptée à la criticité du système et de son environnement. La spécification formelle conduit à un ensemble de contraintes formelles dont le traitement automatique est assuré par des outils reposant sur des modèles mathématiques et logiques avancés. Ce traitement permet de valider le programme ou de relever des points d’inadéquation entre les spécifications et le code.

Connaissances

Concepts

Inférence logique et correspondance preuves-programmes

Preuve de propriétés de programmes

Langages typés, lambda-calcul

Logique de Hoare

Interprétation abstraite

Model-checking

Programmation logique, déclarative, par contraintes

Test de logiciels

Certification de logiciels

Savoir-faire

Spécifier et prouver un programme à l’aide de langages formels

Extraction automatique de programme

Programmation en PROLOG

Approche pédagogique

Le module se déroule en 4 séances de cours/TD, qui serviront à introduire les concepts fondamentaux, suivies de 4 séances de cours/TP qui permettront de donner consistance à ces concepts. Un ou deux projets seront proposés pendant le module.