<P align="justify">Model-checking is an automated technique which aims at verifying properties of computer systems. A model-checker is fed with a model of the system (which capture all its possible behaviors) and a property to verify on this model. Both are given by a convenient mathematical formalism like, for instance, a transition system for the model and a temporal logic formula for the property.</P> <P align="justify">For several reasons (the model-checking is undecidable for this class of model or the model-checking needs too much resources for this model) model-checking may not be applicable. For safety properties (which basically says "nothing bad happen"), a solution to this problem uses a simpler model for which model-checkers might terminate without too much resources. This simpler model, called the abstract model, over-approximates the behaviors of the concrete model. However the abstract model might be too imprecise. In fact, if the property is true on the abstract model, the same holds on the concrete. On the contrary, when the abstract model violates the property, either the violation is reproducible on the concrete model and so we found an error; or it is not reproducible and so the model-checker is said to be inconclusive. Inconclusiveness stems from the over-approximation of the concrete model by the abstract model. So a precise model yields the model-checker to conclude, but precision comes generally with an increased computational cost.</P> <P align="justify">Recently, a lot of work has been done to define abstraction refinement algorithms. Those algorithms compute automatically abstract models which are refined as long as the model-checker is inconclusive. In the thesis, we give a new abstraction refinement algorithm which applies for safety properties. We compare our algorithm with previous attempts to build abstract models automatically and show, using formal proofs that our approach has several advantages. We also give several extensions of our algorithm which allow to integrate existing techniques used in model-checking such as acceleration techniques.</P> <P align="justify">Following a rigorous methodology we then instantiate our algorithm for a variety of models ranging from finite state transition systems to infinite state transition systems. For each of those models we prove the instantiated algorithm terminates and provide encouraging preliminary experimental results.</P> <br> <br> <P align="justify">Le model-checking est une technique automatisée qui vise à vérifier des propriétés sur des systèmes informatiques. Les données passées au model-checker sont le modèle du système (qui en capture tous les comportements possibles) et la propriété à vérifier. Les deux sont donnés dans un formalisme mathématique adéquat tel qu'un système de transition pour le modèle et une formule de logique temporelle pour la propriété.</P> <P align="justify">Pour diverses raisons (le model-checking est indécidable pour cette classe de modèle ou le model-checking nécessite trop de ressources pour ce modèle) le model-checking peut être inapplicable. Pour des propriétés de sûreté (qui disent dans l'ensemble "il ne se produit rien d'incorrect"), une solution à ce problème recourt à un modèle simplifié pour lequel le model-checker peut terminer sans trop de ressources. Ce modèle simplifié, appelé modèle abstrait, surapproxime les comportements du modèle concret. Le modèle abstrait peut cependant être trop imprécis. En effet, si la propriété est vraie sur le modèle abstrait alors elle l'est aussi sur le modèle concret. En revanche, lorsque le modèle abstrait enfreint la propriété : soit l'infraction peut être reproduite sur le modèle concret et alors nous avons trouvé une erreur ; soit l'infraction ne peut être reproduite et dans ce cas le model-checker est dit non conclusif. Ceci provient de la surapproximation du modèle concret faite par le modèle abstrait. Un modèle précis aboutit donc à un model-checking conclusif mais son coût augmente avec sa précision.</P> <P align="justify">Récemment, différents algorithmes d'abstraction raffinement ont été proposés. Ces algorithmes calculent automatiquement des modèles abstraits qui sont progressivement raffinés jusqu'à ce que leur model-checking soit conclusif. Dans la thèse, nous définissons un nouvel algorithme d'abstraction raffinement pour les propriétés de sûreté. Nous comparons notre algorithme avec les algorithmes d'abstraction raffinement antérieurs. A l'aide de preuves formelles, nous montrons les avantages de notre approche. Par ailleurs, nous définissons des extensions de l'algorithme qui intègrent d'autres techniques utilisées en model-checking comme les techniques d'accélérations.</P> <P align="justify">Suivant une méthodologie rigoureuse, nous instancions ensuite notre algorithme pour une variété de modèles allant des systèmes de transitions finis aux systèmes de transitions infinis. Pour chacun des modèles nous établissons la terminaison de l'algorithme instancié et donnons des résultats expérimentaux préliminaires encourageants.</P>

