Vendredi 30 Janvier


Retour à la vue des calendrier
Vendredi 30 Janvier
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Une introduction à la théorie de Squier
Description: Yves Guiraud Un monoïde ayant une présentation par un système de réécriture convergent
fini a un problème du mot décidable. Dans les années 1980, Jantzen
s'interroge sur la réciproque : un monoïde ayant un problème du mot
décidable admet-il toujours une présentation par un système de réécriture
convergent fini ? Squier a répondu négativement à cette question en reliant
des propriétés algorithmiques des systèmes de réécriture, comme la
terminaison et la confluence, à des invariants algébriques, comme
l'homologie ou l'homotopie.

Dans cet exposé, je présenterai le résultat initial de Squier, dans le
formalisme de la réécriture de dimension supérieure. Puis, nous verrons
comment le travail de Squier permet aujourd'hui d'utiliser la réécriture
comme méthode constructive pour calculer des invariants de structures
algébriques.
Heure: 14:00 - 14:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Cost Linear Temporal Logic for Verification
Description: Maximilien Colange Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton. The automata-based approach expresses the property as an automaton then analyses its synchronisation with the model automaton. This method can be extended with various automata flavors to handle quantitative properties.

We focus on an extension of Linear Temporal Logic (LTL) with counting capabilities: Cost Linear Temporal Logic (CLTL). This logics can be translated into Büchi automata equipped with counters, so as to nicely extend the automata approach to model-checking. We describe the new properties that this extension allows to handle, illustrated with examples. We also explain how it is linked to existing qualitative LTL model-checking, and the new challenges it poses. We also propose a CEGAR-like approach to answer compute the bounds of the values reached by the automata.
Heure: 14:40 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Vérification de Spécifications EB-3 à l'aide de Techniques de Model Checking
Description: Dimitrio Vekris EB-3 est un langage de spécification développé pour la spécification des systèmes d'information. Le noyau du langage EB-3 comprend des spécifications d'algèbre de processus afin de décrire le comportement des entités du système et des fonctions d'attributs qui sont des fonctions récursives dont l'évaluation se fait sur la trace d'exécution du système décrivant les attributs des entités. La vérification de propriétés temporelles en EB-3 est un sujet de grande importance pour des utilisateurs de EB-3. Dans cet exposé, on se focalise sur les propriétés de vivacité concernant des systèmes d'information exprimant l'éventualité que certaines actions puissent s'exécuter. La vérification des propriétés de vivacité se fait à l'aide de model checking.

En se basant sur une sémantique opérationnelle de EB-3, selon laquelle les fonctions d'attributs sont évaluées pendant l'exécution du programme puis stockées, on définit une traduction automatique de EB-3 vers LNT, qui est un langage simultané enrichi d'une algèbre de processus. Notre traduction assure la correspondance un à un entre les états et les transitions des systèmes étiquetés de transition correspondent respectivement à des spécifications EB-3 et LNT. Ensuite, on automatise la traduction grâce à l'outil EB3toLNT fournissant aux utilisateurs de EB-3 tous les outils de vérification fonctionnelle disponible dans CADP.