Les techniques formelles de la famille « vérification de modèles » (« model checking ») se heurtent au problème de l’explosion combinatoire. Ceci limite les perspectives d’exploitation dans des projets industriels. Ce problème est provoqué par la combinatoire dans la construction de l’espace des états possibles durant l’exécution des systèmes modélisés. Le nombre d’états pour des modèles de systèmes industriels réalistes dépasse régulièrement les capacités des ressources disponibles en calcul et stockage. Cette thèse défend l’idée qu’il est possible de réduire cette combinatoire en spécialisant les outils pour des familles de propriétés. Elle propose puis valide expérimentalement un ensemble de méthodes pour le développement de ce type d’outils en suivant une approche guidée par les propriétés appliquée au contexte temps réel. Il s’agit donc de construire des outils d’analyse performants pour des propriétés temps réel qui soient exploitables pour des modèles industriels de taille réaliste. Les langages considérés sont, d’une part UML étendu par le profil MARTE pour la modélisation par les utilisateurs, et d’autre part les réseaux de Petri temporisés comme support pour la vérification. Les propositions sont validées sur un cas d’étude industriel réaliste issu du monde avionique : l’étude de la latence et la fraicheur des données dans un système de gestion des alarmes exploitant les technologies d’Avionique Modulaire Intégrée. Ces propositions ont été mise en oeuvre comme une boite à outils qui intègre les cinq contributions suivantes: la définition de la sémantique d’exécution spécifiques aux propriétés temps réel pour les modèles d’architecture et de comportement spécifiés en UML/MARTE; la spécification des exigences temps réel en s’appuyant sur un ensemble de patrons de vérification atomiques dédiés aux propriété temps réel; une méthode itérative d’analyse à base d’observateurs pour des réseaux de Petri temporisés; des techniques de réduction de l’espace d’états spécifiques aux propriétés temps réel pour des Réseaux de Petri temporisés; une approche pour l’analyse des erreurs détectées par « vérification des modèles » en s’appuyant sur des idées inspirées de la « fouille de données » (« data mining »). / Automatic formal verification such as model checking faces the combinatorial explosion issue. This limits its application in indus- trial projects. This issue is caused by the explosion of the number of states during system’s execution , as it may easily exceed the amount of available computing or storage resources. This thesis designs and experiments a set of methods for the development of scalable verification based on the property-driven approach. We propose efficient approaches based on model checking to verify real-time requirements expressed in large scale UML-MARTE real-time system designs. We rely on the UML and its profile MARTE as the end-user modeling language, and on the Time Petri Net (TPN) as the verification language. The main contribution of this thesis is the design and implementation of a property-driven verification prototype toolset dedicated to real-time properties verification for UML-MARTE real-time software designs. We validate this toolset using an avionic use case and its user requirements. The whole prototype toolset includes five contributions: definition of real-time property specific execution semantics for UML-MARTE architecture and behavior models; specification of real- time requirements relying on a set of verification dedicated atomic real- time property patterns; real-time property specific observer-based model checking approach in TPN; real-time property specific state space reduction approach for TPN; and fault localization approach in model checking.