<p>The complex behavior of computer systems offers many challenges for <i>formal verification</i>. The analysis quickly becomes difficult as the number of participating processes increases.</p><p>A <i>parameterized system</i> is a family of systems parameterized on a number <i>n</i>, typically representing the number of participating processes. The <i>uniform verification problem</i> — to check whether a property holds for each instance — is an infinite-state problem. The automated analysis of parameterized and infinite-state systems has been the subject of research over the last 15–20 years. Much of the work has focused on safety properties. Progress in verification of liveness properties has been slow, as it is more difficult in general.</p><p>In this thesis, we consider verification of parameterized and infinite-state systems, with an emphasis on liveness, in the verification framework called <i>regular model checking (RMC)</i>. In RMC, states are represented as words, sets of states as regular expressions, and the transition relation as a regular relation.</p><p>We extend the automata-theoretic approach to RMC. We define a <i>specification logic</i> sufficiently strong to specify systems representable using RMC, and linear temporal logic properties of such systems, and provide an automatic translation from a specification into an analyzable model.</p><p>We develop <i>acceleration techniques</i> for RMC which allow more uniform and automatic verification than before, with greater power. Using these techniques, we succeed to verify safety and liveness properties of parameterized protocols from the literature.</p><p>We present a novel <i>reachability based</i> verification method for verification of liveness, in a general setting. We implement the method for RMC, with promising results.</p><p>Finally, we develop a framework for the verification of dynamic networks based on graph transformation, which generalizes the systems representable in RMC. In this framework we verify the latest version of the DYMO routing protocol, currently being considered for standardization by the IETF.</p>

Since its introduction in 1999, bounded model checking (BMC) has quickly become a serious and indispensable tool for the formal verification of hardware designs and, more recently, software. By leveraging propositional satisfiability (SAT) solvers, BMC overcomes some of the shortcomings of more conventional model checking methods. In model checking we automatically verify whether a state transition system (STS) describing a design has some property, commonly expressed in linear temporal logic (LTL). BMC is the restriction to only checking the looping and non-looping runs of the system that have bounded descriptions. The conventional BMC approach is to translate the STS runs and LTL formulae into propositional logic and then conjunctive normal form (CNF). This CNF expression is then checked by a SAT solver. In this thesis we study the effect on the performance of BMC of changing the translation to propositional logic. One novelty is to use a normal form for LTL which originates in resolution theorem provers. We introduce the normal form conversion early on in the encoding process and examine the simplifications that it brings to the generation of propositional logic. We further enhance the encoding by specialising the normal form to take advantage of the types of runs peculiar to BMC. We also improve the conversion from propositional logic to CNF. We investigate the behaviour of the new encodings by a series of detailed experimental comparisons using both hand-crafted and industrial benchmarks from a variety of sources. These reveal that the new normal form based encodings can reduce the solving time by a half in most cases, and up to an order of magnitude in some cases, the size of the improvement corresponding to the complexity of the LTL expression. We also compare our method to the popular automata-based methods for model checking and BMC.

Estruturas de tratamento de exceção são extremamente comuns em softwares desenvolvidos em linguagens modernas, como Java, e afetam de forma contundente o comportamento de um software quando exercitadas. Apesar destas duas características, as principais técnicas de verificação, teste de software e verificação formal, e as ferramentas a elas vinculadas, tendem a negligenciar o comportamento excepcional. Alguns dos fatores que levam a esta negligência são a não especificação do comportamento excepcional em termos de projeto e a consequente implementação das estruturas de tratamento com base no julgamento individual de cada programador. Isto resulta na não consideração de partes expressivas do código em termos de verificação e, consequentemente, a possibilidade de não serem detectados erros relativos tanto às próprias estruturas de tratamento quanto às estruturas de código vinculadas a estas. A fim de abordar este problema, propomos uma técnica, baseada em model checking, que automatiza o processo de exercício de caminhos excepcionais. Isto permite que seja observado o comportamento de um software quando da ocorrência de uma exceção. Pretendemos, com esta técnica, dar suporte para que seja aplicado aos caminhos que representam o comportamento excepcional de um software as mesmas técnicas de detecção de erros que são aplicadas aos caminhos que representam o comportamento normal e, com isso, agregar um aumento na qualidade do desenvolvimento de software. / Software developed in modern languages, such as Java, commonly present structures of exception handling. These structures, when exercised, may affect the software behavior. Despite these two characteristics, the main verification techniques, software testing and formal verification and the tools related to them, tend to neglect the exceptional behavior. The nonexistent specification of software exceptional behaviors at the design level, and, the subsequent implementation of exception handling based on the judgment of each programmer, are some factors that lead to this neglect. These factors result in the non-consideration of the expressive parts of the code in verification terms and, consequently, the impossibility of errors detection concerning either the exception treatment structures or the code structures linked to them. Taking this fact into consideration, we propose a technique based on the model checking process, which automates the process of exercising exceptional paths to address this problem. This allows the observation of the software behavior when an exception occurs. With this technique, we intend to support the application of the same error detection techniques for program normal behavior paths to the paths that represent the software exceptional behavior. Therefore, using the proposed technique, we aim to increase the software development quality.

