Techn. University, Diss., 2006--München.

This study deals primarily with the efforts of Great Britain to bring the Italian-Ethiopian War to a halt through the Hoare-Laval peace plan of December 10, 1935. Based on memoirs, diaries, and public documents, this study is devoted to an examination of the reasons, both internal and external that formulated British foreign policy toward the war.

No description available.

En informatique comme dans de multiples autres domaines, les graphes peuvent être trouvés partout. Ils sont utilisés pour représenter des données dans des domaines allant de la chimie à l'architecture, en tant que structures abstraites ou que modèles des données et de leurs évolutions. Dans tous ces domaines, il est prévisible que les graphes évoluent au cours du temps suite à des réactions chimiques, une mise à jour des connaissance ou l'exécution d'un programme. Être capable de traiter ces transformations est une tâche particulièrement importante et difficile. Dans ce travail, notre objectif est d'étudier la vérification de telles transformations de graphes, c'est à dire comment prouver qu'une transformation de graphes est correcte. La correction d'une transformation est plus précisément définie comme la correction d'une spécification pour cette transformation contenant en plus une précondition et une postcondition. Nous avons décidé d'utiliser un calcul à la Hoare générant une plus faible précondition pour une postcondition et une transformation. Si cette plus faible précondition est impliquée par la précondition, la spécification est correcte. Nous avons choisi une approche plus algorithmique pour les transformation de graphes utilisant des actions atomiques. Nous définissons deux moyens de construire des transformations de graphes: en utilisant un langage impératif ou en utilisant des systèmes de règles de réécriture. Le principal ingrédient est la logique qui est choisie pour représenter la précondition, la postcondition et les possibles conditions internes. Pour que la logique puisse interagir avec le calcul, nous demandons que le problème de décision soit décidable, qu'elle soit fermée par substitutions et qu'elle soit capable d'exprimer l'existence ou l'absence d'un sous-graphe affecté par la transformation. Le résultat central de ce travail est l'identification et l'explication de ces conditions. / In computer science as well as multiple other fields, graphs have become ubiquitous. They are used to represent data in domains ranging from chemistry to architecture, as abstract structures or as models of the data or its evolution. In all these domains, graphs are expected to evolve over time due to chemical reactions, update of the knowledge or programs. Being able to deal with such transformations is an extremely important and difficult task. In this work, our aim is to study the verification of such graph transformation, that is how to prove that a graph transformation is correct. Correctness of a graph transformation is more precisely defines as correctness of a specification for the transformation containing additionally a precondition and a postcondition. We decided to use a Hoare-like calculus generating the weakest precondition for a postcondition and a transformation. If this weakest precondition is implied by the actual precondition, the specification is correct. We chose a more algorithmic approach to graph transformation by using atomic actions.We chose to define two ways to build graph transformations: using an imperative programming language and using rule-base rewriting systems. The main ingredient of the verification of graph transformation is the logic that is chosen to represent the precondition, the postcondition and the possible conditions internal to the transformation. So that the logic can interact with the calculus, we require that the decision problem be decidable, that the logic be closed under the substitutions introduced by the Hoare-like calculus and that it has to be able to express the existence and absence of a match for the transformation. The core result of this work is the identification and explanation of these conditions.

