ECUE X9S904 - TC4 Validation de systèmes embarqués critiques

UE Cours de spécialisation - 1 ECTS



 Structure & Enseignants
Type
Heures
Enseignants Associés
CM 12 (x1)
 Karen Godary-Dejean 12h


 Description
Enseignant Responsable Karen Godary-Dejean
THE 6
Description ECUE

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

Mots clés Systèmes embarqués critiques temporels
Modélisation par machine à états (automate, réseau)
Validation formelle, vérification (model checking)
Sûreté de fonctionnement
Modalités de contrôle
  • Contrôle continu en cours (devoirs, exposés)
  • Un examen écrit final
Contexte

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.

Contenu
  • 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
Ressources
  • Support de cours
  • Articles et thèse de doctorat
  • Webographie des outils utilisés
Prérequis
  • 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.

+ X9S704 - Systèmes à évènements discrets (SED)
+ X9S610 - Initiation aux microcontrôleurs
+ X9S713 - Conception VHDL
+ X9S905 - TC6 Technologie pour la santé : étude des neuroprothèses


 Connaissances
#
Libellé
N
A
M
E
0
Connaissance des contraintes applicatives des systèmes embarqués critiques. x
0
Connaissance des principes de V&V (Vérification et Validation) x
0
Introduction aux concepts de model checking x


 Compétences
#
Libellé
N
A
M
E
0
Savoir analyser un cahier des charges et en déduire les propriétés à vérifier x
0
Savoir modéliser ces propriétés (logique temporelle) x
0
Savoir modéliser un système en machine à états (réseaux de Petri) x
0
Savoir vérifier les propriétés sur un graphe d'état de ce système x


 Capacités
#
Libellé
Non
Oui
1
Rédiger x
2
Communiquer x
3
Travailler en équipe x
4
Animer et piloter un groupe, un projet x
5
Rigueur et organisation x
6
Sens pratique x
7
Sens critique x
8
Ouverture d'esprit x
9
Capacité d'analyse et de synthèse x
10
Capacité d'abstraction, logique x
11
Capacité d'initiative x
12
Créativité x


 Compétences RNCP
Type
#
Libellé
0
1
2
CTI
1
Aptitude à mobiliser les ressources d'un large champ de sciences fondamentales. x
CTI
2
Connaissance et compréhension d'un champ scientifique et technique de spécialité. x
CTI
3
Maîtrise des méthodes et des outils de l'ingénieur : identification et résolution de problèmes, même non familiers et non complètement définis, collecte et interprétation de données, utilisation des outils informatiques, analyse et conception de systèmes complexes, expérimentation. x
CTI
4
Capacité à s'intégrer dans une organisation, à l'animer et à la faire évoluer : engagement et leadership, management de projets, maîtrise d'ouvrage, communication avec des spécialistes comme avec des non-spécialistes. x
CTI
5
Prise en compte des enjeux industriels, économiques et professionnels : compétitivité et productivité, innovation, propriété intellectuelle et industrielle, respect des procédures qualité, sécurité. x
CTI
6
Aptitude à travailler en contexte international : maîtrise d'une ou plusieurs langues étrangères, sûreté, intelligence économique, ouverture culturelle, expérience internationale. x
CTI
7
Respect des valeurs sociétales : connaissance des relations sociales, environnement et développement durable, éthique. x
POL
1
Aptitude à participer aux actions de recherche et développement des entreprises, éventuellement en lien avec les acteurs de la recherche publique, et à apporter l’esprit d’innovation favorisant l’évolution technologique. x
MEA-SE
1
Spécifier et modéliser dans leur environnement des systèmes embarqués, sous contrainte de cahier des charges, en intégrant les évolutions de l'état de l'art. x
MEA-SE
2
Concevoir, simuler, prototyper et programmer des systèmes embarqués. x
MEA-SE
3
Réaliser, industrialiser, tester et maintenir des systèmes embarqués. x
MEA
4
Spécifier et concevoir des circuits et systèmes intégrés en vue de leur production industrielle. x
MEA
5
Modéliser un système physique, puis concevoir et mettre en œuvre une architecture de contrôle/commande adaptée. x