Conception de systèmes embarqués critiques de controle-commande

Les systèmes embarqués critiques de contrôle-commande se trouvent dans différents domaines industriels (usine 4.0, Avionique, Ferroviaire…) mais aussi dans notre vie quotidienne (domotique, automobile, médical…).

Ces systèmes, souvent critiques, sont soumis à des contraintes de robustesse, de sûreté de fonctionnement et de qualification. Ceci impose de faire appel à des méthodes de spécification qui, au-delà de l’optimisation du processus de conception, garantissent formellement le respect de l’ensemble des propriétés et plus particulièrement les propriétés de sûreté. Le développement de langages et outils certifiés permet de réduire considérablement les coûts de certification des projets en simplifiant la conception et en automatisant la vérification et la génération de code (qualifié/certifié par différentes normes).

L’objectif de cet électif est de former les étudiants aux méthodes de spécification de haut niveau et à la conception dirigée par les modèles en utilisant des méthodes/modèles formels adaptés aux systèmes critiques.

Les activités pédagogiques permettront de définir un modèle formel du comportement du système et de prendre en compte les exigences de sûreté. En effet, la traduction de ces exigences en termes de propriétés vérifiables permettra de faire la preuve du respect de ces dernières.

L’enseignement abordera la génération de code « certifié » et comment embarquer ce dernier sur une plateforme matérielle en prenant en compte les performances d’exécution (performances temporelles, dimensionnement…) Le dernier point concernera les phases d’intégration de vérification et de validation.