Publications

PKIs in C-ITS: Security functions, architectures and projects: A survey

Abstract

In the smart cities context, Cooperative Intelligent Transportation Systems (C-ITS) represent one of the main use cases that aim to improve peoples’ daily lives. Within these environments, messages are exchanged continuously. The latter must be secure and must ensure users’ privacy. In this regard, Public Key Infrastructures (PKIs) represent the major solution to meet security needs. In this work, we present a holistic survey that describes all the different functions and services of a C-ITS PKI and focus on the different standards and consortia works that have been adopted to regulate such PKIs. Relying on the survey, we highlight the main research problems and open challenges for ITS PKIs. Then, we propose a generic model for a C-ITS PKI architecture.

Continue reading

Featured games

Abstract

Feature-based analysis of software product lines and family-based model checking have seen rapid development. Many model checking problems can be reduced to two-player games on finite graphs. A prominent example is mu-calculus model checking, which is generally done by translating to parity games, but also many quantitative model-checking problems can be reduced to (quantitative) games. As part of a program to make game-based model checking available for software product lines, we introduce featured reachability games, featured minimum reachability games, featured discounted games, featured energy games, and featured parity games. We show that all these admit optimal featured strategies, which project to optimal strategies for any product, and how to compute winners and values of such games in a family-based manner.

Continue reading

GenIDA: An international participatory database to gain knowledge on health issues related to genetic forms of neurodevelopmental disorders

Abstract

Intellectual disability with or without manifestations of autism and/or epilepsy affects 1-2% of the population, and it is estimated that more than 30-50% of these cases have a single genetic cause. More than 1000 genes and recurrent chromosomal abnormalities are involved in these genetic forms of neurodevelopmental disorders, which often remain insufficiently described in terms of clinical spectrum, associated medical problems, etc., due to their rarity and the often-limited number of patients’ phenotypes reported. GenIDA is an international online participatory database that aims to better characterise the clinical manifestations and natural histories of these rare diseases. Clinical information is reported by parents of affected individuals using a structured questionnaire exploring physical parameters, cognitive and behavioural aspects, the presence or absence of neurological disorders or problems affecting major physiological functions, as well as autonomy and quality of life. This strengthens the implication in research of the concerned families. GenIDA aims to construct international cohorts of significant size of individuals affected by a given condition. As of July 2022, GenIDA counts some 1545 documented patient records from over 60 nationalities and collaborates with clinicians and researchers around the world who have access to the anonymized data collected to generate new, medically meaningful information to improve patient care. We present the GenIDA database here, together with an overview of the possibilities it offers to affected individuals, their families, and professionals in charge of the management of genetic forms of neurodevelopmental disorders. Finally, case studies of cohorts will illustrate the usefulness of GenIDA.

Continue reading

How to help digital-native students to successfully take control of their learning: A return of 8 years of experience on a computer science e-learning platform in higher education

Abstract

Continue reading

In pursuit of the hidden features of GNN’s internal representations

Abstract

We consider the problem of explaining Graph Neural Networks (GNNs). While most attempts aim at explaining the final decision of the model, we focus on the hidden layers to examine what the GNN actually captures and shed light on the hidden features built by the GNN. To that end, we first extract activation rules that identify sets of exceptionally co-activated neurons when classifying graphs in the same category. These rules define internal representations having a strong impact in the classification process. Then - this is the goal of the current paper - we interpret these rules by identifying a graph that is fully embedded in the related subspace identified by the rule. The graph search is based on a Monte Carlo Tree Search directed by a proximity measure between the graph embedding and the internal representation of the rule, as well as a realism factor that constrains the distribution of the labels of the graph to be similar to that observed on the dataset. Experiments including 6 real-world datasets and 3 baselines demonstrate that our method DISCERN generates realistic graphs of high quality which allows providing new insights into the respective GNN models.

Continue reading

Topology-aware method to segment 3D plan tissue images

Abstract