Les travaux de cette thèse ont pour cadre la vérification formelle, et plus spécifiquement le projet ANR Blanc CLIMT (Categorical and Logical Methods in Model Transformation) dédié aux grammaires de graphes. Ce projet, qui a démarré en février 2012 pour une durée de 48 mois, a donné lieu à la définition du langage Small-tALC, bâti sur la logique de description ALCQI. Ce langage prend la forme d’un DSL (Domain Specific Language) impératif à base de règles, chacune dérivant structurellement un graphe. Le langage s’accompagne d’un composant de preuve basé sur la logique de Hoare chargé d’automatiser le processus de vérification d’une règle. Cependant, force est de constater que tous les praticiens ne sont pas nécessairement familiers avec les méthodes formelles du génie logiciel et que les transformations sont complexes à écrire. En particulier, ne disposant que du seul prouveur, il s’agit pour le développeur Small-tALC d’écrire un triplet de Hoare {P} S {Q} et d’attendre le verdict de sa correction sous la forme d’un graphe contre-exemple en cas d’échec. Ce contre-exemple est parfois difficile à décrypter, et ne permet pas de localiser aisément l’erreur au sein du triplet. De plus, le prouveur ne valide qu’une seule règle à la fois, sans considérer l’ensemble des règles de transformation et leur ordonnancement d’exécution. Ce constat nous a conduits à proposer un environnement d’assistance au développeur Small-tALC. Cette assistance vise à l’aider à rédiger ses triplets et à prouver ses transformations, en lui offrant plus de rétroaction que le prouveur. Pour ce faire, les instructions du langage ont été revisitées selon l’angle ABox et TBox de la logique ALCQI. Ainsi, conformément aux logiques de description, la mise à jour du graphe par la règle s’assimile à la mise à jour ABox des individus (les nœuds) et de leurs relations (les arcs) d’un domaine terminologique TBox (le type des nœuds et les étiquettes des arcs) susceptible d’évoluer. Les contributions de cette thèse concernent : (1) un extracteur de préconditions ABox à partir d’un code de transformation S et de sa postcondition Q pour l’écriture d’une règle {P} S {Q} correcte par construction, (2) un raisonneur TBox capable d’inférer des propriétés sur des ensembles de nœuds transformés par un enchaînement de règles {Pi} Si {Qi}, et (3) d’autres diagnostics ABox et TBox sous la forme de tests afin d’identifier et de localiser des problèmes dans les programmes. L’analyse statique du code de transformation d’une règle, combinée à un calcul d’alias des variables désignant les nœuds du graphe, permet d’extraire un ensemble de préconditions ABox validant la règle. Les inférences TBox pour un enchaînement de règles résultent d’une analyse statique par interprétation abstraite des règles ABox afin de vérifier formellement des états du graphe avant et après les appels des règles. A ces deux outils formels s’ajoutent des analyseurs dynamiques produisant une batterie de tests pour une règle ABox, ou un diagnostic TBox pour une séquence de règles / The overall context of this thesis is formal verification, and more specifically the ANR Blanc CLIMT project (Categorical and Logical Methods in Model Transformation) dedicated to graph grammars. This project, which started in February 2012 for 48 months, gave rise to the development of the Small- tALC language, a graph transformation language based on the ALCQI description logic. This language takes the form of an imperative DSL (Domain Specific Language) based on rules; from each rule structurally derives a graph. It goes with a proof component based on Hoare's logic designed to automate the process of rule verification. However, it must be assumed that not all developers are familiar with formal methods of software engineering, and that graph transformations are complex to write. In particular, using exclusively the prover, the Small- tALC developer must write a Hoare triple {P} S {Q} and wait for the feedback in the form of a counterexample graph in case of failure. This counter-example is sometimes difficult to interpret, and so it does not allow to easily locate the error within the triple. Moreover, the prover validates only one rule at once, without considering all the transformation rules and their execution order. This fact led us to propose an assistance framework for Small- tALC to help developers write their triples and prove their transformations, providing them more feedback than the prover does. To this purpose, the Small- tALC instructions have been reviewed according to the ABox and TBox aspects of the ALCQI logic. Thus, in accordance with description logics, updating the graph by the rule corresponds to the ABox updating of individuals (nodes) and their relationships (edges) of a TBox terminology domain (nodes concepts and edges labels) that is also expected to evolve. The contributions of this thesis concern: (1) an ABox precondition extractor from a transformation code S and its post-condition Q in order to produce a correct by construction rule {P} S {Q}, (2) a TBox reasoner to infer properties on sets of nodes transformed by a rule sequence {Pi} Si {Qi}, and (3) other ABox and TBox diagnostics based on tests to identify and locate errors in programs. The static analysis of the code of a transformation rule, combined with an alias calculus of the variables that can not designate the same nodes of the graph, allows to extract a set of ABox preconditions validating the rule. TBox inferences related to a sequence of rules result from a static analysis by abstract interpretation of the ABox rules. These inferences formally check graph states before and after rule calls. Beside these two formal tools, the framework features dynamic analyzers that produce test cases for an ABox rule, or a TBox diagnosis for a sequence of rules

