Made available in DSpace on 2014-12-17T15:48:09Z (GMT). No. of bitstreams: 1 SarahRRS_DISSERT.pdf: 1954614 bytes, checksum: ba3eee36fc3f3f1030a71fa2ad2f605a (MD5) Previous issue date: 2013-12-13 / Universidade Federal do Rio Grande do Norte / The component-based development of systems revolutionized the software development process, facilitating the maintenance, providing more confiability and reuse. Nevertheless, even with all the advantages of the development of components, their composition is an important concern. The verification through informal tests is not enough to achieve a safe composition, because they are not based on formal semantic models with which we are able to describe precisally a system s behaviour. In this context, formal methods provide ways to accurately specify systems through mathematical notations providing, among other benefits, more safety. The formal method CSP enables the specification of concurrent systems and verification of properties intrinsic to them, as well as the refinement among different models. Some approaches apply constraints using CSP, to check the behavior of composition between components, assisting in the verification of those components in advance. Hence, aiming to assist this process, considering that the software market increasingly requires more automation, reducing work and providing agility in business, this work presents a tool that automatizes the verification of composition among components, in which all complexity of formal language is kept hidden from users. Thus, through a simple interface, the tool BST (BRIC-Tool-Suport) helps to create and compose components, predicting, in advance, undesirable behaviors in the system, such as deadlocks / O desenvolvimento de sistemas baseados em componentes revolucionou o processo de desenvolvimento de software, facilitando a manuten??o, trazendo mais confiabilidade e reutiliza??o. Por?m, mesmo com todas as vantagens atribu?das ao componente, ? necess?rio uma an?lise detalhada de sua composi??o. Realizar verifica??o a partir de testes de software n?o ? o suficiente para se ter uma composi??o segura, pois esses n?o s?o baseados em modelos sem?nticos formais nos quais podemos descrever precisamente o comportamento do sistema. Nesse contexto, os m?todos formais oferecem a possibilidade de especificarmos sistemas de forma precisa, atrav?s de nota??es com forte base matem?tica, trazendo, entre outros benef?cios, mais seguran?a. O m?todo formal CSP possibilita a especifica??o de sistemas concorrentes e verifica??o de propriedades inerentes a tais sistemas, bem como refinamento entre diferentes modelos. Existem abordagens que aplicam restri??es usando CSP, para verificar o comportamento da composi??o entre componentes, auxiliando a verifica??o desses componentes antecipadamente. Visando auxiliar esse processo, tendo em vista que o mercado de software busca cada vez mais automa??o, minimizando trabalhos e trazendo agilidade nos neg?cios, este trabalho apresenta uma ferramenta que automatiza a verifica??o da composi??o entre componentes, onde o conjunto de verifica??es CSP impostas ? gerado e verificado internamente, oculto para o usu?rio. Dessa forma, atrav?s de uma interface simples, a ferramenta BTS (BRIC-Tool-Suport) ajuda a criar e compor componentes, prevendo, com anteced?ncia, comportamentos indesej?veis no sistema, como deadlocks