The study of genetic and molecular mechanisms underlying tissue morphogenesis has received a lot of attention in biology. Especially, accurate segmentation of tissues into individual cells plays an important role for quantitative analyzing the development of the growing organs. However, instance cell segmentation is still a challenging task due to the quality of the image and the fine-scale structure. Any small leakage in the boundary prediction can merge different cells together, thereby damaging the global structure of the image. In this paper, we propose an end-to-end topology-aware 3D segmentation method for plant tissues. The strength of the method is that it takes care of the 3D topology of segmented structures. The keystone is a training phase and a new topology-aware loss - the CavityLoss - that are able to help the network to focus on the topological errors to fix them during the learning phase. The evaluation of our method on both fixed and live plant organ datasets shows that our method outperforms state-of-the-art methods (and contrary to state-of-the-art methods, does not require any post-processing stage). The code of CavityLoss is freely available at https://github.com/onvungocminh/CavityLoss

Continue reading

On GNN explainability with activation rules

Abstract

GNNs are powerful models based on node representation learning that perform particularly well in many machine learning problems related to graphs. The major obstacle to the deployment of GNNs is mostly a problem of societal acceptability and trustworthiness, properties which require making explicit the internal functioning of such models. Here, we propose to mine activation rules in the hidden layers to understand how the GNNs perceive the world. The problem is not to discover activation rules that are individually highly discriminating for an output of the model. Instead, the challenge is to provide a small set of rules that cover all input graphs. To this end, we introduce the subjective activation pattern domain. We define an effective and principled algorithm to enumerate activations rules in each hidden layer. The proposed approach for quantifying the interest of these rules is rooted in information theory and is able to account for background knowledge on the input graph data. The activation rules can then be redescribed thanks to pattern languages involving interpretable features. We show that the activation rules provide insights on the characteristics used by the GNN to classify the graphs. Especially, this allows to identify the hidden features built by the GNN through its different layers. Also, these rules can subsequently be used for explaining GNN decisions. Experiments on both synthetic and real-life datasets show highly competitive performance, with up to 200% improvement in fidelity on explaining graph classification over the SOTA methods.

Continue reading

A modern C++ point of <i>view</i> of programming in image processing

Abstract

C++ is a multi-paradigm language that enables the programmer to set up efficient image processing algorithms easily. This language strength comes from many aspects. C++ is high-level, so this enables developing powerful abstractions and mixing different programming styles to ease the development. At the same time, C++ is low-level and can fully take advantage of the hardware to deliver the best performance. It is also very portable and highly compatible which allows algorithms to be called from high-level, fast-prototyping languages such as Python or Matlab. One fundamental aspects where C++ shines is generic programming. Generic programming makes it possible to develop and reuse bricks of software on objects (images) of different natures (types) without performance loss. Nevertheless, conciliating genericity, efficiency, and simplicity at the same time is not trivial. Modern C++ (post-2011) has brought new features that made it simpler and more powerful. In this paper, we focus on some C++20 aspects of generic programming: ranges, views, and concepts, and see how they extend to images to ease the development of generic image algorithms while lowering the computation time.

Continue reading

The cost of dynamism in static languages for image processing

Abstract

Generic programming is a powerful paradigm abstracting data structures and algorithms to improve their reusability, as long as they respect a given interface. Coupled with a performance-driven language, it is a paradigm of choice for scientific libraries where the implementation of manipulated objects may change depending on their use case, or for performance purposes. In those performance-driven languages, genericity is often implemented statically to perform some optimization. This does not fit well with the dynamism needed to handle objects which may only be known at runtime. Thus, in this article, we evaluate a model that couples static genericity with a dynamic model based on type erasure in the context of image processing. Its cost is assessed by comparing the performance of the implementation of some common image processing algorithms in C++ and Rust, two performance-driven languages supporting some form of genericity. Finally, we demonstrate that compile-time knowledge of some specific information is critical for performance, and also that the runtime overhead depends on the algorithmic scheme in use.

Continue reading

Transformations d’$\omega$-automates pour la synthèse de contrôleurs réactifs

Abstract

