28 août-1 sept. 2017 Paris (France)

Programme

mardi 29 août 2017
10:00
11:00
12:00
13:00
14:00
15:00
16:00
17:00
›10:00 (1h)
Vérification et imposition de propriétés temporisées à l’exécution - Yliès Falcone (LIG, Université de Grenoble)
La vérification à l'exécution désigne les théories, techniques et outils pour déterminer si un système respecte l'ensemble de ses propriétés attendues à partir d'informations collectées durant son exécution. La vérification à l'exécution peut être appliquée lors du développement du système à des fins de débogage ou lorsque le système est en service pour détecter des comportements erratiques qui n'ont pu être évités durant sa conception. L'imposition à l'exécution complète la vérification à l'exécution et concerne plus particulièrement la prévention des erreurs et l'automatisation des réactions aux comportements erratiques. Dans cet exposé, nous présenterons les travaux menés en vérification et imposition de propriétés temporisées sur les systèmes temps réels. Les propriétés temporisées régissent non seulement le séquencement des actions dans les systèmes mais aussi le temps physique qui s'écoule entre ces actions.
›11:00 (30min)
›11:30 (1h)
Vérification classique et statistique pour les systèmes probabilistes - Benoît Delahaye (LS2N, Université de Nantes)
La modélisation et l'abstraction des systèmes est aujourd'hui un point de passage nécéssaire à l'étude et à la compréhension de ceux-ci. Que ce soit dans le cadre de l'étude de systèmes physiques (sciences du vivant, automatique, ...) ou du développement de systèmes logiciels, il est souvent nécéssaire d'avoir recours aux probabilités pour abstraire des aspects trop complexes, prendre en compte l'incertitude due aux observations ou introduire artificiellement de l'aléatoire. Dans cet exposé, nous passerons en revue les différents formalismes de modélisation pour systèmes probabilistes (discrets, continus, avec ou sans non-déterminisme) ainsi que les principales méthodes de vérification applicables à ces modèles. Nous mettrons particulièrement l'accent sur la vérification de modèles probabiliste (exacte) et sur la vérification de modèles statistique (approchée).
›12:30 (1h30)
›15:30 (30min)
Session
Discours
Logistique
Pause
Sortie
Personnes connectées : 1