The complex behavior of computer systems offers many challenges for formal verification. The analysis quickly becomes difficult as the number of participating processes increases. A parameterized system is a family of systems parameterized on a number n, typically representing the number of participating processes. The uniform verification problem — to check whether a property holds for each instance — is an infinite-state problem. The automated analysis of parameterized and infinite-state systems has been the subject of research over the last 15–20 years. Much of the work has focused on safety properties. Progress in verification of liveness properties has been slow, as it is more difficult in general. In this thesis, we consider verification of parameterized and infinite-state systems, with an emphasis on liveness, in the verification framework called regular model checking (RMC). In RMC, states are represented as words, sets of states as regular expressions, and the transition relation as a regular relation. We extend the automata-theoretic approach to RMC. We define a specification logic sufficiently strong to specify systems representable using RMC, and linear temporal logic properties of such systems, and provide an automatic translation from a specification into an analyzable model. We develop acceleration techniques for RMC which allow more uniform and automatic verification than before, with greater power. Using these techniques, we succeed to verify safety and liveness properties of parameterized protocols from the literature. We present a novel reachability based verification method for verification of liveness, in a general setting. We implement the method for RMC, with promising results. Finally, we develop a framework for the verification of dynamic networks based on graph transformation, which generalizes the systems representable in RMC. In this framework we verify the latest version of the DYMO routing protocol, currently being considered for standardization by the IETF.

Un comportement distribué peut être décrit avec un multi-ensemble partiellement ordonné (pomset). Bien que compacts et très intuitifs, ces modèles sont difficiles à vérifier. La principale technique utilisée dans cette thèse est de ramener les problèmes de décision de la logique MSO sur les pomsets à des problèmes de décision sur les mots. Les problèmes considérés sont la satisfiabilité et la vérification. Le problème de la vérification pour une formule donnée et un pomset consiste à décider si une interprétation est vraie, et le problème de satisfiabilité consiste à décider si un pomset répondant à la formule existe. Le problème de satisfiabilité de MSO sur pomsets est indécidable. Une procédure de semi-décision peut apporter des solutions pour de nombreux cas, en dépit du fait qu'elle peut ne pas terminer. Nous proposons un nouveau modèle, que l'on appelle ⌈-Pomset, pouvant rendre l'exploration des pomsets possible. Par conséquent, si une formule est satisfiable alors notre approche mènera éventuellement à la détection d'une solution. De plus, en utilisant les ⌈-Pomsets comme modèles pour systèmes concurrents, le model-checking de formules ordre partiel sur systèmes concurrents est décidable. Certaines expérimentations ont été faites en utilisant l'outil MONA. Nous avons comparé aussi la puissance expressive de certains modèles classiques de la concurrence comme les traces de Mazurkiewicz avec les ⌈-Pomsets. / Multiset of partially ordered events (pomset) can describe distributed behavior. Although very intuitive and compact, these models are difficult to verify. The main technique used in this thesis is to bring back decision problems for MSO over pomsets to problems for MSO over words. The problems considered are satisfiability and verification. The verification problem for a formula and a given pomset consists in deciding whether such an interpretation exists, and the satisfiability problem consists in deciding whether a pomset satisfying the formula exists. The satisfiability problem of MSO over pomsets is undecidable. A semi-decision procedures can provide solutions for many cases despite the fact that they may not terminate. We propose a new model, so called ⌈-Pomset, making the exploration of pomsets space possible. Consequently, if a formula is satisfiable then our approach will eventually lead to the detection of a solution. Moreover, using ⌈-Pomsets as models for concurrent systems, the model checking of partial order formulas on concurrent systems is decidable. Some experiments have been made using MONA. We compare also the expressive power of some classical model of concurrency such as Mazurkiewicz traces with our ⌈-Pomsets.