Le travail de cette thèèse s’inscrit dans le cadre de la crééation de manièère automatique de systèèmes corrects àà partir de spéécifications, ce que l’on appelle “synthèse”synthèèse. Ce besoin de crééation automatique vient d’une part de la complexitéé de plus en plus importante des systèèmes que l’on créée mais aussi de la difficultéé de véérifier si un systèème est correct. Pour que la synthèèse soit utilisable en pratique, y compris dans l’industrie, il faut êêtre capable de produire des solutions pour des problèèmes plus ou moins complexes en un temps raisonnable. De plus, on peut chercher àà optimiser les systèèmes produits afin qu’ils soient les plus simples possibles. Pour déécrire les contraintes que le systèème doit respecter, nous utiliserons des formules de logique linééaire temporelle (LTL) qui ajoutent aux opéérateurs Boolééens traditionnels une notion de temps discret afin d’exprimer des contraintes telles que “il existera un instant où la variable sera vraie”il existera un instant oùù la variable sera vraie. Dans notre cas, il s’agira de produire un contrôôleur rééactif, c’est-àà-dire associant àà une suite d’assignations de variables Boolééennes d’entréées une suite d’assignations de variables Boolééennes de sorties.L’approche de la synthèèse LTL que nous allons déécrire consiste àà :- Traduire la spéécification LTL en un jeu de paritéé oùù un joueur contrôôle l’environnement alors que le second repréésente les actions que peut faire le contrôôleur.- Rechercher dans ce jeu s’il existe une stratéégie gagnante pour le second joueur.- Cette stratéégie indique les actions que doit faire le contrôôleur pour respecter les spéécifications et il reste alors àà l’encoder sous la forme voulue (circuit, programme…).Une partie de la premièère éétape est une procéédure dite de paritisation consistant àà obtenir àà partir d’un automate quelconque un automate de paritéé. Une contribution majeure de cette thèèse consiste en l’améélioration de cette procéédure. Dans cette optique, nous proposons et comparons divers algorithmes de paritisation. La premièère mééthode est une combinaison d’algorithmes existants auxquels ont éétéé associéées des heuristiques mais aussi de nouveaux algorithmes. La seconde est l’adaptation d’une mééthode introduite en 2021 par Casares et al. assurant une forme d’optimalitéé sur la taille de l’automate de paritéé obtenu. Dans les deux cas, ces algorithmes ont àà la fois pour objectif de rééduire le temps néécessaire pour une telle transformation mais aussi de limiter la taille de l’automate créééé.Une autre contribution consiste àà proposer des techniques de simplification du contrôôleur. En particulier, nous tirerons parti des libertéés offertes par la spéécification. Par exemple, si l’on souhaite un systèème allumant une ampoule lorsqu’une préésence est déétectéée, alors ce qu’il faut faire lorsque personne n’est déétectéé n’a pas d’importance. Pour obtenir un systèème simple, on peut déécider de toujours allumer l’ampoule et le systèème n’a alors plus besoin d’un capteur. Deux types de simplifications seront déécrites. La premièère est inspiréée d’un outil existant (MeMin) et utilise un SAT-solver pour obtenir une solution minimale. La complexitéé de la recherche d’optimalitéé (NP-complet) nous incite éégalement àà nous tourner vers une seconde mééthode baséée sur les BDD visant àà fournir un systèème rééduit plus rapidement mais sans garantie d’optimalitéé.Ces deux contributions majeures ont éétéé intéégréées àà l’outil ltlsynt distribuéé avec la bibliothèèque Spot et ont éétéé accompagnéées de plusieurs amééliorations que nous éévaluons : une déécomposition du problèème permettant de crééer des contrôôleurs pour des sous-parties de la spéécification mais aussi une mééthode permettant de s’affranchir de la construction d’un jeu pour une certaine classe de formules. Ces travaux ont fait l’objet de publications dans les conféérences ATVA’20 (premièère mééthode de paritisation), TACAS’22 (seconde mééthode de paritisation), FORTE’22 (simplification de contrôôleur), CAV’22 (préésentation des éévolutions de Spot) ainsi que d’une préésentation de ltlsynt lors de la conféérence SYNT’21.L’outil ltlsynt a par ailleurs participéé aux ééditions 2020, 2021 et 2022 de la SYNTCOMP.

Continue reading