Abstract
From LRDE
R
Spot est une bibliothèque C++ de model checking utilisant l'approche par automates. Pour représenter les propriétés à vérifier, nous utilisons des formules LTL, qui sont traduites en automates. Dans Spot, ces automates sont des Automates de Büchi généralisés basés sur les transitions (TGBA). Un enjeu pour tout model checker, est d'être rapide. Une manière de faire est de rendre les automates aussi petit que possible. La littérature scientifique propose de nombreux algorithmes pour arriver à notre but. La bisimulation et la simulation réduisent des automates qui reconnaissent des mots de longueur infinis. Cette présentation montre comment adapter ces algorithmes pour des TGBA ainsi que le gain apporté par l'implémentation de la bisimulationce qui souligne l'importance d'implémenter la simulation pour réduire les TGBA. +
Les outils de vérification formelle souffrent actuellement d'un problième de passage á l'échelleà cause de leur consommation de mémoire. La réduction d'ordre partiel est une des techniques permettant de la réduire notablement, en ne calculant que les données requises à la volée. Il en existe beaucoup d'algorithmes à l'état de l'art, et cette technique est utilisée dans plusieurs logiciels (comme SPIN ou LTSmin). Nous allons parler ici de l'implémentation de certains de ces algorithmes dans la bibliothèque Spot, puis de leur optimisation. Les résultats obtenus montrent une diminution notable de la consommation de mémoire, ce qui implique un gain pour toutes les étapes suivantes de la vérification. +
Les ω-automates, capables de modéliser des comportements infinis, sont utilisés dans de nombreux domaines dont la vérification de modèle. Les algorithmes utilisés sont en général très coûteux. Pour cette raison, on veut réduire la taille des automates, tout en préservant le langage reconnu en appliquant de nombreuses réductions. Dans ce rapportdans la continuité du précédent, nous allons présenter de nouvelles améliorations à la réduction basée sur des simulations et un nouvel algorithme: le raffinement de chemin. +
L'approche par automates du model checking s'appuie traditionnellement sur des Automates de Büchi (BA) qu'on souhaite les plus petits possible. Etessami et al. ont présenté une méthode de réduction d'un BA basée sur une relation de simulation (dite directe) entre ses états. Spot, bibliothèque de model checking, utilise principalement des TGBA qui généralisent les BA. Nous montrons qu'en adaptant cette simulation aux TGBA on obtient des automates plus concis que les BA équivalents. Cette nouvelle technique est incluse dans Spot 0.9 et a permis de produire des automates plus petits que dans les précédentes versions. +
L'approche par automates du model checking s'appuie traditionnellement sur des Automates de Büchi (BA) qu'on souhaite les plus petits possible. Spot, bibliothèque de model checking, utilise principalement des TGBA qui généralisent les BA. Nous avons déjà présenté une méthode de réduction par simulation (dite directe). Cette technique a permis de produire des automates plus petits que dans les précédentes versions. La simulation consiste à fusionner les états ayant le même suffixe infini. Nous montrons que nous pouvons aussi fusionner ceux ayant le même préfixe infini (c'est la cosimulation). On peut répéter la simulation et la cosimulation pour créer la simulation itérée. Cette méthode est incluse dans Spot 1.0 et est une grande amélioration de la simulation. On expérimente aussi une méthode qui consiste à modifier certaines conditions d'acceptations (appellées sans importances). Puisque celles qui sont sur les transitions entre composantes fortement connexes n'ont pas d'influence sur le langage, on peut les modifier pour aider la simulation. +
Même si la précision du système de localisation de texte développé par le laboratoire a aujourd'hui grandement augmenté, un des principaux problèmes demeure la vitesse. En effet, si l'on souhaite être en mesure de l'utiliser pour extraire du texte dans des vidéos ou s'il doit être embarqué dans des appareils aux ressources limitées tel que des téléphones portables, la consommation de ressources mémoire et CPU doit être réduite. Pour parvenir à cet objectifplusieurs méthodes permettant de réduire l'impact mémoire et CPU des étapes les plus coûteuses peuvent être utilisées. Cependant, toutes n'offrent pas les mêmes résultats en fonction de l'image d'entrée et certaines peuvent même dégrader le résultat final produit par le système. L'objectif est de présenter ces méthodes, d'observer leurs résultats et de déterminer dans quelles situations elles sont applicables. +
Spot peut gerer les automates testeurs depuis Spot 1.0. Cependant, Spot 2.0 introduit une nouvelle structure de données pour les automates avec des conditions d'acceptance génériques. Notre but est de réimplémenter les automates testeurs en utilisant cette nouvelle structure de données. Cela fait, nous espérons pouvoir réutiliser les algorithmes existants, réduire la quantité de code impliquant les automates testeurs et de rendre les automates testeurs compatibles avec le format HOA.L' implémentation choisis permettrait de reduire la taille des automates testeurs. +
S
Scool is a static object-oriented language. It has been created to help one to take advantage of all the power of static Cxx thanks to a more expressive syntax. It is not directly compiled but is translated into Cxx. This year was quite important for the project. Indeed, there are tight links between Scool's development and the generic image processing library Milena from the Olena platform. As some big changes occured in the library, work needs to be done to adapt the language to its new paradigms and to its new needs. Work also needs to be done to continue the implementation of the different features of Scool. This year the work will be focused on concept-oriented programming. This allows one to easily express constraints on generic programming. +
Cxx has proved to be a powerful language to write generic and efficient libraries. However using classical oo Cxx may not fulfill the efficiency criterion sought in some domains, e.g. when building scientific librarieswhere large data sets have to be processed through generic algorithms. A solution consists in combining the power of oop and emphstatic programming— which is in fact meta-code expressed thanks to Cxx template constructs. This has the advantage to replace the oo run-time overhead (due to virtual method dispatch) by compile-time computations. However, such an approach relies on code that is verbose, hard to write and to maintain. Though powerfulCxx lacks high-level static features, and thus clutters the semantics of static constructs with unrelated code. We present Scool, a static language mixing acoo and gp that has been created to take advantage of all the power of static Cxx thanks to a more expressive syntax and high-level constructs, without the drawbacks of plain Cxx. As a full-fledged static OOP language, Scool provides polymorphic methods (i.e., inclusion polymorphism), with the notable difference that every polymorphic call is statically-resolved: the design of Scool is based on the property that the exact (dynamic) type of every object is known at compile-time. As the aim of Scool is to bring all the power of static oop to Cxx, it is not directly compiled but translated into human-readable Cxx. The development of the translator raised classical problems found in dsl like traversal strategies of the abstract syntax tree. We propose an original solution based on the Stratego/XT program transformation framework, and some applications on Milena, a generic and efficient Cxx library from the Olena image processing platform. +
Le Cxx est un langage puissant pour écrire des bibliothèques génériques et performantes. Cependantdans certains domaines l'utilisation de l'orienté objet usuel peut poser des problèmes de performances, comme dans celui des bibliothèques de calcul scientifique dans lesquelles de grands ensembles de données parcourus par des algorithmes génériques. La solution proposée est la combinaison de la programmation orientée objet classique et de la programmation statique qui est en fait de la meta-programmation utilisant intensivement les templates du Cxx. Ceci a l'avantage de remplacer le coût à l'éxecution de l'orienté objet dû à la résolution des méthodes virtuelles par un coût `a la compilation. Cependant, cela engendre souvent du code verbeux, difficile à écrire et à maintenir. Malgré sa puissance, le Cxx ne possède pas d'abstractions statiques de haut niveau ce qui encombre la sémantique du code avec des détails d'implémentation. Nous vous présentons Scool, un langage statique fusionnant l'orienté objet et la programmation générique dans le but d'éxploiter toute la puissance du Cxx statique grâce à une syntaxe plus expressive. De plus, toutes les résolutions de méthodes se feront statiquement grâce au fait que le type exact (dynamique) de chaque objet est connu à la compilation. Le but de Scool étant d'apporter toute la puissance de l'orienté objet statique au Cxx, il ne sera pas directement compilé mais traduit en Cxx correctement formaté. Le développement du traducteur a soulevé les problèmes classiques du domaine des DSL comme la stratégie de parcours de l'arbre de syntaxe. Nous proposons une solution originale basée sur la plateforme de transformation de programme Stratego/XT avec des applications à Milena, la bibliothèque générique et performante de traitement d'image de la plateforme Olena. +
Scool est un langage statique orienté objet qui a été créé afin de pouvoir utiliser toute la puissance du Cxx statique de manière plus aisée grâce à une syntaxe plus expressive et agréable. Il n'a pas pour but d'être directement compilé mais d'être traduit en Cxx. Cette année le travail revêt une importance particulière. En effet, Scool est développé en étroite collaboration avec l'équipe de développement de la bibliothèque de traitement d'images Milena de la plate-forme textscOlena ; l'an passé a été pour elle le cadre de grands changements internes. Un des axes majeurs du développement de Scool va donc être de s'adapter aux nouveaux paradigmes et aux nouveaux besoins de la bibliothèque. Le second axe essentiel de travail est la poursuite du développement du langage. Cette année le travail va être concentré sur la programmation par concepts qui est une approche permettant de formaliser facilement des contraintes sur la programmation générique. +
The Common Lisp language provides a predicate functionSUBTYPEP, for instrospecting sub-type relationship. In some situations, and given the type system of this languageknowing whether a type is a sub-type of another would require enumerating all the element of that type, possibly an infinite number of them. Because of that, SUBTYPEP is allowed to return the two values (NIL NIL), indicating that it couldn't answer the question. Common Lisp implementations have a tendency to frequently not answereven in situations where they could. Such an abusive behavior prevents potential optimizations to occur, or even leads to violating the standard. In his paper entitled “A Decision Procedure for Common Lisp's SUBTYPEP Predicate”Henry Baker proposes an algorithm that he claims to be both more accurate and more efficient than the average SUBTYPEP implementation. In this report, we present a partial implementation of his algorithm, discuss some technical aspects, present some benchmarks and most importantlycompare the accuracy of both implementations. +
Le langage Common Lisp fournit un prédicat, SUBTYPEPqui permet d'introspecter la relation de sous-typage. Dans certaines situations, étant donné le système de typage du langage, il est impossible de déterminer si un type est un sous-type d'un autre sans en énumérer tous les éléments, possiblement en nombre infini. À cause de cela, SUBTYPEP est autorisé à retourner deux valeurs (NIL, NIL), indiquant qu'il n'a pas pu trouver de réponse. Les implémentations de cette fonction ont trop souvent tendance à ne pas répondre, même dans des situations où c'est théoriquement possible. Ce comportement abusif peut alors empêcher certaines optimisations potentielles du compilateur, voire même rendre l'implémentation non conforme au standard. Dans son article og A Decision Procedure for Common Lisp's SUBTYPEP Predicate fg, Henry Baker propose un algorithme qu'il prétend plus précis et plus performant que l'implémentation moyenne de SUBTYPEP. Dans ce rapport nous présentons une implémentation partielle de l'algorithme de Baker, nous exposons certains aspects techniques, nous présentons une étude des performances et enfin nous comparons l'acuité des différentes implémentations du prédicat. +
The best speaker verification systems are based on score combination of several approaches. Support Vector Machines (SVM) give very hopeful results. Thus, combining these methods could be very efficient. In our approach, we propose a new combination method for speaker verification systems based on SVM methods. This one performs a linear combination of several kernel functions in order to produce a new kernel function. In this combination, the weights are speaker dependent, by opposition of score combination approach for which the weight are universal. The idea is to adapt the combination weights for each speaker in order to take the advantage of the best kernel. In our experimentcombinations are performed on several kernel functions: the GLDS kernel, linear and Gaussian GMM supervector kernels. The method can use every kernel functions with no modification. The experiments are done on the NIST-SRE 2005 and 2006 (all trials) database. +
Les meilleurs systèmes de Verification du Locuteur (VL) sont fondés sur la fusion des scores de décision de plusieurs approches. Les méthodes basées sur les Séparateurs à Vaste Marge (SVM) donnent des résultats très performants. En conséquence, l'apport de ces méthodes est très important pour la fusion. Dans notre approche, nous proposons une nouvelle méthode de fusion des systèmes de VL basés sur les méthodes SVM en construisant une nouvelle fonction noyau à partir d'une combinaison linéaire de plusieurs fonctions. Dans cette combinaison, les poids utilisés varient selon les locuteurs, ce qui diffère des approches par fusion de score qui elles utilisent des poids universels. L'idée est donc de tirer avantage des performances de chacun des noyaux, et cela pour chaque locuteur donné. Ces combinaisons sont effectuées sur plusieurs types de noyaux dont les noyaux GLDS, GMM supervecteurs linéaires et Gaussiens. Les expériences sont réalisées sur la base des corpus NIST-SRE 2005 et 2006. +
State of the art speaker verification systems provide a decision based on cosine distance. A different approach is to consider a decision based on Support Vector Machine (SVM) separation. SVMs have been largely used in pattern recognition and decision making as well as in combination with GMM super-vectors (GSV). However, the idea of using SVMs in the i-vector space for speaker recognition has not been well explored. We will study the different kernel functions and how it could be used in speaker verification with i-vector space. We will explore how we could deal with channel and speaker variabilities in the feature space. The experiments are done on NIST-SRE 2010 core condition database. +
Afin d'améliorer la performance globale des systèmes de vérification du locuteur, il faut diversifier les approches. Le but de ce travail est d'étudier les performances d'un système SVM-MLLR. Cette méthode se base sur la construction, à partir du modèle du monded'une transformation linéaire des vecteurs moyennes (mean supervectors) maximisant la vraisemblance du modèle transformé par rapport aux données locuteur. On évaluera deux approches différentes : Dans la première, on utilisera directement le logarithme du rapport de vraisemblance (GMM-MLLR). Dans une deuxième expérimentation, on utilisera les SVMs pour évaluer les scores de décision. La dernière étape consiste à valuer l'apport d'une méthode de compensation du canal (NAP: Nuisance Attribute Projection) sur les performances de ce système). Une fusion des scores avec d'autres systèmes GMM sera étudiée. Une fusion au niveau des noyaux sera quand à elle présentée par Charles-Alban. Tous les tests vont être menés sur les deux bases de données NIST-SRE 2005 et 2006 all trials. +
Afin d'améliorer la performance globale des systèmes de vérification du locuteur, il faut diversifier les approches. Le but de ce travail est d'étudier les performances d'un système SVM-MLLR. Cette méthode se base sur la construction, à partir du modèle du monded'une transformation linéaire des vecteurs moyennes (mean supervectors) maximisant la vraisemblance du modèle transformé par rapport aux données locuteur. On évaluera deux approches différentes : Dans la première, on utilisera directement le logarithme du rapport de vraisemblance (GMM-MLLR). Dans une deuxième expérimentation, on utilisera les SVMs pour évaluer les scores de décision. La dernière étape consiste à valuer l'apport d'une méthode de compensation du canal (NAP: Nuisance Attribute Projection) sur les performances de ce système). Une fusion des scores avec d'autres systèmes GMM sera étudiée. Une fusion au niveau des noyaux sera quand à elle présentée par Charles-Alban. Tous les tests vont être menés sur les deux bases de données NIST-SRE 2005 et 2006 all trials. +