Software testing is complex and time consuming. One way to reduce the effort associated with testing is to generate test data automatically. This thesis is divided into three parts. In the first part a mixed-integer constraint solver developed by Gupta et. al is studied. The solver, referred to as the Unified Numerical Approach (una), is an important part of their generator and it is responsible for solving equation systems that correspond to the program path currently under test. In this thesis it is shown that, in contrast to traditional optimization methods, the una is not bounded by the size of the solved equation system. Instead, it depends on how the system is composed. That is, even for very simple systems consisting of one variable we can easily get more than a thousand iterations. It is also shown that the una is not complete, that is, it does not always find a mixed-integer solution when there is one. It is found that a better approach is to use a traditional optimization method, like the simplex method in combination with branch-and-bound and/or a cutting-plane algorithm as a constraint solver. The second part explores a specification-based approach for generating tests developed by Meudec. Tests are generated by partitioning the specification input domain into a set of subdomains using a rule-based automatic partitioning strategy. An important step of Meudec’s method is to reduce the number of generated subdomains and find a minimal partition. This thesis shows that Meudec’s minimal partition algorithm is incorrect. Furthermore, two new efficient alternative algorithms are developed. In addition, an algorithm for finding the upper and lower bound on the number of subdomains in a partition is also presented. Finally, in the third part, two different designs of automatic testing tools are studied. The first tool uses a specification as an oracle. The second tool, on the other hand, uses a reference program. The fault-detection effectiveness of the tools is evaluated using both randomly and systematically generated inputs.

Software testing remains one of the most important but expensive approaches to ensure high-quality software today. In order to reduce the cost of testing, over the last several decades, various techniques such as formal verification and inductive learning have been used for test automation in previous research. In this thesis, we present a specification-based black-box testing approach, learning-based testing (LBT), which is suitable for a wide range of systems, e.g. procedural and reactive systems. In the LBT architecture, given the requirement specification of a system under test (SUT), a large number of high-quality test cases can be iteratively generated, executed and evaluated by means of combining inductive learning with constraint solving. We apply LBT to two types of systems, namely procedural and reactive systems. We specify a procedural system in Hoare logic and model it as a set of piecewise polynomials that can be locally and incrementally inferred. To automate test case generation (TCG), we use a quantifier elimination method, the Hoon-Collins cylindric algebraic decomposition (CAD), which is applied on only one local model (a bounded polynomial) at a time. On the other hand, a reactive system is specified in temporal logic formulas, and modeled as an extended Mealy automaton over abstract data types (EMA) that can be incrementally learned as a complete term rewriting system (TRS) using the congruence generator extension (CGE) algorithm. We consider TCG for a reactive system as a bounded model checking problem, which can be further reformulated into a disunification problem and solved by narrowing. The performance of the LBT frameworks is empirically evaluated against random testing for both procedural and reactive systems (executable models and programs). The results show that LBT is significantly more efficient than random testing in fault detection, i.e. less test cases and potentially less time are required than for random testing. / QC 20111012

Network systems often contain vulnerabilities that remain unmitigated in a network for various reasons, such as lack of a patch and limited budget. Adversaries can exploit these existing vulnerabilities through different strategies. The attackers can use the existing vulnerabilities to gain capabilities that will enable them to reach their target goal. This thesis aims to find the most effective defense strategy that can defend against all discovered/known attack scenarios in attempt to secure the system's critical assets. Threat modeling is a well-known technique to find and assess vulnerabilities and threats in the system. Attack graphs are one of the common models used to illustrate and analyze attack scenarios. They provide a logical overview that illustrates how an attacker can combine multiple vulnerabilities to reach a specific part of the system. This project utilizes attack graphs, taking advantage of the causal relationship of their elements to formulate a Constraint Solving Problem, performs a number of analyses to define some constraints and objectives to select the most appropriate actions to be taken by the defender. This is achieved by addressing the security requirements and organization requirements for a given budget. The results show that the selected combination of countermeasures restricts all attack paths presented in the Logical attack graph. The countermeasures are be distributed on the most critical parts of a system and reduce the potential harm for several vulnerabilities rather than provide high protection to a few vulnerabilities. This approach aids in finding the most relevant way to protect system's assets based on the available budget.