Les systèmes temps réel (STR) sont au coeur de machines souvent jugés critiques pour lasécurité : ils en contrôlent l’exécution afin que celles-ci se comportent de manière sûre dans le contexte d’un environnement dont l’évolution peut être imprévisible. Un STR n’a d’autre alternative que de s’adapter à son environnement : sa correction dépend des temps de réponses aux stimuli de ce dernier.Il est couramment admis que le formalisme des réseaux de Petri temporels (RdPT) est adapté àla description des STR. Cependant, la modélisation de systèmes simples, ne possédant que quelquestˆaches périodiques ordonnancées de façon basique se révèle être un exercice souvent complexe.En premier lieu, la modélisation efficace d’une gamme étendue de politiques d’ordonnancementsse heurte à l’incapacité des RdPT à imposer un ordre d’apparition à des évènements concurrentssurvenant au même instant. D’autre part, les STR ont une nette tendance à être constitués de caractéristiques récurrentes, autorisant une modélisation par composants. Or les RdPT ne sont guèreadaptés à une utilisation compositionnelle un tant soit peu générale. Afin de résoudre ces deuxproblèmes, nous proposons dans cette thèse Cifre – en partenariat entre Airbus et le Laas-Cnrs– d’étendre les RdPT à l’aide de deux nouvelles relations, les relations d’inhibition et de permission,permettant de spécifier de manière plus fine les contraintes de temps.Afin de cerner un périmètre clair d’adéquation de cette nouvelle extension à la modélisation dessystèmes temps réel, nous avons défini Pola, un langage spécifique poursuivant deux objectifs :déterminer un sous-ensemble des systèmes temps réel modélisables par les réseaux de Petri temporelsà inhibitions/permissions et fournir un langage simple à la communauté temps réel dont lavérification, idéalement automatique, est assurée par construction. Sa sémantique est donnée par traduction en réseaux de Petri temporels à inhibitions/permissions. L’explorateur d’espace d’états de laboite à outils Tina a été étendu afin de permettre la vérification des descriptions Pola / Real time systems (RTS) are at the core of safety critical devices : they control thedevices’ behavior in such a way that they remain safe with regard to an unpredictable environment. ARTS has no other choices than to adapt to its environment : its correctness depends upon its responsetime to the stimuli stemming from the environment.It is widely accepted that the Time Petri nets (TPN) formalism is adapted to the description ofRTS. However, the modeling of simple systems with only a few periodic tasks scheduled according toa basic policy remains a challenge in the worst case and can be very tedious in the most favorable one.First, we put forward some limitations of TPN regarding the modeling of a wide variety of schedulingpolicies, coming from the fact that this formalism is not always capable to impose a givenorder on events whenever they happen at the same time. Moreover, RTS are usually constituted of thesame recurring features, implying a compositional modeling, but TPN are not well adapted to sucha compositional use. To solve those problems we propose in this Cifre thesis – in partnership withAirbus and the Laas-Cnrs – to extend the formalism with two new dual relations, the forbid andallow relations so that time constraints can be finely tuned.Then, to assess this new extension for modeling of real time systems, we define Pola, a specificlanguage aimed at two goals : to determine a subset of RTS which can be modeled with forbid/allowtime Petri nets and to provide a simple language to the real time community which, ideally, can bechecked automatically. Its semantics is given by translation into forbid/allow Time Petri nets. Thestate space exploration tool of the Tina toolbox have been extended so that it can model check Poladescriptions.

Les logiciels embarqués critiques de contrôle-commande sont soumis à des contraintes fortes englobant le déterminisme, la correction logique et la correction temporelle. Nous supposons que les spécifications sont exprimées à l'aide du langage formel de description d'architectures logicielles temps réel multipériodiques Prelude. L'objectif de cette thèse est, à partir d'un programme Prelude ou d'un ensemble de tâches temps réel dépendantes, de générer un code multithreadé exécutable sur une architecture multicœur tout en respectant la sémantique initiale. Pour cela, nous avons développé une boîte à outil, SchedMCore,permettant : - d'une part, la vérification formelle de l'ordonnançabilité. La vérification proposée est basée sur le parcours exhaustif du comportement avec pas de temps discret. Il est alors possible d'analyser des politiques en-ligne (FP, gEDF, gLLF et LLREF) mais également de calculer une affectation de priorité fixe valide et une séquence valide hors-ligne.- d'autre part, l'exécution multithreadée sur une cible multicœur. L'exécutif encode les politiques proposées étudiées dans la partie d'analyse d'ordonnançabilité, à savoir les quatre politiques en-ligne ainsi que les séquences valides générées. L'exécutif permet 3 modes d'utilisation, allant de la simulation temporelle à l'exécution temps précis des comportements des tâches. Il est compatible Posix et facilement portable sur divers OS. / A real-time control-command embedded system is subject to strong constraints such as determinism, logical and temporal correctness. We assume that the specifications are expressed using the formal software architecture description language Prelude, dedicated to real-time multiperiodic applications. The goal of this thesis is, given a Prelude program or dependent real-time taskset, to generate amultithreaded executable code over a multicore architecture while respecting the original semantic. To do so we have developed a toolbox, SchedMcore, that allows: - the formal verification of schedulability. The verification is based on the exhaustive exploration of the behaviour with a discret time frame. It is possible to analyse on-line policies (FP, gEDF, gLLF et LLREF), as well as to compute a fixed valid priority assignment and a valid off-line sequence.- the multithreaded execution over a multicore target. The framework encodes the same policies as those studied in the first part (the four on-line policies and the generated sequences). The framework provides three usage modes, from temporal simulation to time accurate execution. The executive is compatible with Posix and easily portable on several OS.

