Portail HAL des publications du LIRMM
Not a member yet
13279 research outputs found
Sort by
Méthodes formelles pour la programmation et l'analyse de comportements robustes des systèmes autonomes
No full textThe development of autonomous robotic systems uses intelligent functions, system control, data treatment or trajectory planning. These functions are implemented through programmation environments such as ROS, which results in complex software architectures, where dozens of processus run together.The design of autonomous missions demands high-level behavior specifications, which lie on functions given by the robotic system. These behaviors require to be robust if problems arise (for instance, sensor failure), or external events due to the mission and its environment. Furthermore, in critical contexts, high risk missions or when the intervention of a human operator is impossible, it is necessary to bring proofs on the robust and correct behavior of the system. To that end, classical test methods or simulations can prove insufficient for the system.This thesis subject aims to tackle the problematic of specification and analysis of behaviors, through formal methods. Formal methods and Petri networks in particular will be studied for its convenience when specifying concurrent behaviors, possibility to run models, as well as existing tools for model-checking.Le développement de systèmes robotiques autonomes met en oeuvre des fonctionnalités intelligentes, de contrôle du système, de traitement de ses données, ou de planification de sa trajectoire. Ces fonctionnalités sont implantées au travers d’environnements de programmation tels que ROS, ce qui résulte en des architectures logicielles complexes, faisant intervenir plusieurs dizaines de processus.La réalisation de missions en autonomie nécessite de pouvoir spécifier des comportements haut-niveau, qui reposent sur les fonctionnalités fournies par le système robotique. Ces comportements nécessitent d’être robustes à la survenue de pannes sur le système robotique (par ex. pannes de capteurs), ou à des événements extérieurs liés à la mission et à son environnement. De plus, dans des contextes critiques, pour des missions risquées ou lorsque l’intervention d’un opérateur humain est quasiment impossible, il est nécessaire d’apporter des preuves a priori sur le comportement robuste et correct du système. Dans ce cadre, les techniques classiques de tests ou de simulation peuvent se révéler insuffisants à garantir une confiance suffisante dans le système.Ce sujet de thèse vise à aborder cette problématique de la spécification et de l’analyse de comportements, au moyen de méthodes formelles. Le formalisme des réseaux de Petri sera en particulier étudié de par son adéquation à la spécification de comportements concurrents, la possibilité d’exécuter les modèles, ainsi que les outils de model-checking existants
Evidence of distal regulations orchestrated by RNAs initiating at short tandem repeats
No full textShort Tandem Repeats (STRs), also called microsatellites, correspond to tandemly repeated short DNA motifs (1 to 6 bp) and are one of the most polymorphic and abundant repetitive elements in the human genome. Variations of their length (i.e. number of consecutive repeats) have been implicated in gene expression regulation (termed expression(e)STRs). Using cap-trapping followed by long read sequencing, we discovered that STRs can host transcription start sites, the presence of which depends mainly on STR flanking sequences. Here, we investigate the effect of SNPs located in these sequences and ask whether STR-initiating RNAs have regulatory potential. First, we develop fully interpretable deep learning-based models, called Modular Neural Networks, able to predict, for each STR class, the level of RNAs using 101bp-long sequences encompassing STRs. Analysis of MNN filters allows us to identify multiple regulatory elements and candidate transcription factors. Second, leveraging genome sequencing and gene expression data from the Genotype-Tissue Expression project, we use the output of our models to link the levels of STR-initiating RNAs to the expression of nearby genes. We identify 14,340 significant associations (coined RNA(r)STRs) and illustrate how this novel resource can help interpret non-coding variants associated with complex traits and diseases. Third, we unveil an intricate transcriptional interplay between STR-initiating RNAs and Alu repeats that may couple their regulatory actions, extending both the nature and the functional importance of non-coding transcription and shedding new light on the complexity of distal regulations orchestrated by repeated sequences
D1.3 - Recommendations for a FAIR EOSC - White Paper of the FAIR-IMPACT Synchronisation Force
No full textInspired by strategic reports on FAIR and EOSC from the period 2018-2024, the annual FAIR-IMPACT Synchronisation Force workshops discussed key topics on the road to more FAIR digital objects. In this White Paper the main recommendations from these workshops are taken a step further, and mapped to two Strategic Pillars of the EOSC Multi-Annual Roadmap 2026-2027 and the relevant Task Forces and Opportunity Area Expert Groups under the EOSC Association, to facilitate their uptake and impact
Multivariate Time Series Visualization for a Single Individual: A Scoping Review Using PRISMA-ScR
No full textInternational audienceThe digitization of hospital information systems is becoming widespread, enabling the increasing integration of interactive visualization methods into decision support systems. This development facilitates the anticipation of critical risks in monitored patients and helps reduce the workload of healthcare providers. However, Electronic Health Records (EHRs) contain large, heterogeneous, and temporal data. Then, providing tools to understand these complex data is a challenge. Using PubMed and Google Scholar, we conducted a search for articles using keywords related to time, visualization, and data. Out of 3,197 retrieved articles, we identified 111 relevant ones through clustering. Applying exclusion criteria to focus on implemented prototypes, we manually annotated 21 articles for our review. This exploratory literature analysis reveals that while this research area has garnered recent interest, it demonstrates limitations in the proposed solutions. Few approaches employ temporal axis distortion, and no approach in the medical domain visually integrates model predictions. The study highlights preferred functionalities for the visual representation of multivariate temporal data, such as parallel time series and hierarchical views
RomoMicro
No full textRomoMicro is a Software/prototype for the Micro-service based architecture architecture recovery based on the static analysis of monolithic Java application
Romo-API
No full textRomo-API is a software (research prototype) that aims to identify clusters of classes in JAVA-based APIs (e.g. Android APIs) that can be considered as software components with explicit required and provided interfaces (e.g. OSGI components). The goal is to enhance reusability and understandability of these API
HALTRAV: Design of A High-performance and Area-efficient Latch with Triple-node-upset Recovery and Algorithm-based Verifications
No full textInternational audienceWith the rapid advancement of semiconductor technologies, latches become increasingly sensitive to soft errors, especially triple-node-upsets (TNUs), in harsh radiation environments. In this paper, we first propose a high-performance and area-efficient latch, namely HALTRAV, featuring complete TNU-recovery. The storage portion of HALTRAV consists of 28 interlocked source-drain cross-coupled inverters (SCIs) for complete TNU-recovery with area efficiency and low delay. To mitigate the issue that node-upset-recovery verifications for existing latches highly relies on electronic design automation tools, we further propose an algorithm-based verification method that can automatically verify the node-upset-recovery of latches, which greatly simplifies the reliability-verification flow. Simulation results demonstrate the TNU-recovery of HALTRAV and also show that HALTRAV achieves 40.38%, 8.17% and 31.89% reduction in delay, area and delay-power-area product (DPAP) on average, respectively; however; it is at the cost of power as compared to typical latches that are TNU-recoverable. Comparison results also demonstrate the moderate sensitivity of HALTRAV to the impacts of the process, voltage and temperature (PVT) variations
Covariate Model Selection Approaches for Population Pharmacokinetics: A Systematic Review of Existing Methods, From SCM to AI
No full textInternational audienceA growing number of covariate modeling methods have been proposed in the field of popPK modeling, but limited information exists on how they all compare. The objective of this study was to perform a systematic review of all popPK covariate modeling methods, focusing on assessing the existing knowledge on their performances. For each method of each article included in this review, evaluation setting, performance metrics along with their associated values, and relative computational times were reported when available. Evaluation settings report was done for uncertainty assessment of communicated results. Results showed that EBEs‐based ML methods stood out as the best covariate selection methods. AALASSO, a hybrid genetic algorithm, FREM with a clinical significance criterion and SCM+ with stagewise filtering were the best covariate model selection techniques—AALASSO being the very best one. Results also showed a lack of consensus on how to benchmark simulated datasets of different scenarios when evaluating method performances, but also on which metrics to use for method evaluation. We propose to systematically report TPR (sensitivity), FPR (Type I error), FNR (Type II error), TNR (specificity), covariate parameter error bias (MPE) and precision (RMSE), clinical relevance, and model fitness by means of BIC, concentration prediction error bias (MPE), and precision (RMSE) of new proposed methods and compare them with SCM. We propose to systematically combine covariate selection techniques to SCM or FFEM to allow for comparison with SCM. We also highlight the need for an open‐source benchmark of simulated datasets on a representative set of scenarios
Leftover Hash Lemma(s) Over Cyclotomic Rings
No full textIn this work, we propose a systematic approach for obtaining leftover hash lemmas (LHLs) over cyclotomic rings. Such LHLs build a fundamental tool in lattice-based cryptography, both in theoretical reductions as well as in the design of cryptographic primitives. The scattered set of prior works makes it difficult to navigate the landscape and requires a substantial effort to understand the mathematical constraints under which the LHL holds over cyclotomic rings. This is especially painful if one's given setting does not fit exactly into prior studies. We argue that all prior approaches boil down to two different proof strategies, resulting in two main theorems. From there on, we are able to recover all previous flavours of seemingly independent LHLs as corollaries. Moreover, we showcase the power of our interpretation by providing new statements, covering mathematical settings and concrete hash input distributions not considered before. Our work further proves LHLs in the presence of leakage for both approaches and provides novel bounds for wide families of leakage functions. We believe that our work will facilitate future uses of the LHL over cyclotomic rings, especially in the case of new algebraic and leakage settings
Integrating imprecise data in generative models using interval-valued Variational Autoencoders
No full textInternational audienceVariational Autoencoders (VAEs) enable the integration of diverse data sources into a unified latent representation, facilitating the fusion of information from various inputs and the creation of disentangled representations that separate different factors of variation in the data. Traditional VAEs, however, are limited by assuming a single prior distribution for latent variables, which restricts their ability to handle epistemic uncertainty from imprecise measurements and incomplete data. This paper introduces the Interval-Valued Variational Autoencoder (iVAE), which employs a family of prior distributions and incorporates specialized neurons and redefined objective functions for handling interval-valued data. This architecture maintains computational efficiency while extending the model’s applicability to scenarios with pronounced epistemic uncertainty. The iVAE’s efficacy is demonstrated in managing two types of data: intrinsically interval-valued and noisy data preprocessed into interval formats. The first category is exemplified by a graphical analysis of questionnaires, while the second involves case studies focused on estimating the remaining useful life of aviation engines, where the iVAE outperforms traditional methods, thereby providing more accurate diagnostics and robust predictions