40 HEE, 21 HPE

3IF2260

Contact

Frédéric Boulanger frederic.boulanger@centralesupelec.fr

Cours en collaboration avec la société ANSYS

Intervenant : Xavier Fornari Xavier.Fornari@ansys.com

Présentation générale

Ce cours est une introduction à l'approche synchrone et à son environnement formel. Il comporte une part importante de pratique avec la réalisation d'un cas d'étude industriel avec la suite SCADE :

• Conception avancée basée sur les modèles
• Simulation et débogage
• Test et vérification
• Génération automatique de code certifié

Ce cours fait appel à des intervenants de la société ANSYS qui développe la suite SCADE.

Acquis d’apprentissage visés dans le cours

À l'issue de ce cours, les élèves seront capables :

• d'évaluer la pertinence de l'approche synchrone pour la conception d'un système
• de mettre en œuvre cette approche dans la suite SCADE
• de spécifier les propriétés attendues du système, et de les vérifier
• de générer le code applicatif à partir des modèles

Moyens

Les moyens mis en œuvre pour ce cours sont, après deux cours magistraux nécessaires à la présentation de l'approche, la pratique, tout d'abord sur un cas d'étude simple afin de prendre en main les outils, puis sur un cas complet.

Description des compétences acquises à l'issue du cours

C1.2 Utiliser et développer les modèles adaptés, choisir la bonne échelle de modélisation et les hypothèses simplificatrices pertinentes pour traiter le problème

• Identifier les propriétés critiques d'un système, formuler une solution qui permette de les assurer
• Choisir le modèle réactif synchrone lorsqu'il est pertinent
• Capturer les différents aspects du système dans le paradigme synchrone

C1.4 Spécifier, concevoir, réaliser et valider tout ou partie d'un système complexe

• Spécifier les propriétés attendues du système
• Construire un modèle de ce système
• Vérifier les propriétés sur le modèle et générer le code certifié du système.

C2.1 Avoir approfondi un domaine ou une discipline relatifs aux sciences fondamentales ou aux sciences de l'ingénieur

• Approfondissement des notions de temps, de simultanéité, de parallélisme.

Contenu

14 créneaux d'1h30 (21 HPE) : 2 cours magistraux (3h), 2 cours sur machine (3h), 5 bureaux d'étude consacrés au projet (15h) avec soutenance.

• CMs 1 & 2 : Introduction au paradigme synchrone
  • Contexte de développement de logiciel critique
  • Modèle synchrone : structure et gestion du temps
  • Le langage synchrone Lustre
    • opérateurs
    • causalité
• TD sur machine (créneaux 3 & 4) : Initiation à l'environnement de programmation synchrone SCADE à travers un cas d'étude concret:
  • Modèle synchrone de Scade, flots et opérateurs
  • Diagrammes de flots, automates...
  • Simulation
  • Vérification en Scade
    • observateurs des propriétés
    • utilisation du moteur de preuve
    • test et couverture
• TP/projet (créneaux 5 à 14) : Réalisation d'un cas d'étude complet
  • Couvrir toute les étapes du processus de développement depuis la spécification jusqu'à la génération certifiée du code en passant par la modélisation, simulation, preuve et test...
  • Le projet portera sur une application concrète proposée par le partenaire industriel.
  • Les élèves seront encadrés en présentiel pour la prise en main et l'usage de la suite SCADE.

Méthodes pédagogiques

Cours magistraux en faible quantité, pratique très encadrée (TD) pour l'initiation, pratique plus autonome (bureaux d'étude) pour l'application à un cas industriel.

Méthodes d'évaluation

L'évaluation portera sur la qualité des rendus et la soutenance du mini-projet.

Références

• https://www.ansys.com/blog/free-download-ansys-scade-student
• The Synchronous Languages 12 Years Later. Albert Benveniste, Paul Caspi, Stephen A. Edwards, Nicolas Halbwachs, Paul Le Guernic, and Robert de Simone. Proceedings of the IEEE 91(1):64-83, January 2003.
• Synchronous programming of reactive systems. Nicolas Halbwachs, Kluwer Academic. 1993.