L'étude des grands modèles de réseaux biologiques par l'utilisation d'outils d'analyse et de simulation conduit à un grand nombre de prédictions. Cela soulève la question de savoir comment identifier les prédictions intéressantes de nouveaux phénomènes, qui peuvent être confrontés à des données expérimentales. Les techniques de vérification formelle basées sur le model checking constituent une technologie puissante pour faire face à cette augmentation d'échelle et de complexité pour l'analyse de ces réseaux. L'application de ces techniques est par contre difficile, pour plusieurs raisons. Premièrement, le domaine de la biologie des systèmes a mis en évidence quelques propriétés dynamiques du réseau, comme la multi-stabilité et les oscillations, qui ne sont pas facilement exprimables avec les logiques temporelles classiques. Deuxièmement, la difficulté de poser des questions pertinentes et intéressantes en logique temporelle est difficile pour les utilisateurs non-experts. Enfin, la plupart des modèles existants et des outils de simulation ne sont pas capables d'appliquer des techniques de model checking d'une manière transparente. La mise en œuvre des approches développées dans ce travail contribue à enlever des obstacles pour l'utilisation de la technologie de vérification formelle en biologie. Leur application a été validée sur l'analyse et la simulation de deux modèles biologiques complexes. / The study of large models of biological networks by means of analysis and simulation tools leads to large amounts of predictions. This raises the question of how to identify interesting predictions of novel phenomena that can be confronted with experimental data. Formal verification techniques based on model-checking have recently been used to the analysis of these networks, providing a powerful technology to keep up with this increase in scale and complexity. The application of these techniques is hampered, however, by several key issues. First, the systems biology domain brought to the fore a few properties of the network dynamics like multistability and oscillations, that are not easily expressed using classical temporal logics. Second, the problem of posing relevant and interesting questions in temporal logic, is difficult for non-expert users. Finally, most of the existing modeling and simulation tools are not capable of applying model-checking techniques in a transparent way. The approaches developed in this work lower the obstacles to the use of formal verification in systems biology. They have been validated on the analysis and simulation of two real and complex biological models. / O estudo de redes biológicas tem originado o desenvolvimento de modelos cada vez mais complexos e detalhados. O estudo de redes biológicas complexas utilizando ferramentas de análise e simulação origina grandes quantidades de previsões. Isto levanta a questão de como identificar previsões interessantes de novos fenómenos que possam ser comparados com dados experimentais. As técnicas de verificação formal baseadas em model-checking têm sido usadas na análise destas redes, fornecendo uma tecnologia poderosa para acompanhar o aumento de escala e complexidade do problema. A aplicação destas técnicas tem sido dificultada por um conjunto importante de factores. Em primeiro lugar, em biologia de sistemas têm sido tratadas diversas questões acerca da dinâmica da rede, como a multi-estabilidade e oscilações, que não são facilmente expressas usando lógicas temporais clássicas. Em segundo lugar, o problema de como elaborar perguntas relevantes em lógica temporal, é difícil para o utilizador comum. Por último, a maioria das ferramentas de modelação e simulação não estão preparadas para a aplicação de técnicas de model-checking de forma transparente. Os métodos desenvolvidos nesta tese aliviam os obstáculos no uso da verificação formal em biologia de sistemas. Estes métodos foram validados através da análise e simulação de dois modelos biológicos complexos.