Estruturas de tratamento de exceção são extremamente comuns em softwares desenvolvidos em linguagens modernas, como Java, e afetam de forma contundente o comportamento de um software quando exercitadas. Apesar destas duas características, as principais técnicas de verificação, teste de software e verificação formal, e as ferramentas a elas vinculadas, tendem a negligenciar o comportamento excepcional. Alguns dos fatores que levam a esta negligência são a não especificação do comportamento excepcional em termos de projeto e a consequente implementação das estruturas de tratamento com base no julgamento individual de cada programador. Isto resulta na não consideração de partes expressivas do código em termos de verificação e, consequentemente, a possibilidade de não serem detectados erros relativos tanto às próprias estruturas de tratamento quanto às estruturas de código vinculadas a estas. A fim de abordar este problema, propomos uma técnica, baseada em model checking, que automatiza o processo de exercício de caminhos excepcionais. Isto permite que seja observado o comportamento de um software quando da ocorrência de uma exceção. Pretendemos, com esta técnica, dar suporte para que seja aplicado aos caminhos que representam o comportamento excepcional de um software as mesmas técnicas de detecção de erros que são aplicadas aos caminhos que representam o comportamento normal e, com isso, agregar um aumento na qualidade do desenvolvimento de software. / Software developed in modern languages, such as Java, commonly present structures of exception handling. These structures, when exercised, may affect the software behavior. Despite these two characteristics, the main verification techniques, software testing and formal verification and the tools related to them, tend to neglect the exceptional behavior. The nonexistent specification of software exceptional behaviors at the design level, and, the subsequent implementation of exception handling based on the judgment of each programmer, are some factors that lead to this neglect. These factors result in the non-consideration of the expressive parts of the code in verification terms and, consequently, the impossibility of errors detection concerning either the exception treatment structures or the code structures linked to them. Taking this fact into consideration, we propose a technique based on the model checking process, which automates the process of exercising exceptional paths to address this problem. This allows the observation of the software behavior when an exception occurs. With this technique, we intend to support the application of the same error detection techniques for program normal behavior paths to the paths that represent the software exceptional behavior. Therefore, using the proposed technique, we aim to increase the software development quality.

EB-3 est un langage de spécification développé pour la spécification des systèmes d'information. Le noyau du langage EB-3comprend des spécifications d'algèbre de processus afin de décrire le comportement des entités du système et des fonctions d'attributs qui sont des fonctions récursives dont l'évaluation se fait sur la trace d'exécution du système décrivant les attributs des entités. La vérification de propriétés temporelles en EB-3 est un sujet de grande importance pour des utilisateurs de EB-3. Dans cette thèse, on se focalise sur les propriétés de vivacité concernant des systèmes d'information exprimant l'éventualité que certaines actions puissent s'exécuter. La vérification des propriétés de vivacité se fait à l'aide de model checking. Dans un premier temps, on présente une sémantique opérationnelle deEB-3, selon laquelle les fonctions d'attributs sont évaluées pendant l'exécution du programme puis stockées. Cette sémantique nous permet de définir une traduction automatique de EB-3 vers LNT, qui est un langage simultané enrichi d'une algèbre de processus. Notre traduction assure la correspondance un à un entre les états et les transitions des systèmes étiquetés de transition correspondent respectivement à des spécifications EB-3 et LNT. Ensuite, on automatise la traduction grâce à l'outil EB3toLNT fournissant aux utilisateurs de EB-3 une tous les outils de vérification fonctionnelle disponible dans CADP. Dans le but d'améliorer les résultats de notre approche concernant le model checking, on explore des techniques d'abstraction dédiées aux systèmes d'information spécifiées en EB-3. En particulier, on se focalise sur une famille spécifique de systèmes qui s'appellent paramétriques dont le comportement varie en fonction de la valeur prédéfinie d'un paramètre du système. Enfin, on applique cette méthode dans le contexte de EB-3 / EB-3 is a specification language for information systems. The core of the EB-3 language consists of process algebraic specifications describing the behaviour of entities in a system, and attribute functions that are recursive functions evaluated on the system execution trace describing entity attributes. The verification ofEB-3 specifications against temporal properties is of great interest to users of EB-3. In this thesis, we focus on liveness properties of information systems, which express the eventuality that certain actions take place. The verification of liveness properties can beachieved with model checking. First, we present an operational semantics for EB-3 programs, in which attribute functions are computed during program evolution and their values are stored into program memory. This semantics permits us to define an automatic translation from EB-3 to LNT, a value-passing concurrent language with classical process algebra features. Our translation ensures the one-to-one correspondence between states and transitions of the labelled transition systems corresponding to theEB-3 and LNT specifications. Then, we automate this translation with the EB-3toLNT tool, thus equipping the EB-3 method with the functional verification features available in the model checking toolbox CADP. With the aim of improving the model checking results of this approach, we explore abstraction techniques for information systems specified inEB-3. In particular, we concentrate on a specific family of systems called parametric, whose behaviour is scaled in keeping with the predefined value of a system parameter. Finally, we apply this method on the EB-3 context

