tous les documents
  • tous les documents
  • Images
  • Films
  • Rushes
  • Publications
  • Audio
Recherche avancée
Ensemble de recherche :
tous les documents
  • tous les documents
  • Images
  • Films
  • Rushes
  • Publications
  • Audio
Recherche par couleur
Ensemble de recherche :
tous les documents
  • tous les documents
  • Images
  • Films
  • Rushes
  • Publications
  • Audio
Code HTML Copiez-collez le code ci-dessous pour l'intégrer dans une page Web.
Titre :
RII - Astrée : preuve d'absence d'erreurs à l'exécution.
Légende - Résumé :
Xavier Rival présente l'équipe Inria ABSTRACTION (Interprétation abstraite et analyse statique) et l'analyseur statique Astrée dont le but est de prouver l'absence d'erreur à l'exécution dans des programmes C de type synchrone critique tels que des commandes de vol d'avion.

Rencontres Inria - Industrie sur le thème "Les industries de l'aéronautique et de l'espace: modélisation et systèmes sûrs", le 17 mai 2010 à Toulouse.
Nom de fichier :
Inria-697-Abstraction-fr.mp4
Titre :
RII - Astrée : preuve d'absence d'erreurs à l'exécution.
Année :
2010
Durée (min) :
00:03:17
Publications :
https://videotheque.inria.fr/videotheque/doc/697
Autres versions :
Master VF : 697
Master VEN :
Autre : Lien externe :
Lien Equipe-projet :
Lien Centre de Recherche :
Mots clés :
N° master :
697
Durée :
03 min 17 sec
IsyTag :
analyseur - astra - calcul - correction - exécution - fonction - interpellation - programme - rouge - type - variable - zone
Transcription automatiqu :
vous présenter à l'équipe abstraction ainsi que l'analyseur statique astra qui a été élaboré par cette équipe le but de l'analyseur astra de prouver l'absence d'exécutions dans des programmes de type cinq cron critiques tels que des commandes de vol d'avions donc nous ce que nous faisons c'est que nous faisons en un seul calcul en une seule interprétation serait du programme sera approximation de l'ensemble des etats atteignable c'est ce que je représentait en bleu sur graphique donc dans ce cas là la zone blonde à une intersection avec la zone rouge qui est vide donc nous avons effectivement prouvé que le programme ne va pas faire des erreurs à l'exécution pour toutes les exécutions dans le cas où le programme éventuellement une erreur avons donc essayé une execution qui va dans la zone rouge dans la mesure où par construction nous avons toujours calculé un sur approximation de l'ensemble des etats atteignable donc la zone bleue ici on va avoir automatiquement une intersection avec la zone rouge qui va est non vide donc l'analyse va nous dire programme peut ne pas être correct il faut le regarder vais vous montrer l'une des abstraction que fait à ce pour le niveau de précision que je vous avez montré donc sur ce transparent nous avons une fonction d'interpellation donc on a plusieurs domaines sur lesquels on a des formules différentes et pour analyser précisément le programme qui va calculer cela il va falloir quelques années des relations entre le domaine sur lequel on se trouve c'à est dire la formule qu'on va appliquer et les valeurs de la variable d'entrer donc dans un stress ça va être effectué grâce à un parti socialement va euh associer à chaque contexte d'execution des prédicateurs très particuliers dont par ici avons une propriété qui nous dit que si on est dans la deuxième partie dans le deuxième sous domaine de notre nom de fonction interpellation l'entrée est entre moins deux et regarde dans le quatrième chevron la fonction interpellation l'un l'indice vaudra trois et la variable rixe se entre moins et trois au bout du compte lorsqu'on regarde à la fin du programme obtient directement laurent la l'intervalle moins deux pour la variable de sorte est ce qui était calculé par la fonction euh analyser donc ça permet de prouver la correction de l'insertion à la fin à la fin du programme et donc la correction de celui-ci y a deux intérêts par rapport aux méthodes de tests qui sont généralement employées qui consiste à tester le d'exécution du possible notre technique permet de couvrir on entend nos calculs lors d'une journée l'ensemble execution du programme nous fournissons une vraie preuve de correction du programme c'est à dire que la f en de succès de notre analyse on est sûr que le programme ne présentera jamais sous les hypothèses qui ont été compte ailleurs les méthodes de tests sont généralement peu coûteuses dans la mesure où il faut répéter de nombreuses sessions de tests alors que nous on va effectuer un seul calcul de l'ordre de une journée sur une application industrielle telle qu'une commande de vols électriques d'avion cette technique permet de répondre aux exigences des normes de type des eaux cent soixante dix mètres mais à moindre coût et avec un meilleur niveau de qualité actuellement l'outil est en cours d'industrialisation par l'entreprise absente qui en effet la diffusion et le support
Inria-697-Abstraction-fr_HD.MP4

Format : .mp4
120,9 Mo
1024 x 576 pixels
Moyenne définition - équivalent DVD
Encodage PAL .MP4 H264
5 Mbits/s
Sélection
Voir Selection
Déposer ici pour retirer de la sélection