Made available in DSpace on 2015-04-11T14:03:20Z (GMT). No. of bitstreams: 1 HERBERT OLIVEIRA.pdf: 512075 bytes, checksum: acc5d05442df938abdfa025f9db23367 (MD5) Previous issue date: 2011-02-04 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The use of computer-based systems in several domains has increased significantly over the last years, one of the main challenges in software development of these systems is to ensure the correctness and reliability of these. So that software verification now plays an important role in ensuring the overall product quality, aimed mainly the characteristics of predictability and reliability. In the context of software verification, with respect to the use of model checking technique, Bounded Model Checkers have already been applied to discover subtle errors in actual systems projects, contributing effectively in this verification process. The value of the counterexample and safety properties generated by Bounded Model Checkers to create test case and to debug these systems is widely recognized. When a Bounded Model Checking (BMC) finds an error it produces a counterexample. Thus, the value of counterexamples to debug software systems is widely recognized in the state-of-the-practice. However, BMCs often produce counterexamples that are either large or difficult to be understood and manipulated mainly because of both the software size and the values chosen by the respective solver. In this work we aim to demonstrate and analyze the use of formal methods (through using the model checking technique) in the process of developing programs in C language, exploring the features already provided by the model checking as the counterexample and the identification and verification of safety properties. In view of this we present two approaches: (i) we describe a method to integrate the bounded model checker ESBMC with the CUnit framework. This method aims to extract the safety properties generated by ESBMC to generate automatically test cases using the rich set of assertions provided by the CUnit framework and (ii) a method aims to automate the collection and manipulation of counterexamples in order to instantiate the analised C program for proving the root cause of the identified error. Such methods may be seen as a complementary technique for the verification performed by BMCs. We show the effectiveness of our proposed method over publicly available benchmarks of C programs. / A utilização de sistemas baseados em computador em diversos domínios aumentou significativamente nos últimos anos. Um dos principais desafios no desenvolvimento de software de sistemas críticos é a garantia da sua correção e confiabilidade. Desta forma, a verificação de software exerce um papel importante para assegurar a qualidade geral do produto, visando principalmente características como previsibilidade e confiabilidade. No contexto de verificação de software, os Bounded Model Checkers estão sendo utilizados para descobrir erros sutis em projetos de sistemas de software atuais, contribuindo eficazmente neste processo de verificação. O valor dos contra-exemplos e propriedades de segurança gerados pelo Bounded Model Checkers para criar casos de testes e para a depuração de sistemas é amplamente reconhecido. Quando um Bounded Model Checking (BMC) encontra um erro ele produz um contra-exemplo. Assim, o valor dos contra-exemplos para depuração de software é amplamente reconhecido no estado da prática. Entretanto, os BMCs frequentemente produzem contra-exemplos que são grandes ou difíceis de entender ou manipular, principalmente devido ao tamanho do software e valores escolhidos pelo solucionador de satisfabilidade. Neste trabalho visamos demonstrar e analisar o uso de método formal (através da técnica model checking) no processo de desenvolvimento de programas na linguagem C, explorando as características já providas pelo model checking como o contra-exemplo e a identificação e verificação de propriedades de segurança. Em face disto apresentamos duas abordagens: (i) descrevemos um método para integrar o Bounded Model Checker ESBMC como o framework de teste unitário CUnit, este método visa extrair as propriedades geradas pelo ESBMC para gerar automaticamente casos de teste usando o rico conjunto de assertivas providas pelo framework CUnit e (ii) um método que visa automatizar a coleta e manipulação dos contra-exemplos, de modo a instanciar o programa C analisado, para comprovar a causa raiz do erro identificado. Tais métodos podem ser vistos como um método complementar para a verificação efetuada pelos BMCs. Demonstramos a eficácia dos métodos propostos sobre benchmarks públicos de código C.