No description available.

La modélisation de systèmes biologiques est devenue indispensable pour comprendre les phénomènes complexes et émergents issus d'influences partiellement connues, et pour envisager de contrôler un système altéré dans le but de restaurer un comportement physiologique. Tout modèle, quel que soit son paradigme sous-jacent, fait intervenir des paramètres gouvernant sa dynamique mais les mesures expérimentales ne permettent généralement pas de les identifier et cela reste l'un des problèmes majeurs de la modélisation. Cette thèse propose une méthode automatique d'identification des paramètres dynamiques de systèmes biologiques dans un cadre de modélisation hybride. Le cadre hybride choisi découpe l'espace des phases selon l'activité des entités biologiques, et associe à chacun de ces sous-espaces une vitesse d'évolution de chacun des composants. Nous proposons une logique de Hoare en temps continu ainsi qu'un calcul de plus faible précondition qui, à partir d'observations expérimentales qualitatives et chronométriques, construit les contraintes minimales sur les paramètres du modèle pour qu’il soit compatible avec les observations. Ce calcul mène à un problème de satisfaction de contraintes sur les réels et nous montrons que celui-ci peut être résolu par le solveur AbSolute.Le prototype Holmes BioNet développé au cours de cette thèse peut non seulement automatiser le processus d'identification des valeurs des paramètres à partir des observations expérimentales, mais aussi simuler l'évolution du modèle obtenu afin de le comparer avec les traces expérimentales. Nous utilisons ce prototype pour modéliser le couplage des cycles cellulaire et circadien. / Modelling biological systems has become instrumental to understand complex and emerging phenomena resulting from partially known influences, and to consider controlling an altered system in order to restore a physiological behaviour. Any model, independent of the underlying paradigm, involves parameters governing its dynamics. However, experimental measurements generally do not allow their identification and this remains one of the major problems of modelling. This PhD proposes an automatic method for identifying the dynamic parameters of biological systems in a hybrid modelling framework. The chosen hybrid framework splits the phase space according to the activity of the biological entities, and associates to each of these subspaces a celerity for each of the components. We introduce a continuous time Hoare logic as well as its weakest precondition calculus which, from qualitative and chronometrical experimental observations, constructs the minimum constraints on the model parameters making it compatible with the observations. This calculus leads to a Constraint Satisfaction Problem on real numbers and we show that it can be solved by the AbSolute solver.The Holmes BioNet prototype developed during this PhD can not only automate the parameter identification process from experimental data, but also simulate the evolution of the obtained model in order to compare it with experimental traces. We use this prototype to model the coupling of the cellular and circadian cycles.

This thesis explores synergies between deductive verification and model checking, by using the existing model checker TriCera to automatically infer specifications for the deductive verifier Frama-C. To accomplish this, a formal semantics is defined for a subset of ANSI C, extended with assume statements, called Csmall. Then, it is shown how a Hoare logic contract can be translated into statements in Csmall, and the defined formal semantics is used to prove that the translation is correct. Furthermore, it is shown that the translation can be applied also to a real specification language. This is done by defining a subset of ACSL, called ACSLsmall, and giving a formal semantics also for this. Lastly, two examples are provided showing that the theory developed in this thesis can be applied to automatically infer ACSL function contracts. / Den här avhandlingen studerar synergier mellan deduktiv verifikation och modelprovning, genom att använda Tricera, ett verktyg för modellprovning, för att automatiskt generera specifikationer för Frama-C, ett verktyg för deduktiv verifikation. Detta uppnås genom att definiera en formell semantik för en delmängd av ANSI-C, utökat med assume satser, som kallas förCsmall. Sedan visas hur kontrakt kan översättas till satser i Csmall samt att översättningen är korrekt. Därefter visas att översättningen också kan tillämpas på ett verkligt specifikationsspråk, genom att definiera en delmängd av ACSL, som kallas ACSLsmall, och definiera en formell semantik också för detta. Slutligen visas med två exempel hur teorin från uppsatsen kan appliceras för att automatiskt generera funktionskontrakt i ACSL.

