ECUE XSE1011 - Vérification formelle

UE Informatique industrielle S10 - 1.5 ECTS



 Structure & Enseignants
Type
Heures
Enseignants Associés
CM 12 (x1)
 Abdoulaye Gamatie 12h
TD 12 (x1)
 Abdoulaye Gamatie 12h


 Description
Enseignant Responsable Abdoulaye Gamatie
THE 10
Description ECUE

Introduction aux techniques de conception sûre des systèmes embarqués en utilisant les approches formelles, c’est-à-dire basées sur des modèles mathématiques, pour la description et la vérification des propriétés de tels systèmes.

Mots clés Conception sûre, Systèmes embarqués critiques
Programmation synchrone, Langage Signal
Modélisation par machines à états (automate, RdP)
Vérification formelle
Modalités de contrôle
  • Contrôle continu en TP
  • Un examen écrit final
Contexte

Les systèmes embarqués sont des dispositifs constitués de matériels et de logiciels soumis à des contraintes à la fois fonctionnelles (par exemple, la correction des fonctions réalisées) et non fonctionnelles (par exemple, des échéances temporelles à ne pas dépasser, des niveaux de qualité de service à respecter) pour réaliser des traitements, et agir sur leur environnement. Des exemples de domaines où l’on rencontre de tels systèmes sont les télécommunications, le nucléaire, l’avionique ou le médical. Ces systèmes sont souvent critiques, notamment en ce qui concerne les trois derniers domaines cités précédemment, à cause d’enjeux humains et économiques importants en cas de défaillance.

Contenu

Ce cours a pour but de sensibiliser les étudiants à la problématique de la conception sûre des systèmes embarqués critiques en introduisant les enjeux associés et deux approches importantes :

  • La programmation synchrone dédiée aux logiciels embarqués de contrôle/commande dans des domaines comme l’avionique, l’automobile ou le nucléaire. Elle se base sur des langages ayant une sémantique mathématique et accompagnés d’outils adéquats pour garantir la correction des propriétés à la fois fonctionnelles et non fonctionnelles des systèmes. Cette approche sera illustrée à l’aide du langage Signal et de son environnement Polychrony (dont la version industrielle est commercialisée par Dassault Systèmes) ;
  • L'approche de validation formelle par « model-checking », qui permet la vérification de propriétés fonctionnelles sur un modèle du système. Les différentes étapes (modélisation, expression des propriétés, graphe d'analyse et vérification) seront illustrées sur un exemple concret.
Ressources
  • Transparents de cours au format PDF
  • Sujets d’exercices avec corrigés
Prérequis
  • Programmation en langage C
  • Notions (très) élémentaires en mathématiques : ensembles, relations, systèmes d’équations
  • Modélisation en réseaux de Petri ou en automate (machines à états)
  • Problématique du contexte des systèmes critiques et temps réel
+ XSE502 - Algorithmique & langage C
+ XSE501 - Mathématiques pour l'ingénieur
+ XSE623 - Logique et VHDL 2
+ XSE720 - Systèmes à temps discret


 Connaissances
#
Libellé
N
A
M
E
0
Introduction au model checking x
1
Connaissance élémentaire de programmation en C x
2
Notions mathématiques de base sur les ensembles et les relations x
3
Notions de base sur la logique booléenne x
4
Notions élémentaires sur les systèmes d'équations x


 Compétences
#
Libellé
N
A
M
E
0
Savoir vérifier des propriétés sur un modèle x
1
Savoir générer du code C à partir d'un modèle formel x
2
Savoir décrire formellement des propriétés comportementales x
3
Etre sensibilisé à la programmation déclarative en langage synchrone Signal x
4
Etre sensibilisé aux exigences de conception de systèmes temps réel critiques x
5
Savoir appréhender des propriétés d'applications temps réel x
6
Savoir compiler et simuler du code généré automatiquement 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