Les circuits microélectroniques récents intègrent des dizaines d'horloges afin d'optimiser leur consommation et leur performance. Le nombre de traversées de domaines d'horloges (CDC) et la complexité des systèmes augmentant, garantir formellement l'intégrité d'une donnée devient un défi majeur. Plusieurs problèmes sont alors soulevés : configurer le système dans un mode réaliste, décrire l'environnement par des hypothèses sur les protocoles, gérer l'explosion de l'espace des états, analyser les contre-exemples, ...La première contribution de cette thèse a pour but d'atteindre une configuration complète et réaliste du système. Nous utilisons de la vérification formelle paramétrique ainsi qu'une analyse de la structure du circuit afin de détecter automatiquement les composants des arbres d'horloge. La seconde contribution cherche à éviter l'explosion de l'espace des états en combinant des abstractions localisées du circuit avec une analyse de contre-examples. L'idée clé est d'utiliser la technologie de raffinement d'abstraction guidée par contre-exemple (CEGAR) où l'utilisateur influence la poursuite de l'algorithme en se basant sur des informations extraites des contre-exemples intermédiaires. La troisième contribution vise à créer des hypothèses pour des environnements sous-contraints. Tout d’abord, plusieurs contre-exemples sont générés pour une assertion, avec différentes raisons d’échec. Ensuite, des informations en sont extraites et transformées en hypothèses réalistes.Au final, cette thèse montre qu'une vérification formelle concluante peut être obtenue en combinant la rapidité de l'analyse structurelle avec l'exhaustivité des méthodes formelles. / Modern hardware designs typically comprise tens of clocks to optimize consumption and performance to the ongoing tasks. With the increasing number of clock-domain crossings as well as the huge complexity of modern SoCs, formally proving the functional integrity of data propagation became a major challenge. Several issues arise: setting up the design in a realistic mode, writing protocol assumptions modeling the environment, facing state-space explosion, analyzing counter-examples, ...The first contribution of this thesis aims at reaching a complete and realistic design setup. We use parametric liveness verification and a structural analysis of the design in order to identify behaviors of the clock and reset trees. The second contribution aims at avoiding state-space explosion, by combining localization abstractions of the design, and counter-example analysis. The key idea is to use counterexample-guided abstraction refinement as the algorithmic back-end, where the user influence the course of the algorithm based on relevant information extracted from intermediate abstract counterexamples. The third contribution aims at creating protocol assumptions for under-specified environments. First, multiple counter-examples are generated for an assertion, with different causes of failure. Then, information is mined from them and transformed into realistic protocol assumptions.Overall, this thesis shows that a conclusive formal verification can be obtained by combining inexpensive structural analysis along with exhaustive model checking.