Embedded software today is pervasive: they can be found everywhere, from coffee makers and medical devices, to cars and aircraft. Embedded software today is also open and connected to the Internet, exposing them to external attacks that can cause its Control-Flow Integrity (CFI) to be violated. Control-Flow Integrity is an important safety property of software, which ensures that the behavior of the software is not inadvertently changed. The violation of CFI in software can cause unintended behaviors, and can even lead to catastrophic incidents in safety-critical systems. This dissertation develops a two-part approach for CFI: (i) prescribing source-code safetychecks, that prevent the root-causes of CFI, that programmers can insert themselves, and (ii) formally proving CFI for the machine-code of programs with source-code safety-checks. First, our prescribed safety-checks, when applied, prevent the root-causes of CFI, thereby enabling software to recover from CFI violations in a customizable way. In addition, our prescribed safety-checks are visible to programmers, empowering them to ensure that the behavior of their software is not inadvertently changed by the prescribed safety-checks. However, programmer-inserted safety-checks may be incomplete. Thus, current techniques for proving CFI, which assume that safety-checks are complete, may not work. Second, this dissertation develops a logic approach that automates formal proofs of CFI for the machine-code of software containing both source-code CFI safety-checks and system calls. We extend an existing trustworthy Hoare logic with new proof rules, proof tactics, and a novel proof-search algorithm, which exploit the principle of local reasoning for safety properties to automatically generate CFI proofs for the machine-code of programs compiled with our prescribed source-code safety-checks. To the best of our knowledge, our approach to CFI is the first to combine programmer-visible source-code enforcement mechanisms for CFI–enabling programmers to customize them and observe that their software is not inadvertently changed–with machine-code proofs of CFI that can be automated, and that does not require a trusted or verified compiler to ensure its proven properties hold in machine-code. We evaluate our CFI approach on realistic embedded software. We evaluate our approach on the MiBench and WCET benchmarks, implementations of common file utilities, and programs interfacing with hardware inputs and outputs on the Raspberry Pi single-board-computer. The variety of our target programs, and our ability to support useful features such as file and hardware inputs and outputs, demonstrate the wide applicability of our approach.

A number of questions regarding programs involving heap-based data structures can be phrased as questions about numeric properties of those structures. A data structure traversal might terminate if the length of some path is eventually zero or a function to remove n elements from a collection may only be safe if the collection has size at least n. In this thesis, we develop proof methods for reasoning about the connection between heap-manipulating programs and numeric programs. In addition, we develop an automatic method for producing numeric abstractions of heap-manipulating programs. These numeric abstractions are expressed as simple imperative programs over integer variables and have the feature that if a property holds of the numeric program, then it also holds of the original, heap-manipulating program. This is true for both safety and liveness. The abstraction procedure makes use of a shape analysis based on separation logic and has support for user-defined inductive data structures. We also discuss a number of applications of this technique. Numeric abstractions, once obtained, can be analyzed with a variety of existing verification tools. Termination provers can be used to reason about termination of the numeric abstraction, and thus termination of the original program. Safety checkers can be used to reason about assertion safety. And bound inference tools can be used to obtain bounds on the values of program variables. With small changes to the program source, bounds analysis also allows the computation of symbolic bounds on memory use and computational complexity.