Systèmes Hybrides

20 HEE, 9 HPE

Contact

Présentation générale

Ce cours explore les théories fondamentales et les outils pratiques pour la conception et la vérification de systèmes hybrides, en mettant l'accent sur l'interaction entre les aspects discrets et continus. L'utilisation d'une abstraction nous permet de vérifier automatiquement certaines propriétés cruciales. La vérification des systèmes embarqués critiques est un domaine d'application naturel de ces techniques. Une difficulté qui se pose est la nécessité de prendre en compte l'interaction du logiciel avec son environnement physique. La deuxième partie du cours est consacrée à la présentation des solutions actuelles pour l'analyse de tels systèmes.

Acquis d'apprentissage visés dans le cours

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

de concevoir un système informatique (aspect discret) ainsi que l'environnement (aspect continu) dans lequel il devra fonctionner;
de connaître et comprendre l'hétérogénéité et les interactions entre modèles;
de choisir le niveau d’abstraction approprié à l'implémentation d'un système hybride ;
de connaitre les solutions actuelles pour vérifier partiellement les systèmes hybrides;
de comprendre l'approche de l’ingénierie dirigée par les modèles et savoir utiliser les outils pour sa mise en œuvre.

Moyens

Les moyens mis en œuvre combinent cours magistraux pour introduire les concepts théoriques avec TDs pour les appréhender plus profondément. À la fin, il y a un projet encadré par des bureaux d'étude afin de permettre aux élèves de prendre en main rapidement l'outil.

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

C1.1 Étudier un problème dans sa globalité, la situation dans son ensemble. Identifier, formuler et analyser un problème dans ses dimensions scientifiques, économiques et humaines

Identifier les éléments-clés pour modéliser les systèmes hybrides, et formellement les capturer pour pouvoir les analyser.

C1.3 Résoudre le problème avec une pratique de l'approximation, de la simulation et de l'expérimentation

Voir l'avantage de sur-approximation pour les systèmes infinis ainsi celui de méthodes basant sur la simulation.

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 hybride en prenant en compte l'interaction entre les aspects discrets et continus.
Construire un modèle de ce système avec les spécifications.
Partiellement vérifier les propriétés sur le modèle.

Contenu

6 créneaux d'1h30 (9 HPE) : 2 cours + 2 TD, 1 bureaux d'étude (3h).

CM1-TD1 : Introduction et modélisation
- système continu, système discret, système hybride
- automates hybrides (syntax et sémantique)
- simulations, comportements zenos
CM2-TD2 : vérification de systèmes hybrides
- motivation et problèmes
- analyse symbolique de systèmes infinis
- vérification par abstraction
BE (créneaux 5 & 6)
- Environnement pour modéliser les système hybrides (ex: MATLAB & Simulink & Stateflow )
- Environnement pour vérifier les système hybrides (ex: Simulink Design Verifier)

Méthodes pédagogiques

Site web présentant le matériel du cours
Cours magistraux plus TDs pour introduire et présenter les concepts
Bureaux d'étude pour mettre en œuvre les concepts avec la réalisation concrète

Évaluation

L'évaluation se fera en contrôle continu sur la participation aux études de cas et la qualité des rendus.