Seminar/2012-07-04

Mercredi 4 juillet 2012, 14h00-16h30, Amphi 4

Vérification efficace de propriétés insensibles au bégaiement.

Documents

ben-salem.pdf

Ala Eddine Ben Salem (doctorant)

Le model checking est une technique de vérification formelle automatique. Prenant en entrée un modèle décrivant toutes les exécutions possibles du système et une propriété exprimée sous la forme d'une formule de logique temporelle, un algorithme de model checking répond si le modèle satisfait ou non la formule. Le problème principal du model-checking est l'explosion combinatoire de l'espace d'états décrivant le système.

Afin d'améliorer les performances, on a apporté les contributions suivantes à l'approche automate du model checking. D'abord l'amélioration de l'algorithme de vérification en deux passes de l'approche basée sur les automates Testeur TA (Testing Automaton). Ensuite la proposition d'une méthode permettant de transformer un automate TA en un automate vérifiable en une seule passe, qu'on a appelé STA (Single-pass Testing Automaton). Enfin, la contribution la plus significative est un nouveau type d'automate baptisé TGTA (Transition-based Generalized Testing Automaton). L'apport principal de cette nouvelle approche consiste à proposer une méthode permettant de supprimer les transitions bégayantes dans un TGTA sans avoir besoin, ni d'ajouter une seconde passe comme dans l'approche TA, ni d'ajouter un état artificiel comme dans l'approche STA.

A.E. Ben Salem est ingénieur ENSEEIHT-2005 en Informatique et Mathématiques Appliquées, il a obtenu en parallèle un Master Recherche Sûreté du Logiciel et Calcul à haute Performance à l’INP Toulouse. Depuis 2011, il est doctorant au LRDE et au LIP6 sur la vérification formelle de propriétés sur des systèmes logiciels, en lien avec le projet Spot.

Composition dynamique de techniques pour le model checking efficace

Documents

renault.pdf

Étienne Renault (doctorant)

Le model checking est une technique qui permet de s'assurer qu'un système vérifie un ensemble de caratéristiques appelées propriétés. Le système et la négation de la formule sont ensuite représentés de manière abstraite (ici un automate) pour pouvoir détecter des comportements incohérents. Ces propriétés ont été classifiées et possèdent des particularités qui peuvent être exploitées afin de réduire la complexité du processus de vérification. Nous montrerons ici comment tirer parti dynamiquement des différentes classes de formules.

E. Renault est diplômé de Paris VI en système et applications réparties, il s'intéresse à la vérification formelle des systèmes concurents. Il a intégré cette année le LRDE dans le cadre de sa thèse portant sur la composition dynamique de techniques pour le model checking efficace. Ce travail, en collaboration avec l'équipe MoVe du Lip6, s'intègre au projet Spot.

Filtrage morphologique dans les espaces de formes : Applications avec la représentation d'image par arbres

Documents

xu.pdf

Yongchao Xu (doctorant)

(Morphological Filtering in Shape Spaces: Applications using Tree-Based Image Representations)

Connected operators are filtering tools that act by merging elementary regions of an image. A popular strategy is based on tree-based image representations: for example, one can compute a shape-based attribute on each node of the tree and keep only the nodes for which the attribute is sufficiently strong. This operation can be seen as a thresholding of the tree, seen as a graph whose nodes are weighted by the attribute. Rather than being satisfied with a mere thresholding, we propose to expand on this idea, and to apply connected filters on this latest graph. Consequently, the filtering is done not in the image space, but in the space of shapes built from the image. Such a processing is a generalization of the existing tree-based connected operators. Indeed, the framework includes classical existing connected operators by attributes. It also allows us to propose a class of novel connected operators from the leveling family, based on shape attributes. Finally, we also propose a novel class of self-dual connected operators that we call morphological shapings.

Yongchao Xu received the B.S. degree in optoelectronic engineering from Huazhong University of Science and Technology, China, in 2008, the "diplôme d'ingénieur" in electronic & embedded system at Polytech' Paris-Sud and the M.S. degree in signal & image processing from Université Paris Sud, in 2010. He is currently a PhD student at Université Paris Est working on image segmentation, morphological image analysis and, especially shape-based connected morphology.