Garantir la sécurité d’une application tout au long de son cycle de vie est une tâche fastidieuse. Le choix, l’implémentation et l’évaluation des solutions de sécurité est difficile et sujette a des erreurs. Les compétences en sécurité ne sont pas répondues dans toutes les équipes de développement. Afin de réduire ce manque de compétences en sécurité, les développeurs ont a leurs disposition une multitude de documents décrivant des problèmes de sécurité et des solutions requises (i.e., vulnérabilités, attaques, principes de sécurité, patrons sécurité, etc.). Abstraites et informelles, ces documents sont fournis par des sources différentes et leur nombre est en constante croissance. Les développeurs sont noyés dans une multitude de documents ce qui fait obstruction à leur capacité à choisir, implémenter et évaluer la sécurité d’une application. Cette thèse aborde ces questions et propose un ensemble de méthodes pour aider les développeurs à choisir, implémenter et évaluer les solutions de sécurité face aux problèmes de sécurité. Ces problèmes sont matérialisés par les failles, les vulnérabilités, les attaques, etc. et les solutions fournies par des patrons de sécurité. Cette thèse introduit en premier une méthode pour aider les développeurs dans l’implémentation de patrons de sécurité et l’estimation de leur efficacité face aux vulnérabilités. Puis elle présente trois méthodes associant les patrons de sécurité, les vulnérabilités, les attaques, etc. au sein d’une base de connaissance. Cette dernière permet une extraction automatique de classifications de patrons et améliore la rapidité et la précision des développeurs dans le choix des patrons de sécurité face à une vulnérabilité ou une attaque. En utilisant la base de connaissance, nous présentons une méthode pour aider les développeurs dans la modélisation des menaces ainsi que la générations et l’exécution des cas de test de sécurité. La méthode est évaluée et les résultats montrent que la méthode améliore l’efficacité, la compréhensibilité et la précision des développeurs dans le choix des patrons de sécurité et d’écriture des cas de test de sécurité. / Ensuring the security of an application through its life cycle is a tedious task. The choice, the implementation and the evaluation of security solutions is difficult and error prone. Security skills are not common in development teams. To overcome the lack of security skills, developers and designers are provided with a plethora of documents about security problems and solutions (i.e, vulnerabilities, attacks, security principles, security patterns, etc.). Abstract and informal, these documents are provided by different sources, and their number is constantly growing. Developers are drown in a sea of documentation, which inhibits their capacity to design, implement, and the evaluate the overall application security. This thesis tackles these issues and presents a set of approaches to help designers in the choice, the implementation and the evaluation of security solutions required to overcome security problems. The problems are materialized by weaknesses, vulnerabilities, attacks, etc. and security solutions are given by security patterns.This thesis first introduces a method to guide designers implement security patterns and assess their effectiveness against vulnerabilities. Then, we present three methods associating security patterns, attacks, weaknesses, etc. in a knowledge base. This allows automated extraction of classifications and help designers quickly and accurately select security patterns required to cure a weakness or to overcome an attack. Based on this nowledge base, we detaila method to help designers in threat modeling and security test generation and execution. The method is evaluated and results show that the method enhances the comprehensibility and the accuracy of developers in the security solutions choice, threat modeling and in the writing of security test cases.

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-29T18:03:18Z No. of bitstreams: 1 PAULO EDUARDO E SILVA BARBOSA - DISSERTAÇÃO PPGCC 2007..pdf: 549401 bytes, checksum: ffeac306fd7624758ab88a5062b5a5ae (MD5) / Made available in DSpace on 2018-08-29T18:03:18Z (GMT). No. of bitstreams: 1 PAULO EDUARDO E SILVA BARBOSA - DISSERTAÇÃO PPGCC 2007..pdf: 549401 bytes, checksum: ffeac306fd7624758ab88a5062b5a5ae (MD5) Previous issue date: 2007-02-23 / Todo programador ou engenheiro de software lida com um problema crônico na concepção de seus sistemas: violações das especificações ou requisitos de projeto. Essas violações necessitam de uma captura imediata, pois geralmente originam falhas que só podem ser descobertas tardiamente, a um custo de reparo bastante elevado. Nos últimos anos, pesquisadores da ciência da computação estão conseguindo um progressonotávelnodesenvolvimentodetécnicaseferramentasqueverificamautomaticamente requisitos e projeto. A abordagem em maior evidência chama-se verificação de modelos (model-checking). Verificação de modelos é uma técnica formal e algorítmica de se fazer verificação de propriedades de sistemas com um espaço de estados finito. Suas principais vantagens são o poder de automação e a qualidade dos resultados produzidos. Porém, esta técnica sofre de um problema fundamental — a explosão do espaço de estados — que se deve ao crescimento exponencial na estrutura que representa o comportamento de sistemas e à falta de recursos computacionais disponíveis para lidar com grandes quantidades de informação sobre o comportamento dos sistemas sob verificação. Este trabalho concentra-se em verificação de modelos utilizando plataformas de distribuição como tentativa de aliviar o problema citado. Mais detalhadamente, investigamos o uso de grades computacionais que rodam aplicações bag-of-tasks e formulamos algoritmos específicos para o processo de verificação. Aplicações bag-of-tasks são aplicações paralelas cujas tarefas são independentes entre si. Elas são as aplicações mais apropriadas para grades computacionais por permitirem heterogeneidade dos recursos. Aplicamos ferramentas de grades computacionais como uma camada entre a ferramenta de verificação e os recursos distribuídos compartilhados existentes e comparamos os quesitos desempenho e escala nos sistemas a serem verificados em relação às versões centralizadas de verificadores. A plataforma empregada na distribuição é muito atrativa no quesito custo, controle e escala. Através do compartilhamento de uma simples máquina, o engenheiro de sistemas ganha acesso a uma comunidade provedora de uma grande quantidade de recursos heterogêneos e automaticamente gerenciados para se fazer computação paralela seguindo sua filosofia. Durante o trabalho, essas vantagens são comparadas com suas desvantagens, como o alto custo de comunicação e a dificuldade de particionar o processo, por exemplo. O trabalho envolveu a produção das seguintes ferramentas: uma API genérica para a geração distribuída de grafos que representam o comportamento de sistemas concorrentes sobre plataformas de grades computacionais bag-of-tasks, um protótipo de verificação CTL que age de duas maneiras distintas, sendo on-the-fly durante a geração do espaço de estados ou sobre esse espaço de estados distribuído representado explicitamente seguindo a mesma filosofia de comunicação e versões simplificadas de simuladores de sistemas concorrentes sob alguns formalismos baseados em redes de Petri. Resultados experimentais sobre a aplicação deste ferramental são apresentados. / Every programmer or software engineer deals with a chronic problem during the conception of their systems: violations in the project requirements. These violations need to be discovered early be cause they generally produce errors that can be discovered later, at a very expensive cost to repair. In recent years, researchers in computer science are obtaining a notable progress in the development of techniques and tools to automatically verify requirements and designs. The most evidently approach is called model-checking. Model checking is a formal and algorithmic technique to perform properties verification in a finite state space of systems. Its main advantages are the automation power and the quality of the produced results. However this technique suffers from one big and foundamental problem - the state space explosion which is the absense of computational resources available today’s to deal with large amounts of information about the behavior of the systems under verification. This work investigates a solution to verify models in a distributed way using computational grids which runs bag-of-tasks applications, alleviating the mentioned problem. Bagof-tasks applications are those parallel applications which tasks arei ndependent of each other and are the applications most suited for computational grids because they allow heterogeneity between resources. We employ computational grid tools as a layer between between the verificationtooland the distributed shared resources. This verification is performed by adapted CTL algorithms to the bag-of-tasks philosophy. So we intend to obtain improvements in speed-up and scalability in the systems to be checked when compared to centralized versions of verifiers produced in side the group. Moreover,the employed middleware in the distribution is very attractive in the cost and control aspects. By sharing a single machine, the system engineer obtains access to a community that provides large amounts of heterogeneous resources automatically managed to perform parallel computation. This work included the production of the following tools: a generic API to the distributed generation of graphs that describes the behavior of concurrent systems under bag-of-tasks computational grids platforms, a prototype to check for CTL properties using on-the-fly algorithms or iterating over the generated fragments of the distributed graph. We also implemented simplified versions of simulators of concurrent systems following some formalisms based on Petri nets. Experimental results are also presented.

