Bonjour,
nous avons le plaisir de vous inviter au Séminaire des étudiants du LRDE.
Il aura lieu le mercredi 16 janvier 2019 à partir de 10h00 en Amphi IP11 (KB).
Les étudiants ING3 présenteront le résultat de leurs travaux des derniers
mois.
Au programme :
SPOT — BIBLIOTHEQUE DE MODEL CHECKING
10h00 Recherches de contrexemple dans
Spot – CLÉMENT GILLARD
Spot est une bibliothèque de manipulation
d'ω-automates qui tend à aider la vérification de
modèles par ω-automates et le développement d'outils
de transformation d'ω-automates. Elle fournit donc de
multiples algorithmes avec de multiples implémentations qui
fonctionnent sur une grande variété d'ω-automates.
Parmi ces algorithmes, les tests de
vacuité et les recherches de contrexemple sont souvent
utilisés pour diverses raisons. Comme leurs résultats
sont liés, ils sont souvent utilisés ensemble. Cependant,
il manque à Spot les implémentations de recherche de
contrexemple correspondant à certaines implémentations de
tests de vacuité qui soient capables de travailler de la
même manière sur les mêmes automates. Nous
présentons deux implémentations de calcul de contrexemple,
qui viennent compléter deux implémentations de tests de
vacuité déjà existantes, qui suivent leur sillage et se
servent des données déjà accumulées pour construire
efficacement des contrexemples.
10h30 Compression d’états dans
Spot – ARTHUR REMAUD
Pour représenter un système par un automate, il
faut sauvegarder toutes les valeurs des variables
du système pour chaque état de l'automate. Cela
peut prendre beaucoup de place en mémoire
lorsqu'il y a beaucoup de variables et/ou d'états,
et de fait ralentit le temps d'exécution à cause
des défauts de cache. Pour contourner ce problème
dans Spot, on utilise une simple compression du
tableau contenant les variables d'un état, et ce
pour chaque état, ce qui réduit la mémoire
utilisée et aussi le temps d'exécution. Dans ce
rapport, nous présentons une structure de données
qui améliore la compression des variables en
utilisant la redondance des valeurs présentes
dans différents états, et les différents
problèmes rencontrés lors de son ajout dans
Spot.
11h00 Mesures sur la réduction d’ordre partiel
dans Spot – VINCENT TOURNEUR
Ce rapport résume trois méthodes implémentées dans
l'outil de vérification de modèles Spot. La première
vise à améliorer la conversion de modèle de programme
en structure de Kripke grâce à la réduction d'ordre
partiel, une technique qui ignore l'ordre de certaines
actions du programme. Cela permet de réduire la taille de
la structure de Kripke. La seconde méthode modifie la
première pour permettre de l'utiliser pour tester des
propriétés LTL. La troisième a pour but de vérifier
qu'un modèle ne contient pas de livelock, sans utiliser de
propriété LTL. Nous testons toutes ces méthodes, en nous
concentrant sur leur but commun : réduire la quantité de
mémoire requise, ce qui est un goulot d'étranglement
important dans le domaine de la vérification de
modèles.
--
Daniela Becker
Responsable administrative du LRDE
