SCADE et le synchrone pour les systèmes critiques
Ref: 3IF2260
Description
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.
Période(s) du cours
SM11
Prérequis
aucun
Syllabus
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é
- Cours 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
- Cours/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.
Composition du cours
Cours magistraux théoriques en faible quantité, cours avec pratique très encadrée pour l'initiation, pratique plus autonome pour l'application à un cas industriel.
Ressources
Ce cours combine cours magistraux indispensables à la présentation de l'approche et pratique avec SADE suite, d'abord sur un exemple simple, puis sur un cas d'étude plus complet.
Résultats de l'apprentissage couverts par 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
Support de cours, bibliographie
- 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.