abstract: Although models for describing longitudinal data have become increasingly sophisticated, the criticism of even foundational growth curve models remains challenging. The challenge arises from the need to disentangle data-model misfit at multiple and interrelated levels of analysis. Using posterior predictive model checking (PPMC)—a popular Bayesian framework for model criticism—the performance of several discrepancy functions was investigated in a Monte Carlo simulation study. The discrepancy functions of interest included two types of conditional concordance correlation (CCC) functions, two types of R2 functions, two types of standardized generalized dimensionality discrepancy (SGDDM) functions, the likelihood ratio (LR), and the likelihood ratio difference test (LRT). Key outcomes included effect sizes of the design factors on the realized values of discrepancy functions, distributions of posterior predictive p-values (PPP-values), and the proportion of extreme PPP-values. In terms of the realized values, the behavior of the CCC and R2 functions were generally consistent with prior research. However, as diagnostics, these functions were extremely conservative even when some aspect of the data was unaccounted for. In contrast, the conditional SGDDM (SGDDMC), LR, and LRT were generally sensitive to the underspecifications investigated in this work on all outcomes considered. Although the proportions of extreme PPP-values for these functions tended to increase in null situations for non-normal data, this behavior may have reflected the true misfit that resulted from the specification of normal prior distributions. Importantly, the LR and the SGDDMC to a greater extent exhibited some potential for untangling the sources of data-model misfit. Owing to connections of growth curve models to the more fundamental frameworks of multilevel modeling, structural equation models with a mean structure, and Bayesian hierarchical models, the results of the current work may have broader implications that warrant further research. / Dissertation/Thesis / Doctoral Dissertation Educational Psychology 2015

