Vérification efficace de systèmes en temps réel

Structural Variants (SVs) are genomic rearrangements of more than 50 base pairs. Since SVs can reach several thousand base pairs, they can have huge impacts on genome functions, studying SVs is, therefore, of great interest. Recently, a new generation of sequencing technologies has been developed and produce long read data of tens of thousand of base pairs which are particularly useful for spanning over SV breakpoints. So far, bioinformatics methods have focused on the SV discovery problem with long read data. However, no method has been proposed to specifically address the issue of genotyping SVs with long read data. The purpose of SV genotyping is to assess for each variant of a given input set which alleles are present in a newly sequenced sample. This thesis proposes a new method for genotyping SVs with long read data, based on the representation of each allele sequences. We also defined a set of conditions to consider a read as supporting an allele. Our method has been implemented in a tool called SVJedi. Our tool has been validated on both simulated and real human data and achieves high genotyping accuracy. We show that SVJedi obtains better performances than other existing long read genotyping tools and we also demonstrate that SV genotyping is considerably improved with SVJedi compared to other approaches, namely SV discovery and short read SV genotyping approaches.Les automates temporisés sont souvent utilisés pour modéliser des systèmes en temps réel. Le problème d'accessibilité est notamment étudié puisqu'il permet de vérifier des propriétés de sûreté mais aussi de générer des contrôleurs pour réaliser une tâche. Bien que ce problème soit déjà résolu depuis plus de 25 ans et implémenté dans plusieurs outils, nous proposons des algorithmes pour accélérer ces méthodes dans des cas particuliers. Pour le problème de sureté nous proposons des méthodes basées sur des abstractions de zones temporelles, surestimant les parties accessibles. Ces abstractions sont ensuite successivement raffinées grâce à une boucle CEGAR. Pour le problème de génération de contrôleur, nous proposons des algorithmes basées sur des exploration heuristiques et A*. Nous présentons aussi des implémentations de ces algorithmes, ainsi que des résultats sur des différents exemples