Séminaires
Séminaire du 10 Janvier 2006
Lieu
LIP6: comment y aller
Programme
14h00-15h00: Sébastien Bardin (LSV) : FAST : théorie et pratique de l'acceleration
Abstract:Le model checking est maintenant une technique mature pour les systèmes à espaces d'états finis. Cependant, de nombreuses machines réelles ont naturellement un espace d'états infini. Nous nous intéressons à la verification de systèmes infinis. Notre approche se base sur :
- une représentation symbolique pour manipuler effectivement des ensembles infinis X d'états atteignables
- des algorithmes d'acceleration pour calculer en un pas t^*(X), ou t est un circuit du système
- une heuristique pour sélectionner les circuits a accélérer.
Nous montrerons comment cette approche a été instanciée dans le cas des systèmes à compteurs. Les résultats ont été implantes dans l'outil FAST, qui a permis de verifier à ce jour une quarantaine de systèmes à compteurs infinis, et surpasse les outils concurrents de calcul symbolique exact.
15h00-15h30 : Houda Bel Mokadem (LSV) : « Vérification presque partout de propriétés temporisées »
Abstract: les automates programmables industriels (API) sont des mémoires programmables, largement utilisées dans l'industrie pour contrôler les systèmes automatisés. Les programmes des APIs manipulent des variables discrètes, entières ou booléennes, ce qui conduit à des ambiguïtés dûes à la phase de modélisation. En effet, certaines variables peuvent avoir plusieurs valeurs à un instant donné. Ainsi une propriété peut être toujours vraie sauf pendant un moment qui dure 0 unité de temps. Nous nous intéressons donc à vérifier sur les APIs des propriétés temporisées vraies presque partout c'est-à-dire vraies partout sauf sur un ensemble de mesure nulle. Nous proposons une extension de la logique TCTL pour spécifier ce genre de propriétés. Ensuite, nous montrons que cette logique est plus expressive que TCTL et que le model-checking pour cette logique est PSPACE-complet.