Conception d’un système de commande sûr pour un ascenseur
Ref: 2SC5891
Description
Le but de cette étude est de concevoir un logiciel critique à embarquer dans un contrôleur pilotant un ascenseur. Cette étude implémente l’ensemble du cycle de vie du développement d’un logiciel critique en partant d’une spécification formelle jusqu’à la génération automatique du code C qui sera embarqué dans le contrôleur. La méthode formelle B sera l’outils support pour couvrir l’ensemble des étapes du développement formel, et les circuits CSP (CLEARSY Safety Platform) développés par ClearSy, seront utilisés pour implémenter le contrôleur de l’ascenseur.
Numéro de trimestre
ST5
Prérequis
- Cours: Modélisation et Vérification des systèmes critiques (le cours spécifique de la ST)
- Introduction à la modélisation avec la méthode B (fait pendant la 1e journée de l'enseignement d'intégration)
Syllabus
- - Introduction à la modélisation en utilisant la méthode B.
- - Introduction à l'utilisation de l'Atelier B
- - Introduction à l'utilisation de la Clearsy Safety platform
- - Modélisation d'un ascenseur.
- - Vérification des propriétés de sureté.
- - Génération d'un programme informatique embraqué dans des cartes électroniques à partir d'un modèle B.
Composition du cours
Projet sur une semaine (9 demi-journées)
Notation
- Les étudiants seront évalués à la suite d'une présentation de 15 à 20 minutes des résultats obtenus.
Ressources
- Utilisation de l'Atelier B, outils de développement avec la méthode formelle B (https://www.clearsy.com/outils/atelier-b/)
- Utilisation la Clearsy Safety Platform comportant des cartes éléectroniques et un logiciel de développement (https://www.clearsy.com/outils/clearsy-safety-platform/).
Résultats de l'apprentissage couverts par le cours
- Modéliser un système critique en utilisant la méthode formelle B.
- Modélisation des propriétés critiques d'un système.
- Vérification des propriétés de sureté en utilisant la preuve.
- Générer un programme informatique embarqué dans une carte électronique à partir d'un modèle formel prouvé.
Description des compétences acquises à la fin du cours
- C4 - Have a sense of value creation for his company and his customers
- C6 - Be operational, responsible, and innovative in the digital world
- C7 - Know how to convince
Support de cours, bibliographie
Atelier B :
https://www.clearsy.com/outils/atelier-b/
Clearsy-Safety-Platform
https://www.clearsy.com/outils/clearsy-safety-platform/
https://www.youtube.com/watch?v=QtmzVYNe0Fo