Ressource documentaire
| Preuve automatique de la sûreté de logiciels critiques (en Français) | |||
Droits : © Inria Paris - Rocquencourt Auteur(s) : RIVAL Xavier 06-12-2012 Description : Des logiciels tels que des commandes de vol d'avions doivent être d'une fiabilité totale, dans la mesure où un dysfonctionnement du calculateur de vol pourrait entraîner une catastrophe. En particulier, il serait inacceptable qu'un tel logiciel puisse produire des erreurs à l'exécution. Il est mathématiquement impossible de déterminer de manière automatique et exacte si un logiciel informatique est correct, mais il est possible d'effectuer un calcul automatique dit conservatif, qui détectera tout problème potentiel, mais risque d'échouer à prouver la correction de certains programmes qui sont pourtant justes. Je montrerai comment cela peut être effectué grâce à la théorie mathématique de l'interprétation abstraite, et je présenterai quelques applications de ce cadre de travail à des problèmes simples. Mots-clés libres : logiciel,sûreté | TECHNIQUE Type : image en mouvement Format : video/x-flv Source(s) : rtmpt://fms2.cerimes.fr:80/vod/fuscia/preuve.automatique.de.la.s.ret.de.logiciels.critiques_17331/30mnscience_06122012.mp4 | ||
Entrepôt d'origine : Canal-u.fr Identifiant : oai:canal-u.fr:17331 Type de ressource : Ressource documentaire | |||
| Exporter au format XML |
Ressource pédagogique
| Preuve automatique de la sûreté de logiciels critiques (en ) | |||||||||
Identifiant de la fiche : 17331 Schéma de la métadonnée : LOMv1.0, LOMFRv1.0 Droits : libre de droits, gratuit Droits réservés à l'éditeur et aux auteurs© Inria Paris - Rocquencourt Auteur(s) : RIVAL XAVIER Éditeur(s) : INRIA (Institut national de recherche en informatique et automatique) 06-12-2012 Description : Des logiciels tels que des commandes de vol d'avions doivent être d'une fiabilité totale, dans la mesure où un dysfonctionnement du calculateur de vol pourrait entraîner une catastrophe. En particulier, il serait inacceptable qu'un tel logiciel puisse produire des erreurs à l'exécution. Il est mathématiquement impossible de déterminer de manière automatique et exacte si un logiciel informatique est correct, mais il est possible d'effectuer un calcul automatique dit conservatif, qui détectera tout problème potentiel, mais risque d'échouer à prouver la correction de certains programmes qui sont pourtant justes. Je montrerai comment cela peut être effectué grâce à la théorie mathématique de l'interprétation abstraite, et je présenterai quelques applications de ce cadre de travail à des problèmes simples. Mots-clés libres : logiciel, sûreté
| PEDAGOGIQUE Type pédagogique : cours / présentation Niveau : master, doctorat TECHNIQUE Type de contenu : image en mouvement Format : video/x-flv Taille : 3.17 Go Durée d'exécution : 36 minutes 48 secondes RELATIONS Cette ressource fait partie de : | ||||||||
Entrepôt d'origine : Canal-u.fr Identifiant : oai:canal-u.fr:17331 Type de ressource : Ressource pédagogique | |||||||||
| Exporter au format XML |