NFP209 : Construction rigoureuse des logiciels(1) (6 ECTS)

Pré-requis

Public :
Informaticiens désireux d'aquérir une formation dans le domaine des Logiciels Surs. Etudiants visant le diplôme d'ingénieur Cnam option IQL ou le Master STIC MOCS parcours Logiciels Sûrs.
Prerequis :
Bonne connaissance d'un langage de programmation. Il est conseillé d'avoir suivi ou de suivre en parallèle la valeur : Spécification et Modélisation Informatiques (SMI) (code NFP108).

Objectifs

Dans de nombreuses applications comme les télécommunications, les transports terrestre et aérien, le nucléaire, les banques, les soins médicaux etc, un logiciel défectueux peut conduire à des défaillances aux conséquences irréversibles, voire dramatiques.
En dehors de ces domaines critiques, l'essor d'internet, la généralisation de l'utilisation d'un langage comme JAVA permettant la mobilité du code, accroit et généralise le besoin de sécurité et par là même la nécessité de la vérification. D'où la profusion actuelle de projets et d'outils tant industriels qu'universitaires autour de la vérification de code ou de machines virtuelles JAVA.
De nombreuses entreprises travaillant sur ces sujets nous ont fait part de leurs difficultés à recruter des ingénieurs ayant une formation adaptée. C'est pour répondre aux besoins exprimés par ces entreprises, que nous avons mis en place, en collaboration avec elles, un enseignement dans ce domaine.
Cette valeur fait partie de cette formation car elle fournit les techniques de description et d'analyse utilisées dans les méthodes visant à accroitre la robustesse, la sureté et la performance des langages et des logiciels.
Cette valeur constitue la première partie d'une valeur C du diplôme d'ingénieur Cnam, elle consiste en un socle théorique sur la définition mathématique de la notion de programme (sémantique) et en un panorama des techniques et outil de validation de logiciel qui se prolonge dans l'UE NFP210.
Cette valeur fait aussi partie intégrante du Mastère Sciences et Technologies de l'information et de la communication, option Informatique, mention Optimisation, Conception d Systèmes et fournit ainsi les bases nécessaires pour la seconde année du Master, parcours systèmes embarqué sûrs (SEMS).

Projets

Un examen.

Contenu

• Socle théorique abordé: Sémantique des langages de programmation, logique de hoare.
• Techniques et outils abordés
• Verification de ByteCode Java, Verification d'assertion à la Hoare (Frama-C).
• Conception par raffinement et méthode B.
• Suite dans l'UE NFP210

Compétences visées

Maitrise de la signification et du comportement des langages.
Capacité d'analyse et de raisonnement sur ces objets.
Culture de base sur les principales techniques et outils employés industriellement pour la validation de logiciels.

Cette unité d'enseignement n'est dispensée dans aucun centre pour le moment.
N'hésitez pas à revenir consulter cette page régulièrement.