Publications

Survey on smart homes: Vulnerabilities, risks, and countermeasures

Abstract

Over the last few years, the explosive growth of Internet of Things (IoT) has revolutionized the way we live and interact with each other as well as with various types of systems and devices which form part of the Information Communication Technology (ICT) infrastructure. IoT is having a significant impact on various application domains including healthcare, smart home, transportation, energy, agriculture, manufacturing, and many others. We focus on the smart home environment which has attracted a lot of attention from both academia and industry recently. The smart home provides a lot of convenience to home users but it also opens up various risks that threaten both the security and privacy of the users. In contrast to previous works on smart home security and privacy, we present an overview of smart homes from both academic and industry perspectives. Next we discuss the security requirements, challenges and threats associated with smart homes. Finally, we discuss countermeasures that can be deployed to mitigate the identified threats.

Continue reading

The reactive synthesis competition (SYNTCOMP): 2018-2021

Abstract

Continue reading

Some equivalence relation between persistent homology and morphological dynamics

Abstract

In Mathematical Morphology (MM), connected filters based on dynamics are used to filter the extrema of an image. Similarly, persistence is a concept coming from Persistent Homology (PH) and Morse Theory (MT) that represents the stability of the extrema of a Morse function. Since these two concepts seem to be closely related, in this paper we examine their relationship, and we prove that they are equal on $n$-D Morse functions, $n\geq 1$. More exactly, pairing a minimum with a $1$-saddle by dynamics or pairing the same $1$-saddle with a minimum by persistence leads exactly to the same pairing, assuming that the critical values of the studied Morse function are unique. This result is a step further to show how much topological data analysis and mathematical morphology are related, paving the way for a more in-depth study of the relations between these two research fields.

Continue reading

A generic approach to quantitative verification

Abstract

Continue reading

Automatically guided selection of a set of underwater calibration images

Abstract

Continue reading

Données, transparence et démocratie

Abstract

Bienvenue dans l’âge des données. Nos actions sur Internet sont enregistrées au profit d’entreprises qui valorisent ces données et offrent des services en échange. Pouvons-nous faire de même ? Pouvons-nous utiliser les données de l’état pour améliorer notre démocratie ?Depuis 2016, les données publiques doivent être ouvertes àà tous. Les citoyens peuvent les analyser pour mesurer l’efficacité de l’action publique ou pour leur compte personnel. Les data journalistes les utilisent pour nous éclairer, les chercheurs pour comprendre. Ainsi la transparence permet de lutter contre la corruption et les intox, tout comme elle est source de progrès.Ce changement de paradigme, l’accès aux données de l’état, est surtout une opportunité pour participer. Noter un dysfonctionnement permet de suggérer une amélioration, un manque peut être une opportunité économique, même un jeu de données incomplet est une occasion pour tisser des liens entre l’administration, les associations et les citoyens.À travers cet essai, l’auteur nous propose un voyage optimiste dans le monde des données. Chemin faisant, les liens entre ces données et la transparence ouvrent la voie vers une démocratie plus ouverte, plus interactive et donc plus juste.

Continue reading

Effective reductions of Mealy machines

Abstract

We revisit the problem of reducing incompletely specified Mealy machines with reactive synthesis in mind. We propose two techniques: the former is inspired by the tool MeMin and solves the minimization problem, the latter is a novel approach derived from simulation-based reductions but may not guarantee a minimized machine. However, we argue that it offers a good enough compromise between the size of the resulting Mealy machine and performance. The proposed methods are benchmarked against MeMin on a large collection of test cases made of well-known instances as well as new ones.

Continue reading

LTL under reductions with weaker conditions than stutter invariance

Abstract

Verification of properties expressed as omega-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a reduction of a system. A reduction has the property that it can only shorten runs. Lipton’s transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. An implementation and experimental evidence is provided showing most non- random properties sensitive to stutter are actually shortening or lengthening in- sensitive. Performance of experiments on a large (random) benchmark from the model-checking competition indicate that despite being a semi-decision proce- dure, the approach can still improve state of the art verification tools. 1 Introduction Model checking is an automatic verification technique for proving the correctness of systems that have finite state abstractions. Properties can be expressed using the popular Linear-time Temporal Logic (LTL). To verify LTL properties, the automata-theoretic approach [25] builds a product between a Buchi automaton representing the negation of the LTL formula and the reachable state graph of the system (seen as a set of infinite runs). This approach has been used successfully to verify both hardware and software components, but it suffers from the so called “state explosion problem”: as the number of state variables in the system increases, the size of the system state space grows exponentially.

Continue reading

Estimation of the noise level function for color images using mathematical morphology and non-parametric statistics

Abstract

Noise level information is crucial for many image processing tasks, such as image denoising. To estimate it, it is necessary to find homegeneous areas within the image which contain only noise. Rank-based methods have proven to be efficient to achieve such a task. In the past, we proposed a method to estimate the noise level function (NLF) of grayscale images using the tree of shapes (ToS). This method, relying on the connected components extracted from the ToS computed on the noisy image, had the advantage of being adapted to the image content, which is not the case when using square blocks, but is still restricted to grayscale images. In this paper, we extend our ToS-based method to color images. Unlike grayscale images, the pixel values in multivariate images do not have a natural order relationship, which is a well-known issue when working with mathematical morphology and rank statistics. We propose to use the multivariate ToS to retrieve homogeneous regions. We derive an order relationship for the multivariate pixel values thanks to a complete lattice learning strategy and use it to compute the rank statistics. The obtained multivariate NLF is composed of one NLF per channel. The performance of the proposed method is compared with the one obtained using square blocks, and validates the soundness of the multivariate ToS structure for this task.

Continue reading

A benchmark of named entity recognition approaches in historical documents

Abstract

Named entity recognition (NER) is a necessary step in many pipelines targeting historical documents. Indeed, such natural language processing techniques identify which class each text token belongs to, e.g. “person name”, “location”, “number”. Introducing a new public dataset built from 19th century French directories, we first assess how noisy modern, off-the-shelf OCR are. Then, we compare modern CNN- and Transformer-based NER techniques which can be reasonably used in the context of historical document analysis. We measure their requirements in terms of training data, the effects of OCR noise on their performance, and show how Transformer-based NER can benefit from unsupervised pre-training and supervised fine-tuning on noisy data. Results can be reproduced using resources available at https://github.com/soduco/paper-ner-bench-das22 and https://zenodo.org/record/6394464

Continue reading