Modèles des systèmes à évènements discrets et applis (EASI844_IAI)

Présentation

L'objectif de cet EC est d'introduire les notions de systèmes à évènements discrets, leurs diverses modélisations et l'intérêt de ces modèles (communication, précision, vérification, génération de systèmes exécutables, etc.).

Les modèles de comportement des SED sont présentés, depuis les systèmes de transition jusqu'aux modèles « de haut niveau ». Les problèmes de vérification de propriétés sont abordés.

Objectifs

Ce cours vise à rendre l'élève apte à :

Niveau

A l'issue de ce cours l'élève sera capable :

choisir un type de modèle de SED approprié à partir d'un système donné, et pour une question donnée relative à son fonctionnement attendu.

Maîtrise

de décrire les contraintes du modèle

  

de choisir un type de modèle correspondant à ces contraintes parmi ceux étudiés

extraire un modèle pertinent d'un système concernant une question donnée relative au fonctionnement attendu de ce système

Maîtrise

de choisir le niveau d'abstraction du modèle

  

de définir le modèle du système de manière exacte

  

d'utiliser efficacement pour définir le modèle, les outils logiciels adaptés

construire un système à partir de son modèle correct

Application

de réaliser un système logiciel/capteurs/actionneurs (de taille « moyenne ») conforme à un cahier des charges donné

  

de tester les propriétés du système réalisé méthodiquement pour s'assurer de sa fidélité au modèle défini

établir, pour un modèle de système donné et une question donnée relative à son fonctionnement attendu, si oui ou non cette propriété est satisfaite

Application

de réaliser la vérification de la propriété dans le formalisme adapté (preuve, test, simulation, ...)

  

d'utiliser les méthodes et outils logiciels (s'il y a lieu), adaptés à la vérification à réaliser

Pré-requis

  • Automatisation – EEATS 541
  • Conception et programmation orientée objet – IGI 641
  • Systèmes embarqués – IGI 741
  • Méthodes de développement logiciel et qualité – IGI 742

Plan du cours

Plan du cours

  1. SED et modélisation (4,5h)
  2. Systèmes de transition et automates (7,5h)
  3. Réseaux de Petri (9h)
  4. Modèles de haut niveau (UML, etc.) (12h)
  5. Vérification et validation des systèmes (4,5h)

Travaux pratiques

  • Automates et exécutions
  • Réseaux de Petri – modélisation et vérification
  • Modèles de haut niveau – du cahier des charges à la conception détaillée.
  • Applications de contrôle - vision et traitement d'image.

Volume horaire

  • CM : 9.0
  • TD : 19.5
  • TP : 12.0

Informations complémentaires

Bibliographie

  • Cassandras, C. & Lafortune, S., Introduction to discrete event systems, Springer-Verlag, 2008
  • E. Encrenaz-Tiphene, Méthodes formelles pour la vérification des systèmes embarqués, Techniques de l'ingénieur, 2013, réf. H8250, http://www.techniques-ingenieur.fr/base-documentaire/technologies-de-l-information-th9/systemes-embarques-42588210/methodes-formelles-pour-la-verification-des-systemes-embarques-h8250/
  • C. Girault, R. Valk (Eds.), Petri Nets for System Engineering - A Guide to Modelling, Verification, and Applications, Springer-Verlag, 2003

Diplômes intégrant ce cours

En bref

Langue d'enseignement
Français

Contact(s)

UFR, Écoles, Instituts