II.2409 Approches Formelles (2,5 crédits)
Pré-requis : -
Niveau : Avancé
Responsable du module : Olivier Hermant
Déroulement : 12 h de cours/TD, 16 h de cours/TP
Nbre d'heures : 28 h
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.
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
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.
Biblographie
|
