|
Model checking symbolique et Hierarchical Set Decision Diagrams| old_uid | 13706 |
|---|
| title | Model checking symbolique et Hierarchical Set Decision Diagrams |
|---|
| start_date | 2014/03/27 |
|---|
| schedule | 15h30-16h30 |
|---|
| online | no |
|---|
| location_info | Grand Amphiteatre |
|---|
| summary | Le model checking est une technique automatique de vérification : les utilisateurs ont seulement à modéliser leurs systèmes et spécifier les propriétés attendues. Pour vérifier celles-ci, un model checker générera l’ensemble des états qu’un système peut atteindre. De ce fait, les systèmes à vérifier étant toujours plus grands, les techniques de model checking doivent faire face à l’explosion combinatoire : le nombre d’états potentiels est souvent bien trop grand pour être traité naïvement. Depuis 30 ans, les recherches se multiplient pour faire face à ce problème. L’apparition des Binary Decision Diagrams (BDD) et leur application au model checking a permis de prendre en charge des systèmes toujours plus grands. Depuis, la famille des diagrammes de décision s’est agrandie pour s’adapter aux spécificités des formalismes pris en charge. Les Hierarchical Set Decision Diagrams (SDD) apportent une généralisation avec une structure souple permettant un encodage hiérarchique des états et un ensemble d’opérations simples et extensibles. En conjonction, une technique appelée "saturation automatique" permet de gagner plusieurs ordres de grandeur en terme de nombres d’états gérés. |
|---|
| responsibles | <not specified> |
|---|
| |
|