Submitted by Miriam Lucas (miriam.lucas@unioeste.br) on 2018-02-22T14:23:15Z No. of bitstreams: 2 Felipe_Crestani_dos_Santos_2017.pdf: 5495370 bytes, checksum: 82f81445874bba45497cda5c8d784d2f (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2018-02-22T14:23:15Z (GMT). No. of bitstreams: 2 Felipe_Crestani_dos_Santos_2017.pdf: 5495370 bytes, checksum: 82f81445874bba45497cda5c8d784d2f (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2017-11-17 / The main line of research of this work is the study of approaches for supporting the development and analysis of the Power System Protection. In general, this process is carried out through of a large number of simulations involving various operating scenarios. The main limitation of this technique is the impossibility of coverage of all behavior of the system under analysis. In this context, this work proposes the use of Model Checking as a tool to support the procedure of development of power system protection schemes, principally in the sense of proving the security requirements and temporal deterministic expected behavior. Model Checking is a verification technique that explores exhaustively and automatically all possible system states, checking if this model meets a given specification. This work focuses on this two pillars of the Model Checking: to choose an appropriate modeling formalism for representation of the power system protection and how to describe the specification in temporal-logic for the verification process. With regard to the modeling formalism, the power system protection will be represented by the Hybrid Automata theory, while the verification tool adopted will be Statistical Model Checking, by the UPPAAL STRATEGO toolkit. It is underlined that this work is limited to the modeling of individual components of the power system protection, such that 18 models of the devices and protocols like communication bus (LAN), time synchronization protocol (PTP) and IEC 61850 communication protocols (SV and GOOSE) and Logical Nodes of power system protection, and 13 auxiliaries models, which emules the stochastic behavior to subsidise the verification process. The methodology of modelling adopted guarantees the effective representation of the components behaviour of power system protection. For this, the results of Model Checking process were compared with behavioral requirements defined by standards, conformance testings and paper related to the area. With regard to the contributions of this work, were identified three researches areas that could use the models developed in this work: i) implementation of power system protection schemes; ii) achievement of conformance testing; and iii) indication of the parameterization error of the power protection system scheme. / A linha de pesquisa abordada neste trabalho aponta para o estudo e desenvolvimento de ferramentas que subsidiem a proposição e validação de Sistemas de Proteção de Sistemas de Energia Elétrica. Em geral, este processo é realizado mediante simulações computacionais envolvendo diversos cenários de operação e distúrbios, tendo como principal limitação a impossibilidade de representar todos os caminhos de evolução do sistema em análise. Nesse contexto, propõe-se o emprego da técnica de Modelagem e Verificação Formal como ferramenta de suporte ao projeto, análise e implementação de estratégias de proteção, principalmente no sentido de comprovar se a estratégia atende os requisitos de segurança e comportamento determinístico temporal esperado. Em síntese, o método consiste na verificação de propriedades descritas em lógicas temporais, sob uma abstração apropriada (formalismo) do comportamento do sistema. Esta dissertação possui enfoque nestes dois requisitos: modelagem do sistema de proteção através de um formalismo adequado e tradução dos requisitos do comportamento desejado em propriedades descritas em lógica temporal. Com relação ao formalismo de apoio, a modelagem do sistema de proteção é baseada em uma abstração de Autômatos Temporizados Híbridos. Como ferramenta de validação, adota-se a técnica de Verificação Formal Estatística, através do software UPPAAL STRATEGO. Salienta-se que este trabalho se delimita apenas na modelagem e validação individual dos principais equipamentos de um sistema de proteção, sendo 18 modelos de dispositivos e protocolos como barramentos de comunicação (LAN), protocolo de sincronização de tempo PTP, protocolos de comunicação baseados em IEC 61850 e funções de proteção, e 13 modelos auxiliares que implementam um comportamento estocástico para subsidiar o processo de validação do sistema de proteção. O desenvolvimento dos modelos se deu através de uma abordagem sistemática envolvendo processos de simulação e verificação das propriedades sob o modelo em análise. Através desta metodologia, garante-se que os modelos desenvolvidos representam o comportamento esperado de seus respectivos dispositivos. Para isso, os resultados do processo de verificação foram comparados com requisitos comportamentais definidos por normas, testes de conformidade em equipamentos/protocolos e trabalhos acadêmicos vinculados à área. Com relação às contribuições do trabalho, identificou-se três linhas de pesquisa que podem fazer o uso dos modelos desenvolvidos: i) implementação de novas estratégias de proteção; ii) realização de testes de conformidade em equipamentos externos à rede de autômatos; e iii) indicação de erros de parametrização do sistema de proteção.

