Libellé du cours : | Ingenierie des Systèmes Intelligents |
---|---|
Département d'enseignement : | EEA / Electronique Electrotechnique Automatique |
Responsable d'enseignement : | Monsieur ABDOUL-KARIM TOGUYENI |
Langue d'enseignement : | Français |
Ects potentiels : | 4 |
Grille des résultats : | Grade de A+ à R |
Code et libellé (hp) : | G1G2_ED_EEA_ISI - Ing. des systèmes intelligents |
Equipe pédagogique
Enseignants : Monsieur ABDOUL-KARIM TOGUYENI / Monsieur BENOIT TROUILLET / Monsieur GUILHERME ESPINDOLA WINCK
Intervenants extérieurs (entreprise, recherche, enseignement secondaire) : divers enseignants vacataires
Résumé
L’ingénierie des systèmes consiste à développer des méthodologies permettant le développement intégré de systèmes industriels. Leur caractère intelligent consiste à concevoir ces systèmes de manière à leur permettre de réagir à des situations ne correspondant pas au mode normal de fonctionnement. L’objectif de cet enseignement est de donner aux étudiants les connaissances permettant d’utiliser des outils formels pour la conception et l’exploitation de systèmes intelligents. Les outils formels utilisés ici sont ceux permettant la modélisation et la vérification formelle de systèmes dont le comportement peut être abstrait par des évolutions discrètes. Cet enseignement comprendra les parties suivantes : Partie 1 : Introduction aux systèmes de transitions étiquetés et à la vérification formelle Dans cette partie on introduira les langages formels comme formalisme général pour la modélisation des systèmes de transitions étiquettes. Ensuite on fera une rapide introduction aux techniques de vérification formelle comme le theorem proving et le model-checking. Partie 2 : Modélisation et vérification par automates à états finis Dans cette partie, on introduira dans un premier temps les automates à états finis. On distinguera deux catégories d’automates à états finis : les automates déterministes et les automates non déterministes. On montrera que les automates déterministes sont des générateurs de langages réguliers. Ensuite, on présentera les opérateurs de base pour la manipulation des automates : produit cartésien, produit synchrone et produit totalement synchrone. Ensuite, on présentera les automates temporisés. On finira par une introduction de la synthèse de contrôleurs par automates à états finis. On utilisera des outils comme kronos et uppaal pour la contruction des modèles et la vérification. Partie 3 : Modélisation et vérification par Réseaux de Petri Dans cette partie, on introduira le formalisme des Réseaux de Petri (RdP). Les RdP ont été conçu par un mathématicien allemand Carl Adam Petri en 1962 comme un outil permettant de combler les lacunes des automates à états finis pour la modélisation de systèmes caractérisés par de nombreuses évolutions en parallèles et des synchronisations. La force des RdP est de permettre la vérification a priori des propriétés d’un système. Ils sont caractérisés comme les automates par un formalisme graphique mais ils peuvent être également manipulés par le biais de l’algèbre linéaire. Dans un premier temps, nous introduirons les RdP états/transitions définis par Carl Adam Petri. Mais depuis, de nombreuses abréviations et extensions ont été proposées. Une abréviation est un modèle plus concis que les RdP états/ transitions. Les extensions ont un pouvoir d’expression (.i.e une capacité de modélisation) supérieurs aux RdP états/transitions. Nous ferons notamment comme abréviation les RdP colorés. L’outil CPN tool de Jensen sera utilisé pour la modélisation d’études de cas. Il existe de très nombreuses extensions. Nous nous intéresserons notamment aux RdP temporisés qui sont souvent utilisés pour l’évaluation des performances des systèmes. Nous étudierons également les RdP temporels qui ont une expressivité plus importante que les RdP temporisés ou les automates temporels. Nous nous intéresserons également aux RdP stochastiques qui permettent de modéliser les comportements aléatoires. Nous les appliquerons notamment à l’évaluation de la sûreté de fonctionnement des systèmes industriels. Nous utiliserons un outil comme GreatSPN pour manipuler ce type de RdP. Cette partie se terminera par la présentation de méthodes de synthèse de contrôleurs à base de RdP, pour les systèmes industriels. Nous appliquerons notamment à la conception sûre de systèmes industriels de type systèmes de production manufacturière,ou aux systèmes de transports. Partie 4 : Introduction de l’algèbre des dioïdes pour l’évaluation des performances
Objectifs pédagogiques
À l’issue du cours, l’élève sera capable de : - Modéliser de manière formelle un système industriel dont le comportement peut être abstrait par des évolutions discrètes - Faire la vérification formelle des modèles de commande de systèmes industriels - Choisir un outil de modélisation discret en fonction de la problématique Contribution du cours au référentiel de compétences ; à l’issue du cours, l’étudiant aura progressé dans : -
Objectifs de développement durable
Modalités de contrôle de connaissance
Contrôle Continu
Commentaires: Contrôle continu (QCM, note de TD)
Examen final
Ressources en ligne
Serveur pédagogique Moodle
Pédagogie
Cours, TD et études de cas. Travaux de groupe
Séquencement / modalités d'apprentissage
Nombre d'heures en CM (Cours Magistraux) : | 24 |
---|---|
Nombre d'heures en TD (Travaux Dirigés) : | 16 |
Nombre d'heures en TP (Travaux Pratiques) : | 8 |
Nombre d'heures en Séminaire : | 0 |
Nombre d'heures en Demi-séminaire : | 0 |
Nombre d'heures élèves en TEA (Travail En Autonomie) : | 24 |
Nombre d'heures élèves en TNE (Travail Non Encadré) : | 0 |
Nombre d'heures en CB (Contrôle Bloqué) : | 0 |
Nombre d'heures élèves en PER (Travail PERsonnel) : | 0 |
Nombre d'heures en Heures Projets : | 0 |
Pré-requis
Connaissance de l’algèbre linéaire
Nombre maximum d'inscrits
64