40 HEE, 21 HPE

3IF2270

Contact

Pascale Le Gall pascale.legall@centralesupelec.fr

Présentation générale

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 (par exemple l’algorithme “trickle” utilisé pour la propagation de la mise à jour des codes dans les réseaux de capteurs) : modélisation et analyse à l'aide des outils UPPAAL et DIVERSITY.

Moyens

Articles de recherche

Support des cours (diapositives)

Logiciels (UPPAAL, DIVERSITY) installés sur les machines personnelles des élèves

Contenu

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

Méthodes d'évaluation

Réalisation d'un projet (rapport, implémentation, analyse, soutenance orale)