Formation indisponible à l'heure actuelle

Construction rigoureuse des logiciels(1)

Formation

À Montpellier ()

Prix sur demande

Appeler le centre

Avez-vous besoin d'un coach de formation?

Il vous aidera à comparer différents cours et à trouver la solution la plus abordable.

Description

  • Typologie

    Formation

Missions, moyens et organisation
Le Cnam est placé sous la présidence de Jean-Paul Herteman, P-DG du groupe Safran, et dirigé par Olivier Faron.
Il remplit trois missions principales:
la formation professionnelle supérieure tout au long de la vie,
la recherche technologique et l'innovation,
la diffusion de la culture scientifique et technique.
Le Cnam offre des formations développées en étroite collaboration avec les entreprises et les organisations professionnelles afin de répondre au mieux à leurs besoins et à ceux de leurs salariés. Cette UE apparaît dans les diplômes et certificats suivants : Entrée
CYC14p-1 Ingénieur diplômé de l'école d'ingénieurs du Cnam Spécialité informatique, parcours Réseaux, systèmes et multimédia (IRSM)
Centres d'enseignement Entrée
CYC45p-1 Ingénieur diplômé de l'école d'ingénieurs du Cnam Spécialité informatique, parcours Architecture et ingénierie des systèmes et des logiciels (AISL)
Centres d'enseignement Entrée
MR069p-1 Master Sciences, technologies, santé mention informatique spécialité systèmes embarqués mobiles et sûrs (voie recherche et professionnelle)
Centres d'enseignement Entrée

Centres d'enseignement Public et conditions d'accès Public :
Informaticiens désireux d'acquérir une formation dans le domaine des Logiciels Sûrs. Étudiants visant le diplôme d'ingénieur Cnam spécialité Informatique pour les parcours IRSM et AISL.
Prérequis :
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 NFP 108).

Questions / Réponses

Ajoutez votre question

Nos conseillers et autres utilisateurs pourront vous répondre

Saisissez vos coordonnées pour recevoir une réponse

Nous ne publierons que votre nom et votre question

Les Avis

Les matières

  • Correction
  • Ingénieur du son
  • Algèbre

Le programme

Contenu Cette UE permet d'aborder plusieurs méthodes de vérification de logiciels et d'utiliser leurs outils correspondants. Elle comporte 4 parties :
  • Correction d'un programme impératif: Dans cette partie du cours, nous étudierons une méthode classique (la logique de Floyd-Hoare) permettant de prouver la correction d'un programme impératif par rapport à une spécification donnée. Nous présenterons tout d'abord brièvement les fondements théoriques de cette méthode, puis nous passerons à la pratique avec la plateforme Spark Ada. Cette plateforme, qui est utilisée dans l'industrie depuis de nombreuses années, permet de garantir la correction de systèmes critiques développés en Ada. Nous en profiterons pour rappeler les principes du paradigme "design-by-contract" adopté par le standard 2012 du langage.
  • Utilisation de Tests pour la validation de logiciels: Dans cette partie du cours, nous étudierons le développement de logiciels piloté par les tests en évaluant le coût des tests et le modèle de qualité FURPSE. Dans un deuxième temps nous étudierons les Tests dirigés par les modèles en détaillant l'utilisation des modèles dynamiques d'UML pour spécifier les tests.
  • Développement de programmes par la méthode B: de la spécification formelle à la génération automatique de code. Dans cette partie du cours, nous étudierons à l'aide d'études de cas la méthode B pour spécifier formellement des systèmes. Nous vérifierons leur correction à l'aide du prouveur de l'Atelier B et enfin en utilisant des techniques de raffinement nous obtiendrons un code correct par construction.
  • Conception par utilisation de méthodes formelles: algèbre de processus : Dans cette partie du cours, nous étudierons à l'aide d'études de cas l'utilisation d'une algèbre de processus pour spécifier formellement et vérifier des systèmes communicants. Nous utiliserons le langage LOTOS et la plateforme CADP.  
Techniques et outils abordés dans les 4 parties de l'UE :
  • Preuves de correction d'un programme impératif à l'aide de la logique de Floyd-Hoare. Utilisation de la plateforme Spark Ada.
  • Développement de logiciels piloté par les tests et étude du modèle de qualité FURPSE. Étude des tests dirigés par les modèles à l'aide des modèles dynamiques d'UML.
  • Développement de programmes corrects par construction à l'aide de la méthode B. Utilisation de l'Atelier B.
Spécification et vérification formelles de systèmes communicants à l'aide d'une algèbre de processus. Utilisation du langage LOTOS et de la plateforme CADP.
Modalités de l'évaluation Examen final.
Bibliographie
  • Jacques Printz, Jean-Francois Pradat-Peyre : Pratique des tests logiciels, Dunod, 2014.
  • Robert V. Binder, Bruno Legeard, and Anne Kramer : Model-based Testing: Where Does It Stand ?. CACM, Communications of the ACM, 58(2), 2015
  • J. R. Abrial : The B-Book: Assigning Programs to Meanings, Cambridge University Press, 2005.
  • : http:///fr/
  • : http://cadp.inria.fr/

Appeler le centre

Avez-vous besoin d'un coach de formation?

Il vous aidera à comparer différents cours et à trouver la solution la plus abordable.

Construction rigoureuse des logiciels(1)

Prix sur demande