Předkládaná práce se zabývá problémem automatizované syntézy pravděpodobnostních systémů: máme-li rodinu Markovských řetězců, jak lze efektivně identifikovat ten který odpovídá zadané specifikaci? Takové rodiny často vznikají v nejrůznějších oblastech inženýrství při modelování systémů s neurčitostí a rozhodování i těch nejjednodušších syntézních otázek představuje NP-těžký problém. V dané práci my zkoumáme existující techniky založené na protipříklady řízené induktivní syntéze (counterexample-guided inductive synthesis, CEGIS) a na zjemňování abstrakce (counterexample-guided abstraction refinement, CEGAR) a navrhujeme novou integrovanou metodu pro pravděpodobnostní syntézu. Experimenty nad relevantními modely demonstrují, že navržená technika je nejenom srovnatelná s moderními metodami, ale ve většině případů dokáže výrazně překonat, někdy i o několik řádů, existující přístupy.

L'injection de faute est une méthode bien connue pour évaluer la robustesse et détecter les vulnérabilités des systèmes. La détection des vulnérabilités créées par injection de fautes a été approchée par différentes méthodes. Dans la littérature deux approches existent: les approches logicielles et les approches matérielles. Les approches logicielles peuvent fournir une large et rapide couverture, mais ne garantissent pas la présence de vulnérabilité dans le système. Les approches matérielles sont incontestables dans leurs résultats, mais nécessitent l’utilisation de matériaux assez coûteux et un savoir-faire approfondi, qui ne permet tout de même pas dans la majorité des cas de confirmer le modèle de faute représentant l'effet créé. Dans un premier lieu, cette thèse se concentre sur l'approche logicielle et propose une approche automatisée qui emploie les techniques de la vérification formelle pour détecter des vulnérabilités créées par injection de faute au niveau binaire. L'efficacité de cette approche est montrée en l'appliquant à des algorithmes de cryptographie implémentés dans les systèmes embarqués. Dans un second lieu, cette thèse établit un rapprochement entre les deux approches logicielles et matérielles sur la détection de vulnérabilité d'injection de faute en comparant les résultats des expériences des deux approches. Ce rapprochement des deux approches démontre que: toutes les vulnérabilités détectées par l'approche logicielle ne peuvent pas être reproduites dans le matériel; les conjectures antérieures sur le modèle de faute par des attaques d'impulsion électromagnétique ne sont pas précises ; et qu’il y a un lien entre les résultats de l’approche logicielle et l'approche matérielle. De plus, la combinaison des deux approches peut rapporter une approche plus précise et plus efficace pour détecter les vulnérabilités qui peuvent être créées par injection de faute. / Fault injection is a well known method to test the robustness and security vulnerabilities of systems. Detecting fault injection vulnerabilities has been approached with a variety of different but limited methods. Software-based and hardware-based approaches have both been used to detect fault injection vulnerabilities. Software-based approaches can provide broad and rapid coverage, but may not correlate with genuine hardware vulnerabilities. Hardware-based approaches are indisputable in their results, but rely upon expensive expert knowledge, manual testing, and can not confirm what fault model represent the created effect. First, this thesis focuses on the software-based approach and proposes a general process that uses model checking to detect fault injection vulnerabilities in binaries. The efficacy and scalability of this process is demonstrated by detecting vulnerabilities in different cryptographic real-world implementations. Then, this thesis bridges software-based and hardware-based fault injection vulnerability detection by contrasting results of the two approaches. This demonstrates that: not all software-based vulnerabilities can be reproduced in hardware; prior conjectures on the fault model for electromagnetic pulse attacks may not be accurate; and that there is a relationship between software-based and hardware-based approaches. Further, combining both software-based and hardware-based approaches can yield a vastly more accurate and efficient approach to detect genuine fault injection vulnerabilities.