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.
Période(s) du cours
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)
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é.
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