La programmation par contraintes offre des langages et des outils permettant de résoudre des problèmes à forte combinatoire et à la complexité élevée tels que ceux qui existent en vérification de programmes. Dans cette thèse nous résolvons deux familles de problèmes de la vérification de programmes. Dans chaque cas de figure nous commençons par une étude formelle du problème avant de proposer des modèles en contraintes puis de réaliser des expérimentations. La première contribution concerne un langage réactif synchrone représentable par une algèbre de diagramme de blocs. Les programmes utilisent des flux infinis et modélisent des systèmes temps réel. Nous proposons un modèle en contraintes muni d’une nouvelle contrainte globale ainsi que ses algorithmes de filtrage inspirés de l’interprétation abstraite. Cette contrainte permet de calculer des sur-approximations des valeurs des flux des diagrammes de blocs. Nous évaluons notre processus de vérification sur le langage FAUST, qui est un langage dédié à la génération de flux audio. La seconde contribution concerne les systèmes probabilistes représentés par des chaînes de Markov à intervalles paramétrés, un formalisme de spécification qui étend les chaînes de Markov. Nous proposons des modèles en contraintes pour vérifier des propriétés qualitatives et quantitatives. Nos modèles dans le cas qualitatif améliorent l’état de l’art tandis que ceux dans le cas quantitatif sont les premiers proposés à ce jour. Nous avons implémenté nos modèles en contraintes en problèmes de programmation linéaire en nombres entiers et en problèmes de satisfaction modulo des théories. Les expériences sont réalisées à partir d’un jeu d’essais de la bibliothèque PRISM. / Constraint programming offers efficient languages andtools for solving combinatorial and computationally hard problems such as the ones proposed in program verification. In this thesis, we tackle two families of program verification problems using constraint programming.In both contexts, we first propose a formal evaluation of our contributions before realizing some experiments.The first contribution is about a synchronous reactive language, represented by a block-diagram algebra. Such programs operate on infinite streams and model real-time processes. We propose a constraint model together with a new global constraint. Our new filtering algorithm is inspired from Abstract Interpretation. It computes over-approximations of the infinite stream values computed by the block-diagrams. We evaluated our verification process on the FAUST language (a language for processing real-time audio streams) and we tested it on examples from the FAUST standard library. The second contribution considers probabilistic processes represented by Parametric Interval Markov Chains, a specification formalism that extends Markov Chains. We propose constraint models for checking qualitative and quantitative reachability properties. Our models for the qualitative case improve the state of the art models, while for the quantitative case our models are the first ones. We implemented and evaluated our verification constraint models as mixed integer linear programs and satisfiability modulo theory programs. Experiments have been realized on a PRISM based benchmark.