Submitted by Wagner Junior (wagner.junior@unioeste.br) on 2018-11-30T17:04:04Z No. of bitstreams: 2 Claudia_Beatriz_Bozz_2018.pdf: 4791914 bytes, checksum: 0affba2e984ec7e6beefa83d0c3bdfeb (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2018-11-30T17:04:04Z (GMT). No. of bitstreams: 2 Claudia_Beatriz_Bozz_2018.pdf: 4791914 bytes, checksum: 0affba2e984ec7e6beefa83d0c3bdfeb (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2018-07-26 / Real time systems that have continuous behavior associated with discrete elements are called hybrid systems. Among them, in this master’s research, a hydraulic system has been chosen as an object of study in order to perform the reliability analysis of it through modeling and formal verification. Much as several models for the reliability analysis of complex systems have been proposed in the literature, most of them are not suitable to represent the system when its behavior needs to be expressed by means of continuous variables, like the case of hybrid systems. Generally, simulation and experimental testing are used to analyze systems, and they give only approximate results from a large amount of samples. To eliminate the limitations of these techniques, the formal verification is an effective alternative, since it is characterized by performing a sweep in all possible states of the system automatically, verifying the behavior as a whole. The UPPAAL STRATEGO toolkit for modelling by stochastic hybrid automata and model checking has been used in this work, both classic formal verification and statistical formal verification. A benckmark has been used as object of study. Initially, the system has been modelling and its behavior (physical and controlled) verified through simulation and formal verification (property specification and model checking). The reliability parameters obtained in the statistical analysis of the system failures have been compared with results of literature, presenting a dispersion less than 2.5%, so it can be verify that the methodology used and the models constructed were adequate to analyze the reliability of this system hybrid.In a second step of this work, the probability distribution of failure of the components have been modified, in order to become the system more reliable with real hydraulic systems, and estimate the optimum mean time between maintenance (MTBM) of this system. Thus, it’s possible to conclude that the methodology is adequate to perform the reliability analysis of the hydraulic system, being that model checking is effective to estimate the reliability parameters of the hydraulic system. / Sistemas de tempo real que possuem comportamento contínuo associado com elementos de características discretas são chamados de sistemas híbridos. Dentre estes, nesta pesquisa de mestrado, optou-se pelo emprego de um sistema hidráulico como objeto de estudo a fim de realizar a análise de confiabilidade do mesmo a partir de modelagem e verificação formal. Por mais que diversos modelos para a análise de confiabilidade de sistemas complexos tenham sido propostos na literatura, a maioria não são adequados para representar sistemas em que o comportamento é expresso em variáveis contínuas, como é o caso dos sistemas híbridos. De modo geral, para a análise de sistemas, a simulação e os testes experimentais são comumente utilizados, e geram apenas resultados aproximados a partir de uma grande quantidade de amostras. Para eliminar as limitações destas técnicas, a verificação formal é uma alternativa eficaz, visto que é caracterizada por realizar uma varredura em todos os estados possíveis do sistema de forma automática, verificando o comportamento como um todo do mesmo. Neste trabalho, foi utilizada a ferramenta computacional UPPAAL STRATEGO para a modelagem por autômatos estocásticos híbridos e verificação dos modelos, tanto verificação formal clássica como estatística. Um modelo padrão (benchmark) foi utilizado como objeto de estudo. Inicialmente o sistema foi modelado e seu comportamento (físico e controlado) verificado através da simulação e verificação formal (especificação de propriedades e verificação de modelos). Os parâmetros de confiabilidade obtidos na análise estatística de falha do sistema foram comparados com outros existentes na literatura, apresentado uma dispersão inferior a 2,5%, logo pôde se verificar que a metodologia empregada e os modelos construídos foram adequados para análise de confiabilidade deste sistema hibrido. Em uma segunda etapa do trabalho, foi modificada a distribuição de probabilidade de falha dos componentes, a fim de tornar o sistema mais fidedigno com sistemas hidráulicos reais, e estimar o tempo médio entre manutenções (MTBM – Mean Time Between Maintenance) ideal deste sistema. Portanto, conclui-se que a metodologia empregada foi adequada para realizar a análise de confiabilidade do sistema hidráulico, sendo efetivo levantar os parâmetros de confiabilidade através da verificação de modelos.

La gestion de l'évolution des processus métier exige une compréhension approfondie des cause des changements, de leurs niveaux d'application ainsi que de leurs impacts sur le reste du système. Dans cette thèse, nous proposons une approche de gestion et de contrôle de l'éolution des processus métier permettant d'analyser ces changements et de comprendre leurs impacts. Cela assistera les concepteurs et les chargés de l'évolution des processus métier à établir une évaluation a priori de l'impact pour réduire les risques et les coûts liés à ces changements et d'améliorer le service et la qualité des processus métier. Ce travail consiste à proposer un ensemble de contributions permettant une vérification de la cohérence et de la conformité des modèles de processus métier après chaque changement, mais aussi d'établir une éaluation a priori de l'impact structurel et qualificatif des modifications. Les différentes approches proposées sont en cours d'expérimentation et de validation à travers le développement d'une plate-forme basée sur l'environnement Eclipse / The evolution management of the business processes requires an exhaustive understanding of the change. An evolution engineer needs to understand reasons of a change, its application levels, and subsequently its impact on the whole system. In this thesis, we propose an approach for an a priori change impact analysis, to better control the business process evolution. This may help the business experts and the process designers to evaluate change impact in order to reduce the associated risks and estimate the related costs. It may also help to improve the service and quality of the business processes. This work contributes an eventual improvement, in regard, to verify the coherence and the compliance of the business process models, after each change. It leads to evaluate an a priori change impact analysis in structural and qualitatie aspects. The multiple-perspectives of the proposed approach have been reviewed experimentally. The validation of the approach is evaluated by exteding the Eclipse Development Environment, with the help of a set of plug-ins, as a prototype plate-form.

Ce travail appartient au domaine de la simulation numérique sur des plates-formes d'exécution distribuées hétérogènes telles que des grilles de calcul. Ce type de plate-forme se caractérise par des possibles changements de condition d'exécution et par une probabilité importante de défaillance de certains composants. Une application qui s'exécute dans un tel environnement se doit d'être adaptable à son contexte d'exécution et tolérante aux pannes. Face à la complexité croissante de la mise en place de cas de calcul sur des grilles de calcul, nous proposons une plateforme logicielle pour la résolution de cas de calcul numérique dans un environnement distribué hétérogène. Nos travaux apportent une solution qui se base sur un système d'agents mobiles, ce qui permet à une application de s'adapter au changement de son environnement d'exécution. Dans un premier temps, nous utilisons le langage pi calcul d'ordre supérieur pour spécifier une « ferme de travailleurs » capable de participer à la résolution de tout type de cas de calcul. Ensuite, nous énonçons des propriétés qui caractérisent le bon fonctionnement de ce système avec une logique temporelle TCTL. Pour cela, nous souhaitons modéliser notre système à l'aide d'automates temporisés à partir des termes définis par la spécification formelle en pi calcul. Dans ce but, nous définissons une transformation de termes écrits en pi calcul en automates temporisés. Les propriétés sont alors vérifiées avec l'outil UppAal. Pour valider ce travail de modélisation, nous avons réalisé le framework MCA (pour Mobile Computing Architecture). Celui-ci propose un ensemble d'outils facilitant la mise en place de composants sur un environnement distribué hétérogène dans le but d'effectuer la résolution de cas de calcul. La librairie avec laquelle sont développés ces composants, qu'ils soient mobiles ou non, est implantée en Java et se base les technologies Jini et JavaSpaces. Enfin, nous réalisons l'évaluation du framework MCA en procédant à la résolution de trois cas de calcul différents. Chacune de ces expériences, réalisées sur une grappe de 20 noeuds, nous permet de montrer les caractéristiques essentielles de notre framework : une simplicité de programmation, un faible surcoût en temps d'exécution sans l'activation de la tolérance aux pannes et une tolérance aux pannes efficace / This work belongs to the domain of numerical simulation on heterogeneous distributed platforms such as grids. This type of platform is characterized by possible changes in execution conditions and a significant probability of some components failure. An application running in such an environment must be adaptable to its execution context and fault tolerant. Facing the growing complexity of implementing computation cases on grid computing, we propose a software platform which solves numerical computation cases in a distributed heterogeneous environment. Our work provides a solution based on a mobile agent system, which allows an application to adapt to change in its execution environment. At first, we use the higher-order pi calculus language to specify a « farm of workers » able to take part in solving any type of computation case. Then we set the properties that characterize the system's correct execution with a temporal logic TCTL. In order to do this, we perform a temporal modeling system based on terms defined by the formal specification in pi calculus. To achieve this transformation, we define a translation of terms written in pi calculus into timed automata. The properties are verified with the UppAal tool. To validate this modeling work, we develop the MCA (for Mobile Computing Architecture) framework. It offers a set of tools which facilitate the implementation of distributed heterogeneous components in order to solve computation cases. These components, mobile or not, are developed with a library written in Java and which uses Jini and JavaSpaces technologies. Finally, our framework is evaluated through the resolution of three different computation cases. Each of these experiments, performed on a 20 node cluster allow us to highlight our framework's main characteristics : programming simplicity, low overhead in execution time without the fault tolerance activation and efficient fault tolerance

Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.

Nous proposons de nouveaux algorithmes et de nouvelles structures de données pour la vérification formelle de systèmes réactifs finis sur architectures parallèles. Ces travaux se basent sur les techniques de vérification model checking. Notre approche cible des architectures multi-processeurs et multi-cœurs, avec mémoire partagée, qui correspondent aux générations de serveurs les plus performants disponibles actuellement.Dans ce contexte, notre objectif principal est de proposer des approches qui soient à la fois efficaces au niveau des performances, mais aussi compatibles avec les politiques de partage dynamique du travail utilisées par les algorithmes de génération d’espaces d'états en parallèle; ainsi, nous ne plaçons pas de contraintes sur la manière dont le travail ou les données sont partagés entre les processeurs.Parallèlement à la définition de nouveaux algorithmes de model checking pour machines multi-cœurs, nous nous intéressons également aux algorithmes de vérification probabiliste. Par probabiliste, nous entendons des algorithmes de model checking qui ont une forte probabilité de visiter tous les états durant la vérification d’un système. La vérification probabiliste permet des gains importants au niveau de la mémoire utilisée, en échange d’une faible probabilité de ne pas être exhaustif; il s’agit donc d’une stratégie permettant de répondre au problème de l’explosion combinatoire / In this thesis, we propose and study new algorithms and data structures for model checking finite-state, concurrent systems. We focus on techniques that target shared memory, multi-cores architectures, that are a current trend in computer architectures.In this context, we present new algorithms and data structures for exhaustive parallel model checking that are as efficient as possible, but also ``friendly'' with respect to the work-sharing policies that are used for the state space generation (e.g. a work-stealing strategy): at no point do we impose a restriction on the way work is shared among the processors. This includes both the construction of the state space as the detection of cycles in parallel, which is is one of the key points of performance for the evaluation of more complex formulas.Alongside the definition of enumerative, model checking algorithms for many-cores architectures, we also study probabilistic verification algorithms. By the term probabilistic, we mean that, during the exploration of a system, any given reachable state has a high probability of being checked by the algorithm. Probabilistic verification trades savings at the level of memory usage for the probability of missing some states. Consequently, it becomes possible to analyze part of the state space of a system when there is not enough memory available to represent the entire state space in an exact manner