Descriptif

L'interaction de composantes informatiques, qui calculent et communiquent, avec leur environnement régi par des lois physiques, comme pour un avion ou un système médical implanté, est au centre du domaine émergent des systèmes cyber-physiques. Les systèmes embarqués en sont naturellement une brique de base. Mais alors que dans les systèmes embarqués traditionnels se concentrent essentiellement sur les aspects informatiques, ce cours propose de s'attacher plus particulièrement à l'interface entre le monde discret informatique et le monde physique continu. Maitriser la modélisation, l'analyse et le contrôle du comportement de tels systèmes est crucial pour permettre dans le futur d'améliorer l'efficacité, les fonctionnalités, et d'assurer la fiabilité de ces systèmes, toujours plus complexes et souvent critiques en terme de sécurité ou de coût.

Le cours s'attachera à trouver un équilibre entre modélisation et vérification, et entre fondations théoriques et les aspects pratiques. Il introduira notamment aux principes et à l'utilisation de quelques outils représentatifs de l'état de l'art, et s'intéressera à des cas d'étude réalistes (tels qu'un modèle temporel de pacemaker modélisé et vérifié avec l'outil Uppaal).

Le cours est central aux thématiques de la filière Conception des Systèmes Informatiques, mais il est également naturel dans le parcours Electrical Engineering ou dans la filière Algorithmes et Fondements des Langages de Programmation. Des sujets de projets 3A en lien avec des thématiques peuvent être proposés. 

Contenu:

1. Introduction aux systèmes cyber-physiques, modèles synchrones
2. Langages synchrones: spécification et éléments de vérification
3. Modélisation par automates temporisés
4. Logique temporelle et verification par model-checking 
5. Modélisation et simulation de systèmes hybrides
6. Analyse d'atteignabilité de systèmes différentiels et hybrides
7. Modélisation (fin), stabilité et contrôle de systèmes hybrides
8. Analyse logique des systèmes hybrides

Le cours est illustré par des exercices applicatifs (en cours), et par les séances de travaux pratiques utilisant différents outils de modélisation et vérification. Les trois ou quatre dernières séances sont dédiées à un projet, dans lequel l'accent pourra être mis, au choix des étudiants, sur la modélisation complète, et la vérification à un degré plus ou moins poussé, d'un système cyber-physique, ou sur le développement d'une méthode de vérification. 

Le cours sera validé pour une petite moitié sur les TPs, et la grosse moitié restante sur le projet et l'oral associé.

Langue d'enseignement :

Les documents sont en anglais, les cours sont donnés en français par défaut, en anglais sur demande