Les travaux de cette thèse contribuent au développement de méthodes automatiques de vérification et de valida-tion de systèmes informatiques, à partir de modèles. Ils sont divisés en deux parties : vérification et générationde tests.Dans la partie vérification, pour le problème du model-checking régulier indécidable en général, deux nouvellestechniques d’approximation sont définies, dans le but de fournir des (semi-)algorithmes efficaces. Des sur-approximations de l’ensemble des états accessibles sont calculées, avec l’objectif d’assurer la terminaison del’exploration de l’espace d’états. Les états accessibles (ou des sur-approximations de cet ensemble d’états)sont représentés par des langages réguliers, ou automates d’états finis. La première technique consiste à sur-approximer l’ensemble des états atteignables en fusionnant des états des automates, en fonction de critèressyntaxiques simples, ou d’une combinaison de ces critères. La seconde technique d’approximation consisteaussi à fusionner des états des automates, mais à l’aide de transducteurs. De plus, pour cette seconde technique,nous développons une nouvelle approche pour raffiner les approximations, qui s’inspire du paradigme CEGAR(CounterExample-Guided Abstraction Refinement). Ces propositions ont été expérimentées sur des exemplesde protocoles d’exclusion mutuelle.Dans la partie génération de tests, une technique qui permet de combiner la génération aléatoire avec un critèrede couverture, à partir de modèles algébriques (des grammaires algébriques, des automates à pile) est définie.Générer les tests à partir de ces modèles algébriques (au lieu de le faire à partir de graphes) permet de réduirele degré d’abstraction du modèle et donc de générer moins de tests qui ne sont pas exécutables dans le systèmeréel. Ces propositions ont été expérimentées sur la grammaire de JSON (JAvaScript Object Notation), ainsi quesur des automates à pile correspondant à des appels de fonctions mutuellement récursives, à une requête XPath,et à l’algorithme Shunting-Yard. / The thesis contributes to development of automatic methods for model-based verification and validation ofcomputer systems. It is divided into two parts: verification and test generation.In the verification part, for the problem of regular model checking undecidable in general, two new approxi-mation techniques are defined in order to provide efficient (semi-)algorithms. Over-approximations of the setof reachable states are computed, with the objective of ensuring the termination of the exploration of the statespace. Reachable states (or over-approximations of this set of states) are represented by regular languages or,equivalently, by finite-state automata. The first technique consists in over-approximating the set of reachablestates by merging states of automata, based on simple syntactic criteria, or on a combination of these criteria.The second approximation technique also merges automata states, by using transducers. For the second tech-nique, we develop a new approach to refine approximations, inspired by the CEGAR paradigm (for Counter-Example-Guided Abstraction Refinement). These proposals have been tested on examples of mutual exclusionprotocols.In the test generation part, a technique that combines the random generation with coverage criteria, fromcontext-free models (context-free grammars, pushdown automata) is defined. Generate tests from these mo-dels (instead of doing from graphs) reduces the model abstraction level, and therefore allows having moretests executable in the real system. These proposals have been tested on the JSON grammar (JavaScript ObjectNotation), as well as on pushdown automata of mutually recursive functions, of an XPath query, and of theShunting-Yard algorithm.

Computer systems are used in almost all aspects of our lives and our dependency on them keeps on increasing. When computer systems are used to handle critical tasks, any software failure can cause severe human and/or material losses. Therefore, for such applications, it is important to detect software errors at an early stage of software development. Furthermore, the growing use of concurrent and distributed programs exponentially increases the complexity of computer systems, making the problem of detecting software errors even harder (if not impossible). This calls for defining systematic and efficient techniques to evaluate the safety and the correctness of programs. The aim of Model-Checking is to analyze automatically whether a given program satisfies its specification. Early applications of Model-Checking were restricted to systems whose behaviors can be captured by finite graphs, so called finite-state systems. Since many computer systems cannot be modeled as finite-state machines, there has been a growing interest in extending the applicability of Model-Checking to infinite-state systems. The goal of this thesis is to extend the applicability of Model Checking for three instances of infinite-state systems: Ad-Hoc Networks, Dynamic Register Automata and Multi Pushdown Systems. Each one of these instances models challenging types of networks of communicating processes. In both Ad-Hoc Networks and Dynamic Register Automata, communication is carried through message passing. In each type of network, a graph topology models the communication links between processes in the network. The graph topology is static in the case of Ad-Hoc Networks while it is dynamic in the case of Dynamic Register Automata. The number of processes in both types of networks is unbounded. Finally, we consider Multi Pushdown Systems, a model used to study the behaviors of concurrent programs composed of sequential recursive sequential programs communicating through a shared memory.

Cette thèse développe des techniques à base d'automates pour la vérification formelle de systèmes physiquement distribués communiquant via des canaux fiables de tailles non bornées. Chaque machine peut exécuter localement plusieurs programmes récursifs (multi-threading). Un programme récursif peut également utiliser pour ses calculs locaux des structures de données non bornées, comme des files ou des piles. Ces systèmes, utilisés en pratique, sont si puissants que tous leurs problèmes de vérification deviennent indécidables. Nous introduisons et étudions un nouveau paramètre, appelé largeur de coupe (split-width), pour l'analyse de ces systèmes. Cette largeur de coupe est définie comme le nombre minimum de scissions nécessaires pour partitioner le graphe d'une exécution en parties sur lesquelles on pourra raisonner de manière indépendante. L'analyse est ainsi réalisée avec une approche diviser pour régner. Lorsqu'on se restreint à la classe des comportements ayant une largeur de coupe bornée par une constante, on obtient des procédures de décision optimales pour divers problèmes de vérification sur ces systèmes tels que l'accessibilité, l'inclusion, etc. ainsi que pour la satisfaisabilité et le model checking par rapport à divers formalismes comme la logique monadique du second ordre, la logique dynamique propositionnelle et des logiques temporelles. On montre aussi que les comportements d'un système ont une largeur de coupe bornée si et seulement si ils ont une largeur de clique bornée. Ainsi, grâce aux résultats de Courcelle sur les graphes de degré uniformément borné, la largeur de coupe est non seulement suffisante, mais aussi nécessaire pour obtenir la décidabilité du problème de satisfaisabilité d'une formule de la logique monadique du second ordre. Nous étudions ensuite l'existence de contrôleurs distribués génériques pour nos systèmes distribués. Nous proposons plusieurs contrôleurs, certains ayant un nombre fini d'états et d'autres étant déterministes, qui assurent que les comportements du système sont des graphes ayant une largeur de coupe bornée. Un système ainsi contrôlé de manière distribuée hérite des procédures de décision optimales pour les différents problèmes de vérification lorsque la largeur de coupe est bornée. Cette classe décidable de système généralise plusieurs sous-classes décidables étudiées précédemment. / This thesis investigates automata-theoretic techniques for the verification of physically distributed machines communicating via unbounded reliable channels. Each of these machines may run several recursive programs (multi-threading). A recursive program may also use several unbounded stack and queue data-structures for its local-computation needs. Such real-world systems are so powerful that all verification problems become undecidable. We introduce and study a new parameter called split-width for the under-approximate analysis of such systems. Split-width is the minimum number of splits required in the behaviour graphs to obtain disjoint parts which can be reasoned about independently. Thus it provides a divide-and-conquer approach for their analysis. With the parameter split-width, we obtain optimal decision procedures for various verification problems on these systems like reachability, inclusion, etc. and also for satisfiability and model checking against various logical formalisms such as monadic second-order logic, propositional dynamic logic and temporal logics. It is shown that behaviours of a system have bounded split-width if and only if they have bounded clique-width. Thus, by Courcelle's results on uniformly bounded-degree graphs, split-width is not only sufficient but also necessary to get decidability for MSO satisfiability checking. We then study the feasibility of distributed controllers for our generic distributed systems. We propose several controllers, some finite state and some deterministic, which ensure that the behaviours of the system have bounded split-width. Such a distributedly controlled system yields decidability for the various verification problems by inheriting the optimal decision procedures for split-width. These also extend or complement many known decidable subclasses of systems studied previously.