Systèmes temps-réel
Ref: 3IF2270
Description
Ce cours s'intéresse à la modélisation, spécification, validation et vérification des Systèmes Temps-Réels (STR). Il s’agit essentiellement des systèmes réactifs assujettis à des contraintes temps-réelles parfois critiques (systèmes embarqués, protocoles, services web, systèmes cyber-physiques,…). Les contraintes temps-réelles sont particulièrement difficiles à énoncer et à garantir lorsque les systèmes sont concurrents ou distribués, car ces systèmes sont fortement non-déterministes, à cause des entrelacements des événements, de l'asynchronisme des communications, et des défauts de qualité de services (pertes de messages, latence du réseau).
Organisation
1. Présentation des Systèmes Temps-Réels : temps-réel dur/mou, contraintes temporelles, modélisation et simulation (e.g. DEVS Discrete Event System Specifications)
2. Automates temporisés à temps continu (Alur et Dill 1991) sont un formalisme de modélisation fondés sur l’utilisation d’horloges, de variables à valeurs réelles positives ou nulles, en charge de modéliser l’écoulement du temps. Ces horloges peuvent être remises à zéro et conditionnées pour le franchissement des transitions. L’outil UPPAAL (http://www.uppaal.org/) permet d’analyser les propriétés temporelles via des techniques de model-checking.
3. Systèmes de transitions symboliques à entrées sorties temporisés (TIOSTS) constituent un formalisme de modélisation des systèmes réactifs. Ils mettent en jeu des horloges pour modéliser le temps et des variables d'état pour modéliser les données échangées entre les systèmes. Ces systèmes sont étudiés au travers des techniques d’exécution symbolique, utiles à la fois pour valider la conception par animation de specifications et verifier les implementations par le biais de techniques de test de conformité. L’outil DIVERSITY (https://projects.eclipse.org/projects/modeling.efm) est une plate-forme d’exécution symbolique permettant de modéliser et analyser les TIOSTS.
4. Etude de cas : modélisation et analyse d'un système réel à l'aide des outils UPPAAL et DIVERSITY.
Numéro de trimestre
SM11
Prérequis
aucun
Syllabus
Le cours sera organisé selon le schéma suivant :
- des cours magistraux
- des TPs de prise en main des logiciels (UPPAAL, DIVERSITY) sur des exemples pédagogiques
- des séances dédiées à la réalisation d'un projet personnel
Notation
Réalisation d'un projet (rapport, implémentation, analyse, soutenance orale)
Ressources
Articles de recherche
Support des cours (diapositives)
Logiciels (UPPAAL, DIVERSITY) installés sur les machines personnelles des élèves
Support de cours, bibliographie
Diapositives - Articles de recherche