La sécurité des Systèmes d’Information (SI) constitue un défi majeur car elle conditionne amplement la future exploitation d’un SI. C’est pourquoi l’étude des vulnérabilités d’un SI dès les phases conceptuelles est cruciale. Il s’agit d’étudier la validation de politiques de sécurité, souvent exprimées par des règles de contrôle d’accès, et d’effectuer des vérifications automatisées sur des modèles afin de garantir une certaine confiance dans le SI avant son opérationnalisation. Notre intérêt porte plus particulièrement sur la détection des vulnérabilités pouvant être exploitées par des utilisateurs internes afin de commettre des attaques, appelées attaques internes, en profitant de leur accès légitime au système. Pour ce faire, nous exploitons des spécifications formelles B générées, par la plateforme B4MSecure, à partir de modèles fonctionnels UML et d’une description Secure UML des règles de contrôle d’accès basées sur les rôles. Ces vulnérabilités étant dues à l’évolution dynamique de l’état fonctionnel du système, nous proposons d’étudier l’atteignabilité des états, dits indésirables, donnant lieu à des attaques potentielles, à partir d’un état normal du système. Les techniques proposées constituent une alternative aux techniques de model-checking. En effet, elles mettent en œuvre une recherche symbolique vers l’arrière fondée sur des approches complémentaires : la preuve et la résolution de contraintes. Ce processus de recherche est entièrement automatisé grâce à notre outil GenISIS qui a montré, sur la base d’études de cas disponibles dans la littérature, sa capacité à retrouver des attaques déjà publiées mais aussi des attaques nouvelles. / The early detection of potential threats during the modelling phase of a Secure Information System (IS) is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during the system execution. This involves studying the validation of access control rules and performing vulnerabilities automated checks before the IS operationalization. We are particularly interested in detecting vulnerabilities that can be exploited by internal trusted users to commit attacks, called insider attacks, by taking advantage of their legitimate access to the system. To do so, we use formal B specifications which are generated by the B4MSecure platform from UML functional models and a SecureUML modelling of role-based access control rules. Since these vulnerabilities are due to the dynamic evolution of the functional state, we propose to study the reachability of someundesirable states starting from a normal state of the system. The proposed techniques are an alternative to model-checking techniques. Indeed, they implement symbolic backward search algorithm based on complementary approaches: proof and constraint solving. This rich technical background allowed the development of the GenISIS tool which automates our approach and which was successfully experimented on several case studies available in the literature. These experiments showed its capability to extract already published attacks but also new attacks.

De nos jours, les workflows sont largement utilisés par les entreprises et les organisations en vue d’améliorer l’efficacité organisationnelle, la réactivité et la rentabilité en gérant les tâches et les étapes de processus opérationnels. La vérification des spécifications est devenue obligatoire afin d’assurer que ces processus sont correctement conçus et atteignent le niveau de confiance et de qualité attendu.Dans ce contexte, cette thèse porte sur la vérification de spécifications modales – comportements nécessaires ou recevables impliquant plusieurs activités et leurs causalités – de workflows nets – une classe de réseaux de Petri adaptés à la description de workflows. En particulier, cette thèse définit un cadre novateur permettant de modéliser les exécutions de workflow nets,avec ou sans données, et de vérifier des spécifications modales à l’aide de systèmes de contraintes. Elle présente également deux méthodes de réduction préservant la "generalised soundness" et la validité d’une spécification modale donnée. Ces méthodes de réduction sont ensuite présentées comme des étapes de prétraitement réduisant la taille des workflow nets, de sorte que la vérification des propriétés conservées puisse être effectuée sur de plus petites instances. Enfin, cette thèse présente les outils qui ont été mis en oeuvre ainsi que des expérimentations qui ont été menées sur un grand nombre de workflows industriels afin de valider les approches proposées dans cette thèse. Ces résultats expérimentaux convaincants mettent en évidence l’efficacité, l’efficience et le passage à l’échelle de la méthode vérification de spécification modales ainsi que des méthodes de réduction introduites dans cette thèse. / Nowadays workflows are extensively used by companies and organisations in order to improve organizationaleffciency, responsiveness and profitability by managing the tasks and steps of business processes. Theverification of specifications has become mandatory to ensure that such processes are properly designedand reach the expected level of trust and quality. In this context, this thesis addresses the verification ofmodal specifications – necessary or admissible behaviour involving several activities and their causalities –of workflow nets – a Petri nets class suited for the description of workflows.In particular, it defines an innovative constraint system based framework to model executions of ordinary as wellas coloured workflow nets, and verify modal specifications. Further, it presents powerful reduction methodspreserving properties of interest such as generalised soundness and correctness of a given modal specification.Such reduction methods are then portrayed as pre-processing steps reducing workflow nets size, so that theverification of preserved properties can be carried out on smaller instances.Finally, as a practical contribution, this thesis introduces the tools that have been implemented as well asexperimentations that have been carried out over industrial workflow nets in order to validate the approachesproposed in this thesis. The convincing experimental results highlight the effectiveness, effciency andscalability of the modal specification verification method and reduction methods introduced in this thesis.

