Introduction aux techniques de modélisation et vérification formelle des systèmes embarqués, temporelles critiques.

• Contrôle continu en cours (devoirs, exposés)
• Un examen écrit final

Ce cours commence par une introduction générale des concepts de la sûreté de fonctionnement. Puis il présente le côté plus spécifique de la validation de système, avec les différentes méthodes existantes. En s'intéressant aux contextes applicatifs tels que le domaine médical, les transports (automobile, avionique), le spatial ou la robotique, ce cours montre les besoins de techniques de validation telle que le model checking. Cette méthode permet la vérification exhaustive d'en ensemble de propriétés sur l'ensemble des états atteignables d'un modèle du système. Ce cours s'intéresse également à la différence existant entre les résultats de validation et la réalité, en particulier de part l'abstraction de la cible matérielle et de la technologie d'implémentation. Tous les domaines applicatifs concernant les systèmes embarqués, temporelles et/ou critiques sont potentiellement concernés par cette problématique : le domaine médical, les transports (automobile, avionique), le spatial ou la robotique de manipulation médical, de service, militaire, de search&rescue, d'exploration d'environnement fragile, etc.. Les grands "donneurs d'ordres" des domaines industriels tels que l'avionique ou le spatial ce sont depuis plusieurs années déjà intéressés aux possibilités du model checking.

• Introduction générale de la sûreté de fonctionnement
• Zoom sur les techniques de validation de systèmes
• Zoom sur le model checking
• Les réseaux de Petri temporels - description théorique et exercices de modélisation
• Logiques temporelles pour le model checking
• Technique de base du model checking - théorie et outil
• Application à un cas concret dans le cadre de la conception d'implant médicaux pour la stimulation électro-fonctionnelle (SEF)
• Prise en compte des contraintes d'implémentation : problématique et solution de transformation de modèles

• Support de cours
• Articles et thèse de doctorat
• Webographie des outils utilisés

• Techniques de modélisation des SED
• Formalisme des réseaux de Petri temporels.

Une connaissance des cibles micro-controleur avec OS temps réel, ainsi que les FPGA, permettra de mieux comprendre la problématiques des contraintes d'implémentation. De plus, le cours "Technologie pour la santé : étude des neuroprothèses" proposé en parallèle dans ce semestre est un parfait complément à ce cours.