Visioconférence: Zoom (https://tinyurl.com/1a86yh1n)
Résumé: La vérification de systèmes est un sujet de recherche important et différentes techniques permettent de vérifier formellement des systèmes critiques dont il faut garantir la correction. Nous aborderons l’une des techniques formelles les plus utilisées et les plus efficaces, l’évaluation de modèle (model checking en anglais). Pour vérifier un système par évaluation de modèle, on abstrait d’abord son comportement sous la forme d’un système de transitions appelé modèle. Ensuite, on formule une propriété désirée du système dans une logique temporelle. Enfin, on utilise un outil logiciel appelé vérificateur pour vérifier automatiquement si le modèle satisfait la propriété. Contrairement aux vérifications par tests, cette vérification est hors de tout doute.
Nous alons montrer une nouvelle technique pour vérifier des propriétés d’atteignabilité dans des modèles probabilistes appelés processus de Markov étiquetés (en anglais, LMP pour Labelled Markov processes) et qui ont possiblement un ensemble d’états non dénombrable. À partir des propriétés particulières à vérifier, nous construisons un modèle fini probabiliste qui lui peut être vérifié avec des outils existants.
Le modèle fini est construit de telle sorte que nous inférons que le LMP satisfait la propriété d’atteignabilité, si et seulement si le système fini la satisfait. Ainsi, théoriquement, notre approche donne un résultat ultime exact et nous l’avons prouvé. À l’implémentation, nous utilisons une méthode d’intégration numérique pour déterminer les probabilités de transition dans le modèle fini. Malgré les imprécisions numériques qui peuvent nuire au résultat d’une vérification, nous avons prouvé que notre approche a du sens en quantifiant les erreurs. Notre méthode repousse les limites de l’évaluation de modèle, notamment l’explosion combinatoire de l’espace d’états ou de chemins dans la vérification de systèmes probabilistes infinis.
Pour accéder aux enregistrements: http://www2.ift.ulaval.ca/~quimper/Seminaires/