Avec des motivations venant du domaine de la Vérification, nous définissons une notion de WQO effectifs pour lesquels il est possible de représenter les ensembles clos et de calculer les principales opérations ensemblistes sur ces représentations. Dans une première partie, nous montrons que de nombreuses constructions naturelles sur les WQO préservent notre notion d'effectivité, prouvant ainsi que la plupart des WQOs utilisés en pratique sont effectifs. Cette partie est basée sur un article non publié dont Jean Goubault-Larrecq, Narayan Kumar, Prateek Karandikar et Philippe Schnoebelen sont co-auteurs.Dans une seconde partie, nous étudions les conséquences qu'a notre notion sur la logique du première ordre interprété sur un WQO. Bien que le fragment existentiel positif soit décidable pour tous les WQOs effectif, les perspectives de généralisation sont limitées par le résultat suivant: le fragment existentiel de la logique du première ordre sur les mots finis, ordonnés par plongement, est déjà indécidable. Ce résultat a été publié à LICS 2017 avec Philippe Schnoebelen et Georg Zetzsche. / With motivations coming from Verification, we define a notionof effective WQO for which it is possible to represent closed subsetsand to compute basic set-operations on these representations. In a firstpart, we show that many of the natural constructions that preserve WQOsalso preserve our notion of effectiveness, proving that a large class ofcommonly used WQOs are effective. This part is based on an unpublishedarticle with Jean Goubault-Larrecq, Narayan Kumar, Prateek Karandikarand Philippe Schnoebelen.In a second part, we investigate the consequences of our notion onfirst-order logics over WQOs. Although the positive existential fragmentis decidable for any effective WQO, the perspective of extension tolarger fragments is hopeless since the existential fragment is alreadyundecidable for the first-order logic over words with the subwordordering. This last result has been published in LICS 2017 with PhilippeSchnoebelen and Georg Zetzsche.

Made available in DSpace on 2014-06-12T15:51:39Z (GMT). No. of bitstreams: 2 arquivo2757_1.pdf: 5759741 bytes, checksum: 8075c58c36a6d409b242f2a7873fb02f (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Vitorino dos Santos Filho, Jairson; Pierre Louis Robin, Jacques. CHROME: a model-driven component-based rule engine. 2009. Tese (Doutorado). Programa de Pós-Graduação em Ciência da Computação, Universidade Federal de Pernambuco, Recife, 2009.

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.

Ce document présente l'étude de plusieurs modèles de machines à états finis qui étendent tous le même formalisme: les automates d'arbres classiques, et leur application dans différentes tâches telles que l'analyse statique de programmes ou de systèmes, la typage, la vérification de la cohérence de spécifications, le model checking... Les arbres sont une structure naturelle de données, très répandue en informatique, par exemple pour la représentation des structures de données hiérarchiques ou imbriquées, pour des algorithmes spécifiques (arbres binaires de recherche, algorithmes distribués), comme modèle abstrait pour des données semi-structurées utilisées pour l'échange d'information dans le Web, pour une présentation algébrique de processus récursifs, comme les termes en logique... Lorsqu'il s'agit de raisonner sur des systèmes manipulant des arbres, ou modelisés par des arbres, il est crucial d'avoir une représentation finie d'ensembles infinis d'arbres. Les automates d'arbres sont des machines à états finis permettant une telle représentation. Ils ont fait la preuve de leur adéquation à des tâches de raisonnement: ils ont un modèle théorique bien établi, en étroite relation avec la logique, ils bénéficient de bonnes propriétés de composition et d'algorithmes de décision efficaces. En particulier, les automates d'arbres sont utilisées au coeur de systèmes de vérification formelle d'outils de déduction automatique. Toutefois, les automates d'arbres ont des limitations sévères en expressivité. Par exemple, ils sont incapables de faire du filtrage non-linéaire ou d'exprimer des contraintes d'intégrité tels que les clés dans les bases de données. Certaines extensions ont été proposées afin d'améliorer le modèle en essayant de conserver de bonnes propriétés. Nous présentons dans ce document de plusieurs de telles extensions, leurs propriétés et leur utilisation en vérification symbolique de systèmes et de programmes.