Canal-U

Mon compte
Inria

Aspects temporels dans les systèmes embarqués critiques


Copier le code pour partager la vidéo :
<div style="position:relative;padding-bottom:56.25%;padding-top:10px;height:0;overflow:hidden;"><iframe src="https://www.canal-u.tv/video/inria/embed.1/aspects_temporels_dans_les_systemes_embarques_critiques.17248?width=100%&amp;height=100%" style="position:absolute;top:0;left:0;width:100%;height: 100%;" width="550" height="306" frameborder="0" allowfullscreen scrolling="no"></iframe></div> Si vous souhaitez partager une séquence, indiquez le début de celle-ci , et copiez le code : h m s
Auteur(s) :
SOREL Yves

Producteur Canal-U :
Inria
Contacter le contributeur
J’aime
Imprimer
partager facebook twitter Google +

Les chapitres


Aspects temporels dans les systèmes embarqués critiques

La plupart des systèmes embarqués que l'on trouve dans les applications critiques telles que les commandes de vol d'un avion ou le contrôle d'un moteur ou de l'ABS dans une automobile, font intervenir des aspects temporels. Ces derniers compliquent leur conception et leur réalisation lorsqu'il faut assurer qu'ils ont un comportement sûr (de fonctionnement). Afin d'atteindre ce but plusieurs phases, qui doivent être cohérentes, sont nécessaires.

La première phase consiste à effectuer une spécification fonctionnelle, souvent appelée modélisation, du système ou seuls les aspects fonctionnels et/ou causalité sont considérés. Cela permet de faire un premier niveau de vérification en termes d'ordre sur les événements qui entrent et sortent du systèmes relativement à un temps logique (sémantique des langages synchrones). Ce dernier fait l'hypothèse que l'on ne s'intéresse pas au temps physique nécessaire pour exécuter les fonctions. Cette première spécification doit s'accompagner d'une spécification non fonctionnelle dont l'objet est de donner, maintenant, des caractéristiques temporelles physiques aux différentes fonctions, pouvant ou non dépendre de l'architecture matérielle sur lesquelles elles s'exécuteront, et de décrire cette architecture. Dans le cas le plus général cette dernière est formée de plusieurs processeurs pouvant être de types différents, plusieurs circuits intégrés spécifiques réalisant chacun une fonction unique, tous ces composants échangeant des données à l'aide de moyens de communications pouvant, eux aussi, être de types différents.

La deuxième phase consiste à faire une analyse d'ordonnançabilité temps réel (temps physique) dont l'objet est double : montrer que la combinaison de la spécification fonctionnelle et non fonctionnelle peut conduit à une solution ordonnaçable sur l'architecture matérielle et synthétiser cet ordonnancement. Cette analyse d'ordonnançabilité doit bien sûr tenir compte des vérifications effectuées en temps logique.

La dernière phase consiste à transformer le résultat de la phase précédente en un code exécutable par les processeurs et les circuits intégrés spécifiques formant l'architecture matérielle. Cela conduit à générer automatiquement soit des mécanismes de synchronisation dans le cas d'architecture déclanchées par des événements, soit des appels à des fonctions dans le cas d'architecture déclanchées par le temps. Cette approche permet de concevoir et réaliser des systèmes embarqués critiques sûrs par construction.


  •  
    Label UNT : Unisciel
  •  
    Date de réalisation : 4 Juillet 2013
    Durée du programme : 40 min
    Classification Dewey : Traitement des données. Informatique, système embarqué
  •  
    Catégorie : Conférences
    Niveau : niveau Master (LMD), niveau Doctorat (LMD), Recherche
    Disciplines : Informatique, Informatique
    Collections : La demi-heure de science : pourquoi mène t-on des recherches dans ce domaine là ? Inria Paris - Rocquencourt
    ficheLom : Voir la fiche LOM
  •  
    Auteur(s) : SOREL Yves
    Editeur : INRIA (Institut national de recherche en informatique et automatique)
  •  
    Langue : FRA
    Mots-clés : système embarqué
    Conditions d’utilisation / Copyright : © Inria Paris - Rocquencourt
 

commentaires


Ajouter un commentaire Lire les commentaires
*Les champs suivis d’un astérisque sont obligatoires.
Aucun commentaire sur cette vidéo pour le moment (les commentaires font l’objet d’une modération)
 

Dans la même collection

 Explorations Mathématiques de l'activité du cerveau
 Logic-based static analysis for the verification of programs with dynamically allocated data structures
 Resolving Entities in the Web of Data
 Wireless In the Woods: Monitoring the Snow Melt Process in the Sierra Nevada
 Phénomènes Aléatoires dans les Réseaux
 Modèles mémoire pour les multiprocesseurs à mémoire partagée
 Gestion de données personnelles respectueuse de la vie privée
 Génération de maillages pour la simulation numérique
 Transport Optimal et théorème de Brenier
 Réseau optiques, algorithmes et probabilités
 Réduction de modèles de voies de signalisation intracellulaire
 Apprentissage automatique et Big Data
 Quelques questions biomathématiques soulevées par les axes neuro-endocriniens
 Codes correcteurs quantiques
 Quelques modèles solubles pour le trafic routier
 Interopérabilité de protocoles pour des systèmes mobiles émergents dans l’Internet du futur
 Preuve automatique de la sûreté de logiciels critiques
 Cryptanalyse : le fondement de la sécurité
 Transitions de phase : entre physique, mathématiques et informatique
 OCamlPro : promouvoir dans l’industrie un langage de programmation issu de la recherche
 Mesure de la qualité d'expérience Internet depuis le réseau domestique
 Langages de programmation et concurrence, une relation toujours épineuse
 Test et vérification automatique pour systèmes musicaux interactifs
 Utilisation d’algorithmes de calcul scientifique en topologie et vice-versa
 Futurs véhicules terrestres : autonomie ou automatisation ?
FMSH
 
Facebook Twitter Google+
Mon Compte