Дисертації з теми "Vérification de programmes et de modèles"
Щоб переглянути інші типи публікацій з цієї теми, перейдіть за посиланням: Vérification de programmes et de modèles.
Оформте джерело за APA, MLA, Chicago, Harvard та іншими стилями
Ознайомтеся з топ-50 дисертацій для дослідження на тему "Vérification de programmes et de modèles".
Біля кожної праці в переліку літератури доступна кнопка «Додати до бібліографії». Скористайтеся нею – і ми автоматично оформимо бібліографічне посилання на обрану працю в потрібному вам стилі цитування: APA, MLA, «Гарвард», «Чикаго», «Ванкувер» тощо.
Також ви можете завантажити повний текст наукової публікації у форматі «.pdf» та прочитати онлайн анотацію до роботи, якщо відповідні параметри наявні в метаданих.
Переглядайте дисертації для різних дисциплін та оформлюйте правильно вашу бібліографію.
1
Sellami, Yanis. "Raisonnement abductif modulo des théories et application à la vérification de programmes." Thesis, Université Grenoble Alpes, 2020. http://www.theses.fr/2020GRALM018.
Анотація:
Le travail présenté dans cette thèse introduit une méthode générique pour calculer les impliqués premiers d'une formule logique donnée dans une théorie décidable. Il s'agit intuitivement des conséquences clausales les plus générales de cette formule modulo cette théorie. Cette méthode fonctionne en ajoutant récursivement à un ensemble initialement vide des littéraux extraits d'un ensemble d'hypothèses présélectionnées, et ce jusqu'à ce qu'elle puisse démontrer que la disjonction des littéraux de cet ensemble est une conséquence de la formule sur laquelle elle travaille. On démontrera la terminaison, la correction et la complétude de cet algorithme. Cela confirmera qu'il calcule effectivement des impliqués de la formule de départ et qu'il retourne tous les impliqués premiers qui peuvent être construits à partir de l'ensemble d'hypothèses de départ. On construira ensuite à partir de cette méthode un algorithme l'appliquant à la génération d'invariants de boucles de programmes que l'on cherche à vérifier. On présentera également une implémentation C++ de ces deux méthodes, regroupées dans une infrastructure logicielle baptisée Abdulot. Cette implémentation sera utilisée pour évaluer expérimentalement les deux méthodes. On découvrira à cette occasion qu'elles sont capables de générer des solutions pour une large classe de problèmes.Cette thèse présente également un travail introductif sur la minimisation de modèles en logique de séparation et son implémentation. La méthode décrite pourrait également être utilisée pour résoudre des instances de bi-abduction en logique de séparation, à l'aide d'un algorithme qui sera décrit mais pas implémentéThis thesis introduces a generic method to compute the prime implicates of a logical formula, i.e., the most general clausal consequences of a given logical formula, in any given decidable theory. The principle used is to recursively add to an initially empty set, literals taken from a preselected set of hypotheses until it can be proven that the disjunction of these literals is a consequence of the formula under consideration. Proofs of the termination, correctness and completeness of this algorithm are provided, which ensures that the clauses the method computes are indeed implicates and that all the prime implicates that can be constructed from the initial set are indeed returned. This algorithm is then applied in the context of program verification, in which it is used to generate loop invariants that permit to verify assertions on programs. The Abdulot framework, a C++ implementation of the system, is also introduced. Technical considerations required for the design of such systems are detailed, such as their insertion within a well-furnished ecosystem of provers and SMT-Solvers. This implemented framework will be used to perform an experimental evaluation of the method and will show its practical relevance, as it can be used to solve a large scope of problems.This thesis also presents introductory work on an implicant minimizer and applies it in the context of separation logic. The method described in this part could also be used to perform bi-abduction in separation logic, with an algorithm that is described but has not been implemented
2
Sangnier, Arnaud. "Vérification de systèmes avec compteurs et pointeurs." Cachan, Ecole normale supérieure, 2008. http://www.theses.fr/2008DENS0051.
Анотація:
Au cours des dernières années, les méthodes formelles se sont avérées être une approche prometteuse pour garantir que le comportement d’un système informatique respecte une spécification donnée. Parmi les différentes techniques développées, le model-checking a été récemment étudié et appliqué avec succès à un grand nombre de modèles comme les systèmes à compteurs, les automates communicants (avec perte), les automates à pile, les automates temporisés, etc. Dans cette thèse, nous considérons deux modèles particuliers dans l’objectif de vérifier des programmes manipulant des variables entières et des variables de pointeurs. Dans une première partie, nous nous intéressons aux systèmes à compteurs. Nous commençons par définir ce modèle ainsi que ses différentes restrictions. Nous introduisons ensuite une sous-classe de systèmes à compteurs, appelée les machines à compteurs reversal-bornées, pour lesquelles de nombreux problèmes d’accessibilité sont décidables. Nous montrons que cette classe peut être étendue tout en gardant les résultats de décidabilité et nous prouvons qu’il est possible de décider si un Système d’Addition de Vecteurs avec États est reversal-borné, alors que cela n’est pas possible si l’on considère les systèmes à compteurs dans leur généralité. Nous finissons cette partie sur les systèmes à compteurs par l’étude de problèmes de model-checking de logiques temporelles. Les logiques temporelles que nous prenons en compte permettent de parler des données manipulées par le système. En particulier, nous montrons que le model-checking d’automates à un compteur déterministes avec des formules de la logique LTL avec registres est décidable, mais que cela n’est plus vrai lorsque l’hypothèse sur le déterminisme est supprimée. Dans une deuxième partie, nous introduisons le modèle des systèmes à pointeurs, qui est utilisé pour représenter des programmes manipulant des listes simplement chaînées. Nous donnons un algorithme qui traduit tout système à pointeurs en un système à compteurs qui lui est bisimilaire. Ceci nous permet de réutiliser les méthodes existantes pour l’analyse de systèmes à compteurs pour vérifier des programmes avec listes. Nous présentons ensuite une extension de la logique CTL* pour vérifier des propriétés temporelles sur de tels programmes, et nous étudions la décidabilité du problème de model-checking pour cette nouvelle logique. Finalement, dans une dernière partie, nous donnons une description de l’outil TOPICS (Translation of Programs Into Counter Systems) qui traduit un programme écrit dans un fragment syntaxique du langage C en un système à compteursIn the past years, formal methods have shown to be a succesfull approach to ensure that the behavior of an informatic system will respect some properties. Among the different existing techniques, model-checking have been recently studied and successfully applied to a lot of models like counter systems, lossy channel systems, pushdown automata, timed automata, etc. In this thesis, we consider two different models to verify programs which manipulate integer variables and pointer variables. In a first part, we deal with counter systems. We define the model and the different restrictions which have been proposed. We then introduce a restricted class of counter systems, called the reversal-bounded counter machines, for which many reachability problems are decidable. We show that this class can be extended keeping the decidability results and we prove that we can decide whether a Vector Addition System with States is reversal-bounded or not, which is not possible for general counter systems. We then study the problem of model-checking counter systems with different temporal logics. The temporal logics we consider allow to speak about the data manipulated by the system. In particular, we show that the model-checking of deterministic one-counter automata with formulae of LTL with registers is decidable, and becomes undecidable when considering non deterministic one-counter automata and two counter automata. In a second part, we introduce the model of pointer systems, which is used to represent programs manipulating single linked lists. We propose an algorithm to translate any pointer system into a bisimilar counter system. This allows us to reuse existing techniques over counter systems to analyze these programs. We then propose an extension of CTL* to verify temporal properties for such programs, and we study the decidability of the model-checking problem for this new logic. Finally we present the tool TOPICS (Translation of Programs Into Counter Systems) which translates a C-like program with pointers and integer variables into a counter system
3
Blanchard, Allan. "Aide à la vérification de programmes concurrents par transformation de code et de spécifications." Thesis, Orléans, 2016. http://www.theses.fr/2016ORLE2073/document.
Анотація:
Vérifier formellement des programmes concurrents est une tâche difficile. S’il existe différentes techniques pour la réaliser, très peu sont effectivement mises en oeuvre pour des programmes écrits dans des langages de programmation réalistes. En revanche, les techniques de vérification formelles de programmes séquentiels sont utilisées avec succès depuis plusieurs années déjà, et permettent d’atteindre de hauts degrés de confiance dans nos systèmes. Cette thèse propose une alternative aux méthodes d’analyses dédiées à la vérification de programmes concurrents consistant à transformer le programme concurrent en un programme séquentiel pour le rendre analysable par des outils dédiés aux programmes séquentiels. Nous nous plaçons dans le contexte de FRAMA-C, une plate-forme d’analyse de code C spécifié avec le langage ACSL. Les différentes analyses de FRAMA-C sont des greffons à la plate-forme, ceux-ci sont à ce jour majoritairement dédiés aux programmes séquentiels. La méthode de vérification que nous proposons est appliquée manuellement à la vérification d’un code concurrent issu d’un hyperviseur. Nous automatisons la méthode à travers un nouveau greffon à FRAMA-C qui permet de produire automatiquement, depuis un programme concurrent spécifié, un programme séquentiel spécifié équivalent. Nous présentons les bases de sa formalisation, ayant pour but d’en prouver la validité. Cette validité n’est valable que pour la classe des programmes séquentiellement consistant. Nous proposons donc finalement un prototype de solveur de contraintes pour les modèles mémoire faibles, capable de déterminer si un programme appartient bien à cette classe en fonction du modèle mémoire cibleFormal verification of concurrent programs is a hard task. There exists different methods to perform such a task, but very few are applied to the verification of programs written using real life programming languages. On the other side, formal verification of sequential programs is successfully applied for many years, and allows to get high confidence in our systems. As an alternative to dedicated concurrent program analyses, we propose a method to transform concurrent programs into sequential ones to make them analyzable by tools dedicated to sequential programs. This work takes place within the analysis framework FRAMA-C, dedicated to the analysis of C code specified with ACSL. The different analyses provided by FRAMA-C are plugins to the framework, which are currently mostly dedicated to sequential programs. We apply this method to the verification of a concurrent code taken from an hypervisor. We describe the automation of the method implemented by a new plugin to FRAMAC that allow to produce, from a specified concurrent program, an equivalent specified sequential program. We present the basis of a formalization of the method with the objective to prove its validity. This validity is admissible only for the class of sequentially consistent programs. So, we finally propose a prototype of constraint solver for weak memory models, which is able to determine whether a program is in this class or not, depending on the targeted hardware
4
Jahier, Erwan. "Analyse dynamique de programme : Mise en oeuvre automatisée d'analyseurs performants et spécifications de modèles d'exécution." Rennes, INSA, 2000. http://www.theses.fr/2000ISAR0009.
Анотація:
De nombreuses études montrent que la plus grande partie du coût de production d'un logiciel est générée lors de la phase de maintenance. Lors de cette phase, pour corriger des erreurs, pour optimiser des programmes, ou pour ajouter des fonctionnalités, il est essentiel de comprendre les programmes, et en particulier de comprendre leur comportement. Les analyseurs dynamiques d'exécutions tels que les profileurs, les moniteurs, ou les débogueurs, sont alors des outils indispensables. Cependant, ces outils d'analyse dynamique sont extrêmement coûteux à mettre en oeuvre : (1) d'abord, parce qu'il est généralement nécessaire de modifier le système de compilation utilisé, ce qui est fastidieux et pas toujours envisageable ; (2) en outre, les besoins en outils d'analyse de programmes varient d'un utilisateur à l'autre, en fonction de sa compétence, de son expérience du système de programmation utilisé, ainsi que de sa connaissance du code à maintenir ; (3) et enfin, parce que ces outils sont difficilement réutilisables. Il est donc souhaitable que chaque utilisateur puisse spécifier facilement les analyses dynamiques dont il a besoin. C'est pourquoi nous proposons dans cette thèse une architecture qui permet de faciliter leur mise en oeuvre. Cette architecture est basée : (1) sur une instrumentation systématique du programme qui produit une image très détaillée de l'exécution, la trace ; (2) sur un ensemble de primitives qui permettent d'analyser cette trace efficacement. Les analyseurs résultants ont des performances du même ordre de grandeur que leurs équivalents implémentés <<à la main>> par modification du système de compilation. Ils peuvent être mis en oeuvre par des utilisateurs sans connaissance particulière du système de compilation, qu'ils n'ont pas à modifier. Cette architecture leur permet d'implémenter les outils qui leur conviennent, adaptés à leur niveau de compréhension du code qu'ils sont chargés de maintenir. De plus, la structure modulaire de l'architecture proposée devrait permettre de faciliter la réutilisation de ces analyseurs pour d'autres systèmes. Notre propos est illustré dans le cadre du langage de programmation logique et fonctionnelle Mercury. Cependant, les concepts utilisés sont indépendants du paradigme de programmation. La trace sur laquelle nous basons la mise en oeuvre de nos analyseurs se doit de refléter le plus fidèlement possible la sémantique opérationnelle du langage. C'est pourquoi nous proposons également dans cette thèse un cadre de modélisation des traces d'exécutions basé sur une sémantique opérationnelle du langage à analyser. Cette spécification formelle de la trace nous permet de valider expérimentalement les traceurs et de prouver leur correction. Cette étude a été menée dans le cadre du langage de programmation logique PrologSeveral studies show that most of the software production cost is spent during the maintenance phase. During that phase, to locate bugs, to optimize programs, or to add new functionalities, it is essential to understand programs, and in particular to understand their runtime behavior. Dynamic analysis tools such as debuggers, profilers, or monitors, are very useful in that respect. However, such tools are expensive to implement because: (1) it generally requires to modify the compiling system, which is tedious and not always possible; (2) the needs in dynamic analysis tools vary from one user to another, depending on its competence, on its experience of the programming system, and on its knowledge of the code to maintain; (3) such tools are generally difficult to reuse. It is therefore desirable that each user is able to specify easily the dynamic analyses he needs. Hence, we propose an architecture that eases dynamic analysis tools implementation. This architecture is based on: (1) a systematic instrumentation of the program which gives a detailed image of the execution, the trace; (2) a set of trace processing primitives that lets one analyse the trace efficiently. The resulting analysers have performance of the same order of magnitude that their equivalent implemented ``by hand'' by modifying the compiling system. They can be implemented by programmers without any knowledge of the compiling system. This architecture let them implement the tools they need, adapted to their level of comprehension of the code they are in charge to maintain. Furthermore, the modular structure of the proposed architecture should ease the analysers reuse. This work has been held within the context of the logical and functional programming language Mercury. However, the concepts we used do not depend on the programming paradigm. The trace on which we base the implementation of our dynamic analysis tools should reflect as much as possible the runtime behavior of programs. Therefore, we also propose a framework to specify execution traces. This framework is based on an operational semantics of the language to analyse. Such formal specifications of the trace let us experimentally validate tracers, and prove their correctness. This work have been held within the context of the logical programming language Prolog
5
Bobot, François. "Logique de séparation et vérification déductive." Phd thesis, Université Paris Sud - Paris XI, 2011. http://tel.archives-ouvertes.fr/tel-00652508.
Анотація:
Cette thèse s'inscrit dans la démarche de preuve de programmes à l'aide de vérification déductive. La vérification déductive consiste à produire, à partir des sources d'un programme, c'est-à-dire ce qu'il fait, et de sa spécification, c'est-à-dire ce qu'il est sensé faire, une conjecture qui si elle est vraie alors le programme et sa spécification concordent. On utilise principalement des démonstrateurs automatiques pour montrer la validité de ces formules. Quand ons'intéresse à la preuve de programmes qui utilisent des structures de données allouées en mémoire, il est élégant et efficace de spécifier son programme en utilisant la logique de séparation qui est apparu il y a une dizaine d'année. Cela implique de prouver des conjectures comportant les connectives de la logique de séparation, or les démonstrateurs automatiques ont surtout fait des progrès dans la logique du premier ordre qui ne les contient pas.Ce travail de thèse propose des techniques pour que les idées de la logique de séparation puissent apparaître dans les spécifications tout en conservant la possibilité d'utiliser des démonstrateurs pour la logique du premier ordre. Cependant les conjectures que l'ont produit ne sont pas dans la même logique du premier ordre que celles des démonstrateurs. Pour permettre une plus grande automatisation, ce travail de thèse a également défini de nouvelles conversions entre la logique polymorphe du premier ordre et la logique multi-sortée dupremier ordre utilisé par la plupart des démonstrateurs.La première partie a donné lieu à une implémentation dans l'outil Jessie, la seconde a donné lieu à une participation conséquente à l'écriture de l'outil Why3 et particulièrement dans l'architecture et écriture des transformations qui implémentent ces simplifications et conversions.
6
Fernandes, Pires Anthony. "Amélioration des processus de vérification de programmes par combinaison des méthodes formelles avec l’Ingénierie Dirigée par les Modèles." Thesis, Toulouse, ISAE, 2014. http://www.theses.fr/2014ESAE0023/document.
Анотація:
Lors d’un développement logiciel, et plus particulièrement d’un développement d’applications embarquées avioniques, les activités de vérification représentent un coût élevé. Une des pistes prometteuses pour la réduction de ces coûts est l’utilisation de méthodes formelles. Ces méthodes s’appuient sur des fondements mathématiques et permettent d’effectuer des tâches de vérification à forte valeur ajoutée au cours du développement. Les méthodes formelles sont déjà utilisées dans l’industrie. Cependant, leur difficulté d’appréhension et la nécessité d’expertise pour leur mise en pratique sont un frein à leur utilisation massive. Parallèlement au problème des coûts liés à la vérification logicielle, vient se greffer la complexification des logiciels et du contexte de développement. L’Ingénierie Dirigée par les Modèles (IDM) permet de faire face à ces difficultés en proposant des modèles, ainsi que des activités pour en tirer profit.Le but des travaux présentés dans cette thèse est d’établir un lien entre les méthodes formelles et l’IDM afin de proposer à des utilisateurs non experts une approche de vérification formelle et automatique de programmes susceptible d’améliorer les processus de vérification actuels. Nous proposons de générer automatiquement sur le code source des annotations correspondant aux propriétés comportementales attendues du logiciel, et ce, à partir de son modèle de conception. Ces annotations peuvent ensuite être vérifiées par des outils de preuve déductive, afin de s’assurer que le comportement du code est conforme au modèle. Cette thèse CIFRE s’inscrit dans le cadre industriel d’Atos. Il est donc nécessaire de prendre en compte le contexte technique qui s’y rattache. Ainsi, nous utilisons le standard UML pour la modélisation,le langage C pour l’implémentation et l’outil Frama-C pour la preuve du code. Nous tenons également compte des contraintes du domaine du logiciel avionique dans lequel Atos est impliqué et notamment les contraintes liées à la certification.Les contributions de cette thèse sont la définition d’un sous-ensemble des machines à états UML dédié à la conception comportementale de logiciel avionique et conforme aux pratiques industrielles existantes, la définition d’un patron d’implémentation C, la définition de patrons de génération des propriétés comportementales sur le code à partir du modèle et enfin l’implémentation de l’approche dans un prototype compatible avec l’environnement de travail des utilisateurs potentiels en lien avec Atos. L’approche proposée est finalement évaluée par rapport à l’objectif de départ, par rapport aux attentes de la communauté du génie logiciel et par rapport aux travaux connexesDuring software development, and more specifically embedded avionics applications development, verification is very expensive. A promising lead to reduce its costs is the use of formal methods. Formal methods are mathematical techniques which allow performing rigorous and high-valued verification tasks during software development. They are already applied in industry. However, the high level of expertise required for their use is a major obstacle for their massive use. In addition to the verification costs issue, today software and their development are subject to an increase in complexity. Model Driven Engineering (MDE) allows dealing with these difficulties by offering models, and tasks to capitalize on these models all along the development lifecycle. The goal of this PhD thesis is to establish a link between formal methods and MDE in order to propose to non-expert users a formal and automatic software verification approach which helps to improve software verification processes. We propose to automatically generate annotations, corresponding to the expected behavioural properties of the software, from the design model to the source code. Then, these annotations can be verified using deductive proof tools in order to ensure that the behaviour of the code conforms to the design model. This PhD thesis takes place in the industrial context of Atos. So, it is necessary to take into account its technical specificities. We use UML for the design modeling, the C language for the software implementation and the Frama-C tool for the proof of this implementation. We also take into account the constraints of the avionics field in which Atos intervenes, and specifically the certification constraints. The contributions of this PhD thesis are the definition of a subset of UML state machine dedicated to the behavioural design of embedded avionics software and in line with current industrial practices, the definition of a C implementation pattern, the definition of generation patterns for the behavioural properties from the design model to the source code and the implementation of the whole approach in a prototype in accordance with the working environment of the potential users associated with Atos. The proposed approach is then assessed with respect to the starting goal of the thesis, to the expectation of the software engineering community and to related work
7
Bardou, Romain. "Vérification de programmes avec pointeurs à l'aide de régions et de permissions." Thesis, Paris 11, 2011. http://www.theses.fr/2011PA112220/document.
Анотація:
La vérification déductive de programmes consiste à annoter des programmes par une spécification, c'est-à-dire un ensemble de formules logiques décrivant le comportement du programme, et à prouver que les programmes vérifient bien leur spécification. Des outils tels que la plate-forme Why prennent en entrée un programme et sa spécification et calculent des formules logiques telles que, si elles sont prouvées, le programme vérifie sa spécification. Ces formules logiques peuvent être prouvées automatiquement ou à l'aide d'assistants de preuve.Lorsqu'un programme est écrit dans un langage supportant les alias de pointeurs, c'est-à-dire si plusieurs variables peuvent désigner la même case mémoire, alors le raisonnement sur le programme devient particulièrement ardu. Il est nécessaire de spécifier quels pointeurs peuvent être égaux ou non. Les invariants des structures de données, en particulier, sont plus difficiles à vérifier.Cette thèse propose un système de type permettant de structurer la mémoire de façon modulaire afin de contrôler les alias de pointeurs et les invariants de données. Il est basé sur les notions de région et de permission. Les programmes sont ensuite interprétés vers Why de telle façon que les pointeurs soient séparés au mieux, facilitant ainsi le raisonnement. Cette thèse propose aussi un mécanisme d'inférence permettant d'alléger le travail d'annotation des opérations de régions introduites par le langage. Un modèle est introduit pour décrire la sémantique du langage et prouver sa sûreté. En particulier, il est prouvé que si le type d'un pointeur affirme que celui-ci vérifie son invariant, alors cet invariant est effectivement vérifié dans le modèle. Cette thèse a fait l'objet d'une implémentation sous la forme d'un outil nommé Capucine. Plusieurs exemples ont été écrits pour illustrer le langage, et ont été vérifié à l'aide de CapucineDeductive verification consists in annotating programs by a specification, i.e. logic formulas which describe the behavior of the program, and prove that programs verify their specification. Tools such as the Why platform take a program and its specification as input and compute logic formulas such that, if they are valid, the program verifies its specification. These logic formulas can be proven automatically or using proof assistants.When a program is written in a language supporting pointer aliasing, i.e. if several variables may denote the same memory cell, then reasoning about the program becomes particularly tricky. It is necessary to specify which pointers may or may not be equal. Invariants of data structures, in particular, are harder to maintain.This thesis proposes a type system which allows to structure the heap in a modular fashion in order to control pointer aliases and data invariants. It is based on the notions of region and permission. Programs are then translated to Why such that pointers are separated as best as possible, to facilitate reasoning. This thesis also proposes an inference mechanism to alleviate the need to write region operations introduced by the language. A model is introduced to describe the semantics of the language and prove its safety. In particular, it is proven that if the type of a pointer tells that its invariant holds, then this invariant indeed holds in the model. This work has been implemented as a tool named Capucine. Several examples have been written to illustrate the language, and where verified using Capucine
8
Bardou, Romain. "Verification de programmes avec pointeurs a l'aide de regions et de permissions." Phd thesis, Université Paris Sud - Paris XI, 2011. http://tel.archives-ouvertes.fr/tel-00647331.
Анотація:
La vérification déductive de programmes consiste à annoter des programmes par une spécification, c'est-à-dire un ensemble de formules logiques décrivant le comportement du programme, et à prouver que les programmes vérifient bien leur spécification. Des outils tels que la plate-forme Why prennent en entrée un programme et sa spécification et calculent des formules logiques telles que, si elles sont prouvées, le programme vérifie sa spécification. Ces formules logiques peuvent être prouvées automatiquement ou à l'aide d'assistants de preuve.Lorsqu'un programme est écrit dans un langage supportant les alias de pointeurs, c'est-à-dire si plusieurs variables peuvent désigner la même case mémoire, alors le raisonnement sur le programme devient particulièrement ardu. Il est nécessaire de spécifier quels pointeurs peuvent être égaux ou non. Les invariants des structures de données, en particulier, sont plus difficiles à vérifier.Cette thèse propose un système de type permettant de structurer la mémoire de façon modulaire afin de contrôler les alias de pointeurs et les invariants de données. Il est basé sur les notions de région et de permission. Les programmes sont ensuite interprétés vers Why de telle façon que les pointeurs soient séparés au mieux, facilitant ainsi le raisonnement. Cette thèse propose aussi un mécanisme d'inférence permettant d'alléger le travail d'annotation des opérations de régions introduites par le langage. Un modèle est introduit pour décrire la sémantique du langage et prouver sa sûreté. En particulier, il est prouvé que si le type d'un pointeur affirme que celui-ci vérifie son invariant, alors cet invariant est effectivement vérifié dans le modèle. Cette thèse a fait l'objet d'une implémentation sous la forme d'un outil nommé Capucine. Plusieurs exemples ont été écrits pour illustrer le langage, et ont été vérifié à l'aide de Capucine.
9
Clouet, Myriam. "Langage de spécification et outil de vérification pour le consentement et la nécessité des données fondés sur une classification relative au respect de la vie privée." Electronic Thesis or Diss., université Paris-Saclay, 2024. http://www.theses.fr/2024UPASG023.
Анотація:
La vie privée est un droit fondamental que l'on retrouve dans plusieurs lois dans le monde entier. Donc, vérifier qu'un système respecte la vie privée est crucial. Cependant, la vie privée est une notion complexe. Assurer qu'un système respecte la vie privée nécessite de vérifier que les propriétés de vie privées sont respectées durant tout le cycle de vie, ce qui complique le processus de vérification. Une grande variété de solutions ont été proposées pour améliorer le respect de la vie privée. Il est souvent difficile de précisément identifier quand elles ciblent la même problématique.Dans cette thèse, j'adresse ces problèmes en proposant une façon de classifier des articles concernant la vie privée et une approche pour vérifier des propriétés de vie privée à deux étapes du cycle de vie. Je propose GePyR, une nouvelle représentation de la vie privée, générique et spécialisable, et une ontologie instanstiable, PyCO, qui modélise les éléments clés de la vie privée et leurs relations. Cette classification est évaluée sur la littérature, en réalisant un Systematic Mapping Study. Dans cette thèse, je formalise également deux propriétés de vie privée, la conformité aux finalités consenties et la conformité à la nécessité des données. Je propose une nouveau langage de spécification, CSpeL, qui permet de formaliser les éléments nécessaires pour vérifier ces propriétés, et introduit un nouvel outil, CASTT, pour vérifier ces propriétés sur des traces d'exécutions, sur un modèle ou un programme. Cette approche est appliquée sur deux cas d'utilisation à deux niveaux d'abstraction, pour évaluer sa correction, sont efficacité et son utilitéPrivacy is a fundamental right implemented in many laws around the world. Therefore, verifying that a system complies with privacy is crucial. However, privacy is also a complex notion. Besides, ensuring compliance of a software system with respect to privacy requires to verify that the expected privacy properties hold during the whole system lifecycle. It usually involves different abstraction levels, which complicates the verification process. Many different solutions have been proposed to enhance privacy. It is often quite hard to precisely identify whether they target the same problem.This thesis addresses these issues by proposing a way to classify privacy papers and an approach to verify privacy properties at two different development stages. It proposes GePyR, a new generic and specializable representation, and an instantiable ontology, PyCO, that models key privacy elements and their relationships. This classification is evaluated on the literature, by using a Systematic Mapping Study. This thesis also formalizes two privacy properties, purpose compliance and necessity compliance. It proposes a new specification language, named CSpeL, that allows engineers to formally specify key system elements with regards to these properties, and introduces a new tool, CASTT, to verify the aforementioned properties on execution traces, on a model or on a program. This approach is applied on two use cases, both at two abstraction levels (model and code), in order to evaluate its correctness, its efficiency and its usefulness
10
Ngo, Van Chan. "Vérification Formelle d'un Compilateur Synchrone: de Signal vers C." Phd thesis, Université Rennes 1, 2014. http://tel.archives-ouvertes.fr/tel-01058041.
Анотація:
Les langages synchrones tels que SIGNAL, LUSTRE et ESTEREL sont dédiés à la conception de systèmes critiques. Leurs compilateurs, qui sont de très gros programmes complexes, peuvent a priori se révéler incorrects dans certains situations, ce qui donnerait lieu alors à des résultats de compilation erronés non détectés. Ces codes fautifs peuvent invalider des propriétés de sûreté qui ont été prouvées en appliquant des méthodes formelles sur les programmes sources. En adoptant une approche de validation de la traduction, cette thèse vise à prouver formellement la correction d'un compilateur optimisé et industriel de SIGNAL. La preuve de correction représente dans un cadre sémantique commun le programme source et le code compilé, et formalise une relation entre eux pour exprimer la préservation des sémantiques du programme source dans le code compilé.
11
Chorfi, Redha. "Abstraction et vérification de programmes informatiques." Thesis, Université Laval, 2008. http://www.theses.ulaval.ca/2008/25710/25710.pdf.
Анотація:
Les systèmes informatiques offrent une grande flexibilité aux usagers en leur permettant
l’accès, notamment par le biais de réseaux de télécommunication ou de l’Internet, à
un vaste éventail de services. Toutefois, certains de ces services sont soumis à de fortes
contraintes de sécurité, comme le télépaiement qui est au coeur du commerce électronique.
Ainsi, les fournisseurs et les utilisateurs expriment des besoins croissants, et antagonistes,
en sécurité. Répondre à ces deux besoins simultanément est un enjeu technologique transversal
à de nombreux domaines de l’informatique. L’objectif de ce travail est de développer
un mécanisme permettant de garantir la sécurité des systèmes, en s’appuyant sur
l’expérience établie dans le domaine de la sécurité et des méthodes formelles. Pour se
faire, nous définissons un nouveau cadre de vérification des propriétés de sécurité d’un
programme informatique par l’analyse des flots de données et de contrôle construits à
partir du code de ce dernier. L’idée principale consiste à définir un modèle pouvant abstraire
la trace d’événements et les dépendances de ressources engendrés au moment de
l’exécution du programme, et pouvant être soumis à des algorithmes de vérification de
modèle (model-checking) pour l’analyse de la sûreté du programme vis-à-vis d’une propriété.
12
Garavel, Hubert. "Compilation et vérification de programmes LOTOS." Grenoble 1, 1989. http://tel.archives-ouvertes.fr/tel-00004339.
Анотація:
LOTOS (Language Of Temporal Ordering Specification) est un langage de description de systèmes parallèles communicants, normalisé par l'ISO et le CCITT afin de permettre la définition formelle des protocoles et des services de télécommunications. Le langage utilise des types abstraits algébriques pour spécifier les données et un calcul de processus proche de CSP et CCS pour exprimer le contrôle. Cette thèse propose une technique de compilation permettant de traduire un sous-ensemble significatif de LOTOS vers un modele reseau de Petri interprete (pouvant servir a produire du code executable) puis vers un modèle automate d'etats finis (permettant la vérification formelle de programmes LOTOS soit par réduction ou comparaison modulo des relations d'equivalence, soit par évaluation de formules de logiques temporelles). La méthode employée diffère des approches usuelles basées sur la réécriture de termes, qui construisent directement le graphe d'états correspondant à un programme LOTOS. Ici au contraire la traduction est effectuée en trois étapes successives (expansion, génération et simulation) s'appuyant sur des modèles sémantiques intermédiaires (le langage SUBLOTOS et le modèle reseau). Elle met en oeuvre une analyse statique globale du comportement des programmes. Elle prend en compte les données, celles-ci devant être compilées au moyen d'algorithmes déjà existants. Ces principes de compilation ont été entièrement implémentés dans le logiciel CAESAR. Les performances obtenues confirment l'intérêt de la méthode
13
Cassez, Franck. "Compilation et vérification des programmes ELECTRE." Nantes, 1993. http://www.theses.fr/1993NANT2013.
Анотація:
On présente dans cette thèse une sémantique opérationnelle du langage réactif asynchrone ELECTRE basée sur un système de réécriture conditionnelle par calcul d'attributs synthétises sur la grammaire du langage. On montre que cette sémantique permet de construire un modèle d'exécution fini et déterministe pour tous les programmes du langage. Ce modèle est un système de transitions à file. Enfin, nous donnons des modèles de validation équivalents au modèle d'exécution sur lesquels on peut vérifier des propriétés comportementales par utilisation d'outils d'analyse de systèmes de transitions
14
Djoko, Djoko Simplice. "Analyses et vérification des programmes à aspects." Phd thesis, Université de Nantes, 2009. http://tel.archives-ouvertes.fr/tel-00752116.
Анотація:
La programmation par aspects est un paradigme de programmation qui permet de mieux séparer les préoccupations d'une application. Un aspect est défini pour chaque préoccupation qui ne peut pas être isolée dans un module. Les aspects sont ensuite ajoutés au programme de base par un processus automatique appelé tissage. Cependant, l'expressivité des langages d'aspect généraux permet de modifier totalement la sémantique du programme de base (par ex., un aspect peut remplacer certains appels de méthode par du code arbitraire). Ce comportement peut entraîner la perte des avantages (lisibilité, maintenabilité, réutilisabilité, etc.) d'une meilleure modularisation des préoccupations. Il devient impossible de raisonner sur le programme de base sans regarder le programme tissé. Cette thèse apporte une réponse aux problèmes ci-dessus en définissant des catégories d'aspects dont l'impact sur la sémantique du programme de base reste sous contrôle. Pour chaque catégorie d'aspects, nous déterminons l'ensemble des propriétés du programme de base qui est préservé par tissage. L'appartenance d'un aspect à une catégorie est garantie par construction grâce à des langages d'aspect dédiés pour chaque catégorie. L'utilisation de ces langages assure que le tissage préservera l'ensemble des propriétés associé à la catégorie concernée. Les propriétés préservées sont représentées comme des sous ensembles de LTL et de CTL*. Nous prouvons formellement que quelque soit le programme de base, le tissage de n'importe quel aspect d'une catégorie préserve les propriétés de la catégorie correspondante. Ces langages et catégories sont définis dans un cadre formel indépendant de tout langage de base ou d'aspect. L'expressivité de ce cadre est montrée en décrivant des primitives complexes de langages d'aspect comme AspectJ et CaesarJ et en effectuant une preuve de correction de transformation d'aspect.
15
Atig, Mohamed Faouzi. "Vérification de Programmes Concurrents : Décidabilité et Complexité." Paris 7, 2010. http://www.theses.fr/2010PA077066.
Анотація:
Cette thèse porte sur la vérification des programmes concurrents, en nous intéressant en particulier à l'étude la décidabilité et la complexité des problèmes d'accessibilité. Dans la plus grande partie de cette thèse, nous considérons des programmes concurrents où les processus séquentiels correspondent à des threads pouvant faire des appels de procédures (potentiellement récursives). La difficulté vient de l'interaction entre la récursivité et de la concurrence qui rend le problème de l'accessibilité indécidable en général. Nous étudions alors les conditions sous lesquelles ce problème devient décidable. Ces conditions peuvent être vues comme des contraintes à poser sur l'ordonnancement des actions le long des exécutions du programme analysé. Ainsi, les résultats de décidabilité peuvent être utilisés pour définir des procédures d'analyse sous-approchée permettant de détecter de manière efficace des comportements illicites des programmes. Dans un second temps, nous nous intéressons aux programmes s'exécutant selon un modèle faible de la mémoire partagée (weak memory model). Dans de tels programmes, l'ordre entre les actions d'un même processus est relâché pour des besoins de performance en permettant la permutation entre certains types d'actions. Cela rend alors le conception des programmes concurrents encore plus difficile du fait que la sémantique de la concurrence devient hautement complexe et contre-intuitive. Nos travaux montrent qu'en effet selon le type des relaxations d'ordre entre actions, le problème de l'accessibilité peut être décidable mais hautement complexe dans certains cas, et il peut même être indécidable dans d'autresThis thesis addresses the verification problems in both, concurrent and recursive Systems as well as concurrent Systems with store buffers. We establish the required theoretical basis for automated analyses: decidability and complexity results for reachability problems. In a first time, we are interested in verifying concurrent programs where each process corresponds to a sequential program with (recursive) procedure calls. The difficulty in analyzing such programs cornes from the interaction between recursion and concurrency which makes the reachability problems undecidable in general. However, in practice programs obey additional constraints that can be exploited to turn the reachability problem decidable. Their study is subject of this thesis. These conditions may be seen as constraints to impose on the order between the actions of the analyzed programs. Moreover, these decidability results can be used to perform an under-approximation analysis to effectively detect bad behaviors of the analyzed programs. In a second time, we study concurrent programs running under weak memory models. In such kind of programs, the order between actions of the same process is relaxed (for performance reasons) by allowing the permutation between certain types of memory operations. This makes reasoning about the behaviors of concurrent programs much more difficult. Moreover, it is not clear how to apply standard reasoning techniques. Our works show that indeed according to the type of relaxation, the reachability problem becomes décidable (but with a highly complexity) in other cases, it even turns out undecidability
16
Declerck, David. "Vérification par model-checking de programmes concurrents paramétrés sur des modèles mémoires faibles." Thesis, Université Paris-Saclay (ComUE), 2018. http://www.theses.fr/2018SACLS336/document.
Анотація:
Les multiprocesseurs et microprocesseurs multicœurs modernes mettent en oeuvre des modèles mémoires dits faibles ou relâchés, dans dans lesquels l'ordre apparent des opérations mémoire ne suit pas la cohérence séquentielle (SC) proposée par Leslie Lamport. Tout programme concurrent s'exécutant sur une telle architecture et conçu avec un modèle SC en tête risque de montrer à l'exécution de nouveaux comportements, dont certains sont potentiellement des comportements incorrects. Par exemple, un algorithme d'exclusion mutuelle correct avec une sémantique par entrelacement pourrait ne plus garantir l'exclusion mutuelle lorsqu'il est mis en oeuvre sur une architecture plus relâchée. Raisonner sur la sémantique de tels programmes s'avère très difficile. Par ailleurs, bon nombre d'algorithmes concurrents sont conçus pour fonctionner indépendamment du nombre de processus mis en oeuvre. On voudrait donc pouvoir s'assurer de la correction d'algorithmes concurrents, quel que soit le nombre de processus impliqués. Pour ce faire, on s'appuie sur le cadre du Model Checking Modulo Theories (MCMT), développé par Ghilardi et Ranise, qui permet la vérification de propriétés de sûreté de programmes concurrents paramétrés, c'est-à-dire mettant en oeuvre un nombre arbitraire de processus. On étend cette technologie avec une théorie permettant de raisonner sur des modèles mémoires faibles. Le résultat ce ces travaux est une extension du model checker Cubicle, appelée Cubicle-W, permettant de vérifier des propriétés de systèmes de transitions paramétrés s'exécutant sur un modèle mémoire faible similaire à TSOModern multiprocessors and microprocesseurs implement weak or relaxed memory models, in which the apparent order of memory operation does not follow the sequential consistency (SC) proposed by Leslie Lamport. Any concurrent program running on such architecture and designed with an SC model in mind may exhibit new behaviors during its execution, some of which may potentially be incorrect. For instance, a mutual exclusion algorithm, correct under an interleaving semantics, may no longer guarantee mutual exclusion when implemented on a weaker architecture. Reasoning about the semantics of such programs is a difficult task. Moreover, most concurrent algorithms are designed for an arbitrary number of processus. We would like to ensure the correctness of concurrent algorithms, regardless of the number of processes involved. For this purpose, we rely on the Model Checking Modulo Theories (MCMT) framework, developed by Ghilardi and Ranise, which allows for the verification of safety properties of parameterized concurrent programs, that is to say, programs involving an arbitrary number of processes. We extend this technology with a theory for reasoning about weak memory models. The result of this work is an extension of the Cubicle model checker called Cubicle-W, which allows the verification of safety properties of parameterized transition systems running under a weak memory model similar to TSO
17
Bolduc, Claude. "Oméga-Algèbre : théorie et application en vérification de programmes." Thesis, Université Laval, 2006. http://www.theses.ulaval.ca/2006/23728/23728.pdf.
Анотація:
L’algèbre de Kleene est la théorie algébrique des automates finis et des expressions régulières. Récemment, Kozen a proposé un cadre de travail basé sur l’algèbre de Kleene avec tests
(une variante de l’algèbre de Kleene) pour vérifier qu’un programme satisfait une politique
de sécurité spécifiée par un automate de sécurité. Malheureusement, cette approche ne permet
pas de vérifier des propriétés de vivacité pour les programmes réactifs (programmes qui
s’exécutent à l’infini). Le but de ce mémoire est d’étendre la méthode de vérification de programmes
proposée par Kozen pour enlever cette limitation. Pour y arriver, nous développons
la théorie de l’oméga-algèbre (une extension de l’algèbre de Kleene qui prend en compte
les exécutions infinies) qui constitue la majeure partie de ce mémoire. En particulier, nous
présentons des résultats de complétude concernant la théorie de Horn de cette algèbre.Kleene algebra is the algebraic theory of finite automata and regular expressions. Recently, Kozen has proposed a framework based on Kleene algebra with tests (a variant of Kleene algebra) for verifying that a program satisfies a security policy specified by a security automaton. Unfortunately, this approach does not allow to verify liveness properties for reactive programs (programs that execute forever). The goal of this thesis is to extend the framework proposed by Kozen for program verification to remove this limitation. For that, we develop the theory of omega algebra, an extension of Kleene algebra suitable for reasoning about nonterminating executions. The main part of this thesis is about omega algebra. In particular, we show some completeness results about the Horn theory of omega algebra.
Inscrit au Tableau d'honneur de la Faculté des études supérieures
18
Brown, Naïma. "Vérification et mise en œuvre distribuée des programmes unity." Nancy 1, 1994. http://www.theses.fr/1994NAN10384.
Анотація:
L'affinement successif de programmes parallèles à partir de spécifications formelles permet de s'assurer de la correction du programme obtenu par rapport a la specification initiale, puisque la transformation est fondée sur la préservation de propriétés telles que celles d'invariance et celles de fatalité. Cependant, les programmes obtenus sont écrits dans une notation abstraite éloignée des langages de programmation parallèles classiques et il convient de développer des techniques de transformation de programmes (ensemble d'actions) en des programmes écrits dans des langages de programmation parallèles (linda, occam). Bien entendu, cela conduit à analyser les techniques possibles de parallélisation de systèmes d'actions ou de distribution de systèmes d'actions. Notre travail de thèse s'appuie sur le formalisme unity de Chandy et Misra pour lequel nous avons construit un outil d'aide à la preuve dans l'outil b et nous avons examiné plusieurs types de transformations de programmes unity en d'autres langages ainsi que des stratégies de répartition. Nous proposons un langage intermédiaire que nous dénommons UCL (unity communication language) qui facilite l'implantation d'unity sur une architecture parallèle, et qui assure la correction formelle de cette implantation vis-à-vis de la spécification initiale. Le langage UCL est ensuite utilisé comme nouveau point de départ de la transformation et permet de produire soit un programme Clinda, soit un programme Occam. Cette approche favorise la réutilisation de cette première étape de transformation avant de cibler une architecture particulière
19
Pavlova, Mariela. "Vérification de programmes en code octet et ses applications." Nice, 2007. http://www.theses.fr/2007NICE4010.
Анотація:
Les techniques de vérification basées sur les logiques de programmation ainsi que sur les générateurs de conditions de vérification permettent de raisonner de manière efficace sur les programmes. Bien que ces techniques aient souvent été utilisées avec des langages de haut niveau pour bénéficier de leurs structures, il est souvent nécessaire, plus spécifiquement dans le contexte du code mobile, de prouver la correction de programmes déjà compilés. C’est pourquoi il est très intéressant d’avoir un moyen pour utiliser la vérification de code source au niveau de l’utilisateur de code. Nous proposons un mécanisme qui permet de transférer des informations depuis le programme source vers le programme compilé. Il est construit autour d’un langage de spécification pour le code binaire, un générateur de conditions de vérification qui s’utilise sur des programmes annotés et un compilateur qui transforme les annotations au niveau du code source en des annotations au niveau du code binaire. Nous montrons que le générateur des conditions de vérification est correct et que les obligations de preuves au niveau du source et du code binaire sont presque les mêmes. Nous illustrons les bénéfices de notre démarche par deux études de casProgram verification techniques based on programming logics and verification condition generators provide a powerful means to reason about programs. Whereas these techniques have very often been employed in the context of high-level languages in order to benefit from their structural nature. It is often required, especially in the context of mobile code, to prove the correctness of compiled programs. Thus it is highly desirable to have a means of bringing the benefits of source code verification to code consumers. We propose a mechanism that allows to transfer evidence from source programs to compiled programs. It builds upon a specification language for bytecode, a verification condition generator that operates on annotated programs, and a compiler that transforms source annotations into bytecode annotations. We show that the verification condition generator is sound, and that the proof bytecode level nearly coincides. We illustrate the benefits of oue framework in two case studies
20
Kerbrat, Alain. "Méthodes symboliques pour la vérification de processus communicants : étude et mise en oeuvre." Université Joseph Fourier (Grenoble), 1994. http://tel.archives-ouvertes.fr/tel-00005100.
Анотація:
Ce travail porte sur la vérification formelle de programmes parallèles. Parmi les méthodes habituellement utilisées, nous nous intéressons aux méthodes basées sur la construction d'un modèle du programme à vérifier; la vérification proprement dite s'effectue sur ce modèle. Cette approche est limitée par l'explosion de la taille du modèle, dès que le programme traite est de complexité réaliste. Notre but est l'étude et la mise en œuvre de techniques permettant d'effectuer la vérification malgré cette explosion. Les techniques que nous présentons sont liées par une caractéristique commune : l'utilisation de méthodes symboliques de représentation du modèle. Nous étudions en premier lieu des techniques de réduction de modèles. Ces réductions s'opèrent par rapport à des relations d'équivalence basées sur la notion de bisimulation. Nous étudions en particulier un algorithme de minimisation de modèle pendant sa génération (Génération de Modèle Minimal). Dans une seconde partie, nous nous intéressons a deux techniques symboliques de représentation de modèles. Il s'agit d'une part de Graphes de Décision Binaires, qui permettent la manipulation efficace de formules booléennes, et d'autre part de systèmes d'inéquations linéaires, connus sous le nom de polyèdres convexes, pour la manipulation de variables entières. L'utilisation de ces techniques permet de représenter et manipuler des modèles de taille souvent prohibitive pour des méthodes énumératives classiques. Nous présentons la mise en œuvre de méthodes de comparaison et réduction de modèles aves les Graphes de Décision Binaires, avec en particulier l'algorithme de Génération de Modèle Minimal. L'application de l'outil correspondant à plusieurs exemples de programmes LOTOS a permis de montrer l'intérêt, mais aussi les limites de l'utilisation de cette représentation symbolique. Enfin, nous présentons une méthode d'analyse statique de protocoles, basée sur l'utilisation des polyèdres convexes. Cette analyse permet le calcul d'approximations supérieures d'invariants du programme et de vérifier la véracité de propriétés définies en termes de variables du programme.
21
Hurlin, Clément. "Spécification et vérification de programmes orientés objets en logique de séparation." Phd thesis, Université de Nice Sophia-Antipolis, 2009. http://tel.archives-ouvertes.fr/tel-00424979.
Анотація:
Cette thèse propose une extension de la logique de séparation pour les programmes parallèles et orientés-objets. La logique de séparation est un formalisme récent et prometteur pour vérifier les programmes impératifs. Cependant, jusqu'à présent, la logique de séparation a été appliquée à des programmes utilisant un opérateur parallèle irréaliste (||) et des verrous non-ré-entrants (contrairement au langage Java). Dans cette thèse, nous adaptons la logique de séparation aux opérateurs "fork" et "join" (utilisés par de nombreux langages: C, Java, etc...) et aux verrous ré-entrants (utilisés par le langage Java).Cette adaptation inclut un système de vérification pour des programmes similaires aux programmes Java. Ce système est constitué d'un ensemble de triplets de Hoare qui forment un algorithme de vérification. La preuve de correction de ce système a été effectuée et ce système a été évalué sur plusieurs exemples ambitieux (dont la classe Itérateur de la librairie Java et un algorithme de couplage de verrous).
En plus de l'extension décrite ci-dessus, plusieurs analyses utilisant la logique de séparation ont été inventées.
La première analyse consiste à spécifier les séquences d'appels de méthodes autorisées (appelés "protocoles") dans les classes. Cette analyse décrit finement des protocoles complexes (telle que celui de la classe Itérateur). En outre, nous avons proposé une nouvelle technique permettant de vérifier que les spécifications d'un programme sont correctes en utilisant les protocoles.
La seconde analyse permet de montrer qu'une formule en logique de séparation n'implique pas une autre formule. Cela est utile dans les vérificateurs de programmes car ceux-ci doivent fréquemment démontrer des implications entre formules. L'intérêt de cette analyse est que sa complexité est basse : cela permet de l'utiliser souvent sans consommer beaucoup de ressources.
La troisième analyse permet de paralléliser automatiquement des programmes. Cette analyse prend en entrée des programmes prouvés en logique de séparation et rend en sortie des programmes parallélisés, optimisés, et prouvés. Notre analyse utilise la sémantique de séparation de l'opérateur "*" pour détecter quand deux sous programmes accèdent à des parties disjointes du tas. Dans ce cas, la parallélisation est possible. L'algorithme de détection est implémenté par un système de réécriture.
22
Ratel, Christophe. "Définition et réalisation d'un outil de vérification formelle de programmes LUSTRE." Phd thesis, Grenoble 1, 1992. http://tel.archives-ouvertes.fr/tel-00341223.
Анотація:
Lustre est un langage de programmation spécialement conçu pour la réalisation des systèmes réactifs. Le besoin de garantir que ces systèmes ont un comportement conforme a celui attendu nécessite de définir et de mettre en œuvre des méthodes de vérification formelle des programmes lustre, qui sont relatées dans cette thèse. La vérification d'un système consiste a contrôler que tous ses comportements sont corrects vis-a-vis de ses spécifications. Les comportements d'un programme lustre peuvent classiquement être représentés par une machine d'états finis, dont la génération permet de vérifier ses spécifications. La methode standard mettant en œuvre ce principe est limitée par le probleme d'explosion de la machine générée, qui n'est pas minimale. Un nouvel algorithme évitant ce probleme est présenté. Son implémentation nécessite l'emploi d'une technique de représentation et de manipulation symbolique de la machine (bdds), dont le cout d'utilisation est largement abaisse grâce a de nombreuses optimisations. Basées sur cette technique, deux autres implémentations originales de la methode standard et de la nouvelle methode proposée ci-dessus sont décrites. Les aspects de diagnostic correspondant au cas ou les programmes sont incorrects vis-a-vis de leurs spécifications sont aussi abordes
23
Botbol, Vincent. "Analyse statique de programmes concurrents avec variables numériques." Electronic Thesis or Diss., Sorbonne université, 2018. https://accesdistant.sorbonne-universite.fr/login?url=https://theses-intra.sorbonne-universite.fr/2018SORUS390.pdf.
Анотація:
La vérification de systèmes distribués est un problème complexe pour de nombreuses raisons tant théoriques que pratiques, en particulier lorsque ces systèmes sont capables d'effectuer localement des calculs numériques. Le but de cette thèse est de proposer une méthode de vérification formelle de tels systèmes. Nous présentons un modèle général, basé sur l'interprétation abstraite, permettant de construire des analyses statiques pour des systèmes de processus communiquants. Notre méthodologie s'inspire du Regular Model Checking en représentant des ensembles d'états de programmes concurrents sous la forme d'automates de treillis et la sémantique de ces programmes comme la réécriture des langages reconnus par ces automates. Ce modèle nous permet notamment d'exprimer des communications entre processus et des créations/destructions dynamiques de processus. L'utilisation de l'interprétation abstraite nous permet d'obtenir une sur-approximation sûre de l'espace d'atteignabilité des programmes nous permettant ainsi de vérifier des propriétés de sûreté numériques. Nous avons implanté cette méthode permettant d'analyser automatiquement des programmes utilisant la bibliothèque logicielle de calculs distribués MPI/CVerifying distributed systems is a difficult problem on both theoretical and practice levels, in particular when systems are capable of local numerical computations. The goal of this thesis is to provide a formal verification method of such systems. We present a general model, based on abstract interpretation, allowing the construction of static analyses for systems of communicating processes. Our methodology is inspired by Regular Model Checking where the set of program states are represented as lattice automata and the program semantics are encoded using rewriting systems applied on the language recognized by the automata. This model offers the possiblity of expressing communications between processes as well as dynamic creation/destruction of process. Using the abstract interpretation methodology, we are able to provide a sound over-approximation of the reachability set of programs allowing us to verify numerical safety properties. We implemented this method allowing us to automatically analyse programs that use the distributed computation library MPI/C
24
Ben, Ahmed Daho Okacha. "Vérification de programmes de commande numérique pour l'usinage de poches : une application du partitionnement du plan." Limoges, 1998. http://www.theses.fr/1998LIMO0020.
Анотація:
L'emulation logicielle des directeurs de commande numerique des machines-outils est un moyen efficace pour faciliter la mise au point de programmes piece et leur validation. Ces derniers sont verifies, mais aussi optimises, au moyen d'une serie de tests geometriques et technologiques. Pour affiner cette validation, nous proposons un ensemble d'applications liees a l'usinage de poches, une tache frequemment rencontree dans la fabrication de pieces mecaniques. Nous avons pour cela procede a la modelisation geometrique des trajectoires de l'outil de coupe par application du partitionnement du plan. Un graphe planaire decrivant les informations geometriques et topologiques implicitement definies par les trajectoires de l'outil est obtenu. L'utilisation de cette methode connue de la geometrie algorithmique a cependant necessite dans notre contexte industriel l'elaboration de traitements specifiques. D'une part, afin de determiner les points d'intersection dans le cas des chevauchements (complet ou incomplet) entre les aretes, et d'autre part, afin de modeliser les configurations geometriques de l'usinage qui sont a l'origine de la non connexite du graphe decrivant le partitionnement. Ainsi une representation complete des trajectoires de l'outil (traces) est obtenue. Afin de quantifier les recouvrements des surfaces balayees par l'outil, nous avons introduit le concept d'histoire d'une cellule du partitionnement. Pour chaque region de la poche, le nombre de passages de l'outil est determine. Ainsi, nous avons donne a la representation geometrique des regions de la poche une semantique liee a l'usinage. Ce concept nous permis de determiner la quantite de matiere enlevee le long d'une trajectoire, les passes d'usinage a vide et la variation de la largeur radiale le long de la trajectoire globale de l'outil. Nous avons propose aussi l'extraction de caracteristiques de forme a partir du modele geometrique de la piece usinee. Enfin, pour mettre en evidence la complexite globale de l'algorithme, nous etudions les complexites des differentes etapes de construction du partitionnement. Puis, nous procedons a une evaluation experimentale en presentant differents resultats concernant des exemples realistes issus d'un systeme de cfao.
25
Bouyer-Decitre, Patricia. "Modèles et algorithmes pour la vérification des systèmes temporisés." Cachan, Ecole normale supérieure, 2002. http://www.theses.fr/2002DENS0008.
26
Kanig, Johannes. "Spécification et preuve de programmes d'ordre supérieur." Paris 11, 2010. http://www.theses.fr/2010PA112183.
Анотація:
Nous présentons d'abord un système théorique permettant la preuve de programmes d'ordre supérieur avec etfets de bord. Ce système est constitué de trois composantes majeures. D'abord un langage de programmation avec un système à effets, avec polymorphisme d'etfets, permettant une analyse fine des effets. Ensuite, un langage de spécitication d'ordre supérieur qui contient aussi un moyen de parler des évolutions d'états. Enfin, un calcul de plus faibles préconditions, permettant d'obtenir, à partir d'un programme annoté, des obligations de preuve, c'est-à-dire des formules dont la validité implique la correction du programme. Nous présentons également deux restrictions du système initial : la première interdit l'aliasing entre régions, ce qui garantit la modularité des spécifications : la deuxième restreint chaque région à un singleton, ne contenant qu'une seule référence. Les deux restrictions permettent de simplifier les obligations générées, mais restreignent l'ensemble des programmes acceptés. Nous présentons une implantation du système théorique. Cet outil repose notamment sur des traductions des obligations de preuve vers la logique d'ordre supérieur et la logique du premier ordre. La première traduction permet notamment l'utilisation de l'assistant de preuve Coq pour valider les obligations de preuve. La traduction vers la logique du premier ordre permet, quant à elle, l'utilisation de démonstrateurs automatiques. Des programmes d'ordre supérieur, entre autres de la bibliothèque standard d'OCaml, sont prouvés correct, ainsi qu'une implémentation à base de continuations de l'algorithme de Koda-RuskeyLn this thesis, we first present a theoretical system that enables proof of higher-order programs with side effects. This system consists of three major parts. First, a programming language with a traditional type, effect and region system, with effect polymorphism. Second, a higher-order specification language, that also contains a means to describe modifications of the state. Finally, a weakest precondition calcul us that, starting from an annotated program, allows to obtain proof obligations, that is, formulas whose validity implies the correctness of the program w. R. T. Its specification. We also present two restrictions of the initial system. The first disallows region aliasing, obtaining better modularity of the calculus, the second restricts the system to regions that are singleton, containing only a single reference. Both restrictions enable important simplifications that can be applied to proof obligations, but restrict the set of accepted programs. We also present an implementation of this theoretical system, called Who. This tool uses in particular translations of the proof obligations to higher-order logic and first-order logic; these translations are detailed in this thesis. The translation to higher-order logic in particular allows using the Coq proof assistant to validate proof obligations. The translation to first-order logic allows using automated theorem provers. Higher-order programs, found in the standard library of OCaml and elsewhere, have been proved correct using the tool Who, as well as a continuation-based implementation of the Koda-Ruskey algorithm
27
Kunz, César. "Préservation des preuves et transformation de programmes." Phd thesis, École Nationale Supérieure des Mines de Paris, 2009. http://pastel.archives-ouvertes.fr/pastel-00004940.
Анотація:
Le paradigme du code mobile implique la distribution des applications par les producteurs de code à environnements hétérogènes dans lesquels elles sont exécutées. Une pratique étendue de ce paradigme est constituée par le développement d'applications telles que les applets ou les scripts Web, transferés à travers un réseau non sécurisé comme Internet à des systèmes distants, par exemple un ordinateur, un téléphone mobile ou un PDA (Assistant personnel). Naturellement, cet environnement peux ouvrir la porte au déploiement de programmes malveillants dans des plateformes distantes. Dans certains cas, la mauvaise conduite du code mobile ne constitue pas un risque grave, par exemple lorsque l'intégrité des données affectées par l'exécution n'est pas critique ou lorsque l'architecture d'exécution impose de fortes contraintes sur les capacités d'exécution du code non sécurisé. Il y a toujours, toutefois, des situations dans lesquelles il est indispensable de vérifier la correction fonctionnelle du code avant son exécution, par exemple lorsque la confidentialité de données critiques comme l'information des cartes de crédit pourrait être en danger, ou lorsque l'environnement d'exécution ne possède pas un mécanisme spécial pour surveiller la consommation excessive des ressources. George Necula a proposé une technique pour apporter de la confiance aux consommateurs sur la correction du code sans faire confiance aux producteurs. Cette technique, Proof Carrying Code (PCC), consiste à déploier le code avec une preuve formelle de sa correction. La correction est une propriété inhérente du code reçuu qui ne peut pas être directement déduite du producteur du code. Naturellement, cela donne un avantage à PCC quant-aux méthodes basées sur la confiance à l'autorité d'un tiers. En effet, une signature d'une autorité ne suffit pas à fournir une confiance absolue sur l'exécution du code reçu. Depuis les origines du PCC, le type de mécanisme utilisé pour générer des certificats repose sur des analyses statiques qui font partie du compilateur. Par conséquent, en restant automatique, il est intrinsèquement limité à des propriétés très simples. L'augmentation de l'ensemble des propriétés à considerer est difficile et, dans la plupart des cas, cela exige l'interaction humaine. Une possibilité consiste à vérifier directement le code exécutable. Toutefois, l'absence de structure rend la vérification du code de bas niveau moins naturelle, et donc plus laborieuse. Ceci, combiné avec le fait que la plupart des outils de vérification ciblent le code de haut niveau, rend plus appropriée l'idée de transferer la production de certificats au niveau du code source. Le principal inconvénient de produire des certificats pour assurer l'exactitude du code source est que les preuves ne comportent pas la correction du code compilé. Plusieurs techniques peuvent etre proposées pour transférer la preuve de correction d'un programme à sa version exécutable. Cela implique, par exemple, de déployer le programme source et ses certificats originaux (en plus du code exécutable) et de certifier la correction du processus de compilation. Toutefois, cette approche n'est pas satisfaisante, car en plus d'exiger la disponibilité du code source, la longueur du certificat garantissant la correction du compilation peut être prohibitive. Une alternative plus viable consiste à proposer un mécanisme permettant de générer des certificats de code compilé à partir des certificats du programme source. Les compilateurs sont des procédures complexes composées de plusieurs étapes, parmi lesquelles le programme original est progressivement transformé en représentations intermédiaires. Barthe et al. et Pavlova ont montré que les certificats originaux sont conservés, à quelques différences près non significatives, par la première phase de compilation: la compilation non optimale du code source vers une représentation non structurée de niveau intermédiaire. Toutefois, les optimisations des compilateurs sur les représentations intermédiaires représentent un défi, car a priori les certificats ne peuvent pas être réutilisés. Dans cette thèse, nous analysons comment les optimisations affectent la validité des certificats et nous proposons un mécanisme, Certificate Translation, qui rend possible la génération des certificats pour le code mobile exécutable à partir des certificats au niveau du code source. Cela implique transformer les certificats pour surmonter les effets des optimisations de programme.
28
Le, Viet Hoang. "Une couverture combinant tests et preuves pour la vérification formelle." Thesis, Toulouse, ISAE, 2019. http://www.theses.fr/2019ESAE0023/document.
Анотація:
Actuellement, le développement d’un logiciel de taille industriel repose généralement surdes tests ou des preuves unitaires pour garantir rigoureusement ses exigences. En outre, il adéjà été montré que l’utilisation combinée du test et de la preuve unitaires est plus efficaceque l’utilisation d’une seule de ces deux techniques. Néanmoins, un ingénieur en vérificationhésite encore à utiliser ces deux techniques conjointement, faute d’une notion de couverturecommune au test et à la preuve. Définir une telle notion est l’objet de cette thèse.En effet, nous introduisons une nouvelle couverture, appelée « couverture label-mutant ».Elle permet de représenter les critères de couverture structurelle habituels du test, comme lacouverture des instructions, la couverture des branches ou la couverture MC/DC et de décidersi le critère choisi est satisfait en utilisant une technique de vérification formelle, qu’elle soitpar test, par preuve ou par une combinaison des deux. Elle permet également de représenterles critères de couverture fonctionnelle. Nous introduisons aussi dans cette thèse une méthodereposant sur des outils automatiques de test et de preuve pour réduire l’effort de vérificationtout en satisfaisant le critère de couverture choisi. Cette méthode est mise en oeuvre au seinde la plateforme d’analyse de code C (Frama-C), fournissant ainsi à un ingénieur un moyenopérationnel pour contrôler et réaliser la vérification qu’il souhaiteCurrently, industrial-strength software development usually relies on unit testing or unitproof in order to ensure high-level requirements. Combining these techniques has already beendemonstrated more effective than using one of them alone. The verification engineer is yetnot been to combine these techniques because of the lack of a common notion of coverage fortesting and proving. Defining such a notion is the main objective of this thesis.We introduce here a new notion of coverage, named « label-mutant coverage ». It subsumesmost existing structural coverage criteria for unit testing, including statement coverage,branch coverage or MC/DC coverage, while allowing to decide whether the chosen criterionis satisfied by relying on a formal verification technique, either testing or proving or both.It also subsumes functional coverage criteria. Furthermore, we also introduce a method thatmakes use of automatic tools for testing or proving in order to reduce the verification costwhile satisfying the chosen coverage criterion. This method is implemented inside Frama-C, aframework for verification of C code (Frama-C). This way, it offers to the engineer a way tocontrol and to perform the expected verifications
29
Clochard, Martin. "Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels." Thesis, Université Paris-Saclay (ComUE), 2018. http://www.theses.fr/2018SACLS071/document.
Анотація:
Cette thèse se positionne dans le domaine de la vérification déductive de programmes, qui consiste à transformer une propriété à vérifier sur un programme en un énoncé logique, pour ensuite démontrer cet énoncé. La vérification effective d'un programme peut poser de nombreuses difficultés pratiques. En fait, les concepts mis en jeu derrière le programme peuvent suffire à faire obstacle à la vérification. En effet, certains programmes peuvent être assez courts et n'utiliser que des constructions simples, et pourtant s'avérer très difficiles à vérifier. Cela nous amène à la question suivante: dans le contexte d'un environnement de vérification déductive de programmes basé sur les démonstrateurs automatiques, quelles méthodes appliquer pour réduire l'effort nécessaire à la fois pour spécifier des comportements attendus complexes, ainsi que pour démontrer qu'un programme respecte ces comportements attendus? Pour mener notre étude, nous nous sommes placés dans le cadre de l'environnement de vérification déductive de programmes Why3. La vérification de programmes en Why3 est basée sur la génération de conditions de vérification, et l'usage de démonstrateurs externes pour les prouver, que ces démonstrateurs soient automatiques ou interactifs. Nous avons développé plusieurs méthodes, certaines générales et d'autres spécifiques à des classes de programmes, pour réduire l'effort manuel. Nos contributions sont les suivantes. Tout d'abord, nous ajoutons des fonctionnalités à Why3 pour assister le processus de vérification, notamment un mécanisme léger de preuve déclarative basé sur la notion d'indicateurs de coupures. Ensuite, nous présentons une méthode de vérification d'absence de débordement arithmétique pour une classe d'utilisation des entiers difficile à traiter par les méthodes standards. Enfin, nous nous intéressons au développement d'une bibliothèque générique pour la spécification et la preuve de programmes générateurs de codeThis thesis is set in the domain of deductive verification of programs, which consists of transforming a property to be verified about a program into a logical statement, and then proving this statement. Effective verification of a program can pose many practical difficulties. In fact, the concepts behind the program may be sufficient to impede verification. Indeed, some programs can be quite short and use only simple constructions, and yet prove very difficult to verify. This leads us to the following question: in the context of a deductive program verification environment based on automatic provers, what methods can be applied to reduce the effort required both to specify complex behaviors, as well as to prove that a program respects these expected behaviors? To carry out our study, we placed ourselves in the context of the deductive verification environment of programs Why3. The verification of programs in Why3 is based on the generation of verification conditions, and the use of external provers to prove them, whether these provers are automatic or interactive. We have developed several methods, some general and others specific to some program classes, to reduce manual effort. Our contributions are as follows. First, we add features to Why3 to assist the verification process, including a lightweight declarative proof mechanism based on the notion of cut indicators. Then we present a method for checking the absence of arithmetic overflow, for use cases which are difficult to process by standard methods. Finally, we are interested in the development of a generic library for the specification and proof of code generating programs
30
Petiot, Guillaume. "Contribution à la vérification de programmes C par combinaison de tests et de preuves." Thesis, Besançon, 2015. http://www.theses.fr/2015BESA2045/document.
Анотація:
La vérification de logiciels repose le plus souvent sur une spécification formelle encodant les propriétés du programme à vérifier. La tâche de spécification et de vérification déductive des programmes est longue et difficile et nécessite une connaissance des outils de preuve de programmes. En effet, un échec de preuve de programme peut être dû à une non-conformité du code par rapport à sa spécification, à un contrat de boucle ou de fonction appelée trop faible pour prouver une autre propriété, ou à une incapacité du prouveur. Il est souvent difficile pour l’utilisateur de décider laquelle de ces trois raisons est la cause de l’échec de la preuve car cette information n’est pas (ou rarement) donnée par le prouveur et requiert donc une revue approfondie du code et de la spécification. L’objectif de cette thèse est de fournir une méthode de diagnostic automatique des échecs de preuve afin d’améliorer le processus de spécification et de preuve des programmes C. Nous nous plaçons dans le cadre de la plate-forme d’analyse des programmes C FRAMA-C, qui fournit un langage de spécification unique ACSL, un greffon de vérification déductive WP et un générateur de tests structurels PATHCRAWLER. La méthode que nous proposons consiste à diagnostiquer les échecs de preuve en utilisant la génération de tests structurels sur une version instrumentée du programme d’origineSoftware verification often relies on a formal specification encoding the program properties to check. Formally specifying and deductively verifying programs is difficult and time consuming and requires some knowledge about theorem provers. Indeed, a proof failure for a program can be due to a noncompliance between the code and its specification, a loop or callee contrat being insufficient to prove another property, or a prover incapacity. It is often difficult for the user to decide which one of these three reasons causes a given proof failure. Indeed, this feedback is not (or rarely) provided by the theorem prover thus requires a thorough review of the code and the specification. This thesis develops a method to automatically diagnose proof failures and facilitate the specification and verification task. This work takes place within the analysis framework for C programs FRAMAC, that provides the specification language ACSL, the deductive verification plugin WP, and the structural test generator PATHCRAWLER. The proposed method consists in diagnosing proof failures using structural test generation on an instrumented version of the program under verification
31
Guider, Romain. "Analyse statique de programmes Java [et] application à la parallélisation." Nice, 2000. http://www.theses.fr/2000NICE5434.
Анотація:
Nous proposons une analyse statique de programmes à objets par interprétation abstraite. L'analyse de programmes à objets comporte deux particularités que nous traitons séparément : l'analyse du flot de contrôle et la représentation des graphes d'objets. Dans un premier temps, nous présentons une analyse de flot de contrôle paramétrée par une représentation abstraite de graphes d'objets. Cette analyse est générique et peut servir de base à de nombreuses applications. De plus, elle est conçue par interprétation abstraite ce qui nous permet de montrer sa correction sous certaines hypothèses qui portent sur le domaine employé pour représenter les graphes d'objets. Nous dérivons de notre interpréteur abstrait une présentation des problèmes d'analyse statique sous la forme d'un système d'équations et nous prouvons que ce système d'équations est équivalent à l'interpréteur abstrait. La présentation sous cette forme permet de résoudre efficacement les problèmes d'analyse en utilisant des stratégies d'itérations de point fixe sophistiquées (et aussi d'utiliser des solveurs génériques) et de limiter le nombre de calculs qui est fait [sic] pendant les itérations de point fixe en les reportant sur la phase de construction du système d'équation (. . . ). Dans un second temps nous instancions notre analyseur statique en utilisant un domaine abstrait pour les graphes d'objets qui est dû à Sagiv, Reps et Wilhelm. Nous étendons ce domaine pour construire une analyse interprocédurale (. . . ). Enfin, nous décrivons une application de l'analyse statique à la parallélisation et à la distribution de programmes à objets (. . . ).
32
Evangelista, Sami. "Méthodes et outils de vérification pour les réseaux de Petri de haut niveau : Application à la vérification de programmes Ada concurrents." Paris, CNAM, 2006. http://www.theses.fr/2006CNAM0543.
Анотація:
Cette thèse s'inscrit dans le cadre de la vérification automatique de programmes concurrents basée sur un modèle formel intermédiaire, les réseaux de Petri colorés. Nous nous attachons particulièrement à définir, ou adapter, des méthodes qui visent à lutter contre le phénomène d'explosion combinatoire induit par les algorithmes d'exploration du graphe d'accessibilité. Nous oeuvrons pour cela à deux niveaux : au niveau structurel, par des techniques d'abstraction du modèle, et au niveau sémantique, par des techniques de réduction du graphe d'accessibilité du système. Afin de valider l'intérêt pratique des techniques proposées nous les avons implantées dans deux outils : Helena un model checker pour les réseaux de Petri de haut niveau et Quasar une plate-forme pour la validation de programmes Ada concurrentsThis thesis enters in the frame of the automatic verification of concurrent software based on an intermediary formal language, colored Petri nets. We particularly endeavor to define, or adapt, methods which aim at tackling the state explosion induced by an exhaustive exploration of the state space. We work at two levels : at a structural level, by defining some automatic automatic abstraction rules of the model, and at a semantic level, by reducing the reachabiblity graph of the system. In order to validate the practical interest of the proposed techniques we implemented them in two tools: Helena a model checker for high level Petri nets and Quasar, a platform for the verification of concurrent Ada software
33
Munch-Maccagnoni, Guillaume. "Syntaxe et modèles d'une composition non-associative des programmes et des preuves." Phd thesis, Université Paris-Diderot - Paris VII, 2013. http://tel.archives-ouvertes.fr/tel-00918642.
Анотація:
La thèse contribue à la compréhension de la nature, du rôle et des mécanismes de la polarisation dans les langages de programmation, en théorie de la preuve et dans les modèles catégoriels. La polarisation correspond à l'idée que la condition d'associativité de la composition peut être relâchée, comme on le montre à travers un résultat qui relie les duploïdes, notre modèle direct de la polarisation, aux adjonctions. En conséquence, la polarisation sous-tend de nombreux modèles du calcul, ce que l'on souligne encore en montrant comment les modèles par passage de continuation pour des opérateurs de contrôle délimité se décomposent en trois étapes fondamentales. Elle explique également des phénomènes de constructivité en théorie de la démonstration, ce que l'on illustre en donnant une interprétation selon le principe de la formule comme type à la polarisation en général et à une négation involutive en particulier. Notre approche est basée sur une représentation interactive des démonstrations et des programmes à base de termes (calcul L), qui met en évidence la structure des polarités. Celle-ci est basée sur la correspondance entre les machines abstraites et les calculs de séquents, et vise à synthétiser diverses directions : la modélisation du contrôle, de l'ordre d'évaluation et des effets dans les langages de programmation, la quête d'un lien entre la dualité catégorielle et les continuations, et l'approche interactive de la constructivité en théorie de la preuve. On introduit notre technique en supposant uniquement une connaissance élémentaire du λ-calcul simplement typé et de la réécriture.
34
Munch, Guillaume. "Syntaxe et modèles d'une composition non-associative des programmes et des preuves." Paris 7, 2013. http://www.theses.fr/2013PA077130.
Анотація:
La thèse contribue à la compréhension de la nature, du rôle et des mécanismes de la polarisation dans les langages de programmation, en théorie de la preuve et dans les modèles catégoriels. La polarisation correspond à l'idée que la condition d'associativité de la composition peut être relâchée, comme on le montre à travers un résultat qui relie les duploïdes, notre modèle direct de la polarisation, aux adjonctions. En conséquence, la polarisation sous-tend de nombreux modèles du calcul, ce que l'on souligne encore en montrant comment les modèles par passage de continuation pour des opérateurs de contrôle délimité se décomposent en trois étapes fondamentales. Elle explique également des phénomènes de constructivité en théorie de la démonstration, ce que l'on illustre en donnant une interprétation selon le principe de la formule comme type à la polarisation en général et à une négation involutive en particulier. Notre approche est basée sur une représentation interactive des démonstrations et des programmes à base de termes (calcul L), qui met en évidence la structure des polarités. Celle-ci est basée sur la correspondance entre les machines abstraites et les calculs de séquents, et vise à synthétiser diverses directions: la modélisation du contrôle, de l'ordre d'évaluation et des effets dans les langages de programmation, la quête d'un lien entre la dualité catégorielle et les continuations, et l'approche interactive de la constructivité en théorie de la preuve. On introduit notre technique en supposant uniquement une connaissance élémentaire du lambda-calcul simplement typé et de la réécritureThe thesis is a contribution to the understanding of the nature, role, and mechanisms of polarisation in programming languages, proof theory and categorical models. Polarisation corresponds to the idea that we can relax the associativity of composition, as we show by relating duploids, our direct model of polarisation, to adjunctions. As a consequence, polarisation underlies many models of computation, which we further show by decomposing continuation-passing-style models of delimited control in three fondamental steps which allowing us to reconstruct four call-by-name variants of the shift and reset operators. It also explains constructiveness-related phenomena in proof theory, which we illustrate by providing a formulae-as-types interpretation for polarisation in general and for an involutive negation in particular. The cornerstone of our approach is an interactive term-based représentation of proofs and programs (L calculi) which exposes the structure of polarities. It is based on the correspondence between abstract machines and sequent calculi, and it aims at synthesising various trends: the modelling of control, evaluation order and effects in programming languages, the quest for a relationship between categorical duality and continuations, and the interactive notion of construction in proof theory. We give a gentle introduction to our approach which only assumes elementary knowledge of simply-typed lambda calculus and rewriting
35
Hubert, Thierry. "Analyse statique et preuve de programmes industriels critiques." Paris 11, 2008. http://www.theses.fr/2008PA112061.
Анотація:
Dans cette thèse, nous avons contribué au développement de la plate-forme Why afin de fournir une méthode de preuve de la sûreté des programmes industriels critiques. Dans un premier temps, cette thèse présente la plate-forme Why telle qu'elle existait. Cette plate-forme, basée sur le calcul de plus faible pré-condition, s'utilise directement sur le code source et fournit en sortie les conditions de vérification qui doivent être validées pour assurer la sûreté du programme. La première contribution consiste à montrer la méthode de fonctionnement de cette plate-forme en effectuant la preuve d'un programme mettant en {\oe}uvre un algorithme complexe sur les graphes : Schorr-Waite. La deuxième contribution consiste en une analyse de séparation des pointeurs. Cette analyse, basée sur une séparation en régions de la mémoire, est une analyse par typage, donc entièrement statique. La troisième contribution consiste en une analyse de simplification des conditions de vérification. En effet, les conditions de vérification contiennent souvent plein d'hypothèses inutiles à la validation de celles-ci. Pour résoudre ce problème une analyse de pertinence des hypothèses a été développé afin de simplifier les conditions de vérification. Cette thèse se termine sur l'étude de cas d'un programme industriel critique développé chez Dassault Aviation afin de valider notre approcheIn this thesis, we contributed to the development of the Why platform to design a proof method for the safety of critical industrial programs. At first, this thesis presents the platform Why such as it existed before the thesis. This platform, based on the calculus of weakest precondition, is directly used on the source code and generates the verification conditions which must be validated to ensure the program safety. The first contribution is a case study of proof of a program implementing a complex algorithm on graphs: Schorr-Waite. The second contribution consists of a separation analysis of pointers. This analysis, based on a separation in regions of the memory, is a type-based analysis, thus completely static. The third contribution consists of a method of simplification of the verification conditions. Indeed, the verification conditions often contain a large number of hypotheses that are useless for the validation of them. To resolve this problem an analysis of relevance of the hypotheses was developed to simplify the verification conditions. This thesis ends with the case study of a critical industrial program developed at Dassault Aviation to validate our approach
36
Jeannet, Bertrand. "Partitionnement dynamique dans l'analyse de relations linéaires et application à la vérification de programmes synchrones." Grenoble INPG, 2000. http://www.theses.fr/2000INPG0074.
Анотація:
Ce travail porte sur la verification, par des methodes algorithmiques, de proprietes de surete de systemes synchrones ou plus generalement reactifs, presentant a la fois des aspects booleens et numeriques. Il propose une technique originale permettant d'augmenter tres sensiblement la taille des systemes verifies. Nous commencons par rappeler le cadre theorique utilise, qui est celui de l'interpretation abstraite, et une de ses applications, l'analyse de relations lineaires, qui permet d'inferer des relations lineaires liant les variables numeriques d'un programme en ses points de controle. Cette analyse a ete appliquee a la verification de programmes synchrones numeriques et de systemes hybrides lineaires. Dans ce contexte, deux problemes se posent : le premier est que la structure de controle explicite de ces systemes est souvent de taille prohibitive, et le deuxieme est que la precision de l'analyse est quelquefois insuffisante pour la preuve de certaines proprietes. Ces deux problemes s'averant lies, nous proposons une solution pour obtenir un compromis entre complexite et precision, consistant a utiliser un domaine abstrait combinant proprietes booleennes et numeriques, et a se servir d'une structure de controle pour ajuster la precision de l'analyse. Celle-ci se sert de la propriete a montrer pour raffiner automatiquement une structure de controle initiale grossiere, jusqu'a ce que la precision obtenue permette de conclure a la preuve de la propriete. Un outil de verification fonde sur ces principes a ete developpe et experimente sur plusieurs exemples significatifs, et pour certains d'entre eux inabordables par d'autres techniques automatiques existantes.
37
Zinelabdine, Aoufa. "Modélisation des programmes d'investissement : méthodologie et étude de cas." Châtenay-Malabry, Ecole centrale de Paris, 1986. http://www.theses.fr/1986ECAP0016.
Анотація:
On étudie les modèles de planification et de sélection de projets industriels, on en présente une application au secteur mondial des phosphates et on met l'accent sur une réflexion méthodologique de modélisation et de résolution de problèmes spécifiques que l'on rencontre lors de l'utilisation de ces modèles. Ces aspects concernent le passage du modèle statique au modèle dynamique, la démarche d'agrégation des données, la résolution des phénomènes d'échelle, et la stratégie d'élaboration des scenarios. L'application de ce type de modèle a permis de dégager des résultats numériques concernant l'industrie mondiale des phosphates permettant de prendre des décisions d'investissements
38
Baro, Sylvain. "Conception et implémentation d'un système d'aide à la spécification et à la preuve de programmes ML." Phd thesis, Université Paris-Diderot - Paris VII, 2003. http://tel.archives-ouvertes.fr/tel-00008416.
Анотація:
Pouvoir vérifier la conformité d'un programme avec sa spécification représente un enjeu important. On peut utiliser un assistant de preuve : un logiciel permettant la description du problème, la construction des preuves et leur vérification. Nous avons implémenté un système où l'utilisateur décrit la spécification du programme dans un formalisme logique ad hoc, donne le programme dans le sous-ensemble fonctionnel de ML (comprenant filtrage, définitions récursives et fonctions partielles), puis construit interactivement les preuves de correction nécessaires pour prouver la validité du programme.
39
Heyd, Barbara. "Application de la théorie des types et du démonstrateur COQ à la vérification de programmes parallèles." Nancy 1, 1997. http://www.theses.fr/1997NAN10291.
Анотація:
Dans cette thèse, nous nous intéressons plus particulièrement à la vérification formelle de programmes parallèles en utilisant des techniques déductives basées sur la preuve de théorèmes. En particulier, nous nous spécifions et vérifions mécaniquement les programmes décrits en UNITY à l'aide de l'assistant de preuves COQ. Nous décrivons tout d'abord la logique sous jacente à l'assistant de preuves COQ, le Calcul des Constructions Inductives. Puis nous introduisons la théorie UNITY en s'attardant plus particulièrement sur les problèmes de sa logique résultant d'une ambiguïté de quantification au niveau des triplets de Hoare. Nous proposons alors une nouvelle logique, extension de la précédente, résolvant ses différents problèmes : une notion de contexte ou d'environnement à un programme apparaît et une nouvelle définition de l'ensemble des états atteignables est donnée. Une fois, la complétude et la correction de cette nouvelle logique démontrées, nous présentons l'outil Coq-UNITY, résultat de l'implémentation de cette nouvelle logique dans l'assistant COQ. Nous illustrons l'outil Coq-UNITY par différents exemples. Les quatre premiers sont la division euclidienne, les lecteurs-rédacteurs, le parking et le contrôleur d'ascenseur. Même si ce sont tous des cas d'école, leur difficulté est croissante. Chacun d'entre eux met, en effet, en évidence un problème particulier soit au niveau des preuves, soit au niveau spécification. Le dernier exemple concerne un protocole de télécommunications, le protocole ABT / DT. Sur cet exemple, nous montrons l'intérêt de la notion de contexte tant au niveau spécification qu'au niveau vérificationThis thesis is an approach to the formaI specification and verification of distributed systems and in particular to the computer assisted verification. In this work, we use the COQ prover to verify concurrent programs and the chosen specification mechanism is the UNITY logic. First, we describe the Calculus of Inductive Constructions, which is the logic used in the Coq prover. Then we introduce the UNITY theory, but we linger over the problems of its logic, due to the ambiguity of quantifications in the Hoare triples. We propose also an extension of the logic, which solves these problems: a program's context is introduced and a new definition for reachable states is given. After the correctness and the completness of this new logic, we present the Coq-UNITY tool, which results of the implementation of this extension in the Coq system. To illustrate the feasibility of our approach, we present several examples of different complexities: the euclidian division, the reader-writer, the parking and the lift control. These four examples are the first case studies. Each of them highlights a particular problem either in proofs or in specifications. A last example describes a telecommunication protocol, namely the ABT/DT protocol. This example shows that the context is an important notion. Once the context is well-defined, it becomes very helpful in the verification
40
Contet, Jean-Michel. "Modèles multi-agents réactifs pour la navigation multi-véhicules : spécification formelle et vérification." Phd thesis, Université de Technologie de Belfort-Montbeliard, 2009. http://tel.archives-ouvertes.fr/tel-00472415.
Анотація:
Cette thèse propose des modèles multi-agents réactifs fondés sur un cadre formel pour la vérification de propriétés et les valider par la simulation et l'expérimentation en considérant la navigation multi-véhicules comme domaine d'application. La navigation multi-véhicules soulève plusieurs problématiques : perception de l'environnement, communication inter-véhicule, évitement d'obstacle, ... Dans ce contexte, nous avons abordé plus particulièrement les aspects suivants : - Concernant la navigation multi-véhicules nous avons abordé deux problèmes spécifiques : la conduite en convoi ou platooning et la navigation autonome. En ce qui concerne la navigation autonome, nous avons mis l'accent sur l'évitement d'obstacles. - Concernant l'approche proposée : nous adoptons les systèmes multi-agents réactifs, dont les interac- tions sont inspirée de la physique. Pour la conduite en convoi, nous proposons un modèle d'interaction basé sur la physique classique. En ce qui concerne l'évitement d'obstacles, nous adoptant un modèle inspiré de la physique statistique. - Nous plaçons les systèmes multi-agents réactifs dans un cadre formel pour la vérification des pro- priétés, compte-tenu des contraintes de sécurité imposées par la classe d'applications cible. Pour faire face à la complexité des modèles, nous proposons une règle et une méthode de vérification compositionnelle. Cela nous a permis de vérifier la satisfaction d'une propriété de sûreté essentielle : la non-collision entre véhicules lors de la conduite en convoi. - Nous abordons également la question de la validation du système multi-agents par la simulation et l'expérimentation : nous avons contribué au développement d'un simulateur de la conduite en convoi et la navigation autonome. Le simulateur prend en compte les caractéristiques physiques des véhicules et est couplé à un outil de visualisation 3D. Nous avons aussi expérimenté nos modèles sur des véhicules tels que le Cycab et le GEM Car.
41
Chapurlat, Vincent. "Vérification et validation de modèles de systèmes complexes: application à la Modélisation d'Entreprise." Habilitation à diriger des recherches, Université Montpellier II - Sciences et Techniques du Languedoc, 2007. http://tel.archives-ouvertes.fr/tel-00204981.
Анотація:
Cette Habilitation à Diriger des Recherches est le fruit des résultats, tant en recherche qu'en enseignement ou en transfert, de mon activité d'enseignant chercheur. Initiée au sein du Laboratoire d'Informatique, de Microélectronique et de Robotique de Montpellier (LIRMM, UMR CNRS/UM2) de 1991 à 1994, cette activité s'est ensuite concrétisée au sein du Laboratoire de Génie Informatique et d'Ingénierie de Production (LGI2P) de l'Ecole des Mines d'Alès où j'exerce depuis 1994.Le travail de recherche entrepris depuis le début du Doctorat en 1991 relève de la thématique de la modélisation de systèmes complexes puis de la vérification et de la validation de ces modèles. Ceci a pour objectif d'assurer, ou à défaut de rassurer, le modeleur sur la qualité des modèles, sur leur pertinence vis-à-vis du système considéré et sur le respect d'exigences qui ont présidé à leur construction. La recherche a donc consisté au développement d'approches de modélisation, de spécification formelle de propriétés, de vérification par preuve de propriétés au moyen de Graphes Conceptuels et de simulation comportementale. Les domaines d'application privilégiés ont été les systèmes de contrôle commande répartis, puis plus largement la modélisation d'entreprise et tentent aujourd'hui d'intégrer une dimension risque dans la modélisation d'entreprise et de s'ouvrir plus largement à l'ingénierie des systèmes complexes. Les résultats sont des langages et un cadre de modélisation intégré, un langage de spécification baptisé LUSP, une suite de mécanismes de preuve formelle et de simulation qui ont donné lieu à divers encadrements de thèses, de travaux et à des transferts vers l'industrie.
Enfin, l'activité d'enseignement a tenté de rester cohérente avec le profil de compétence à la fois de producticien et d'ingénierie système acquis ou inspiré par la thématique de recherche. Elle s'est déroulée dans le cadre de diverses Universités, Ecoles d'Ingénieurs ou de cursus spécialisés. Les résultats sont des propositions et l'accompagnement de thématiques nouvelles, une activité d'ingénierie pédagogique et une implication dans diverses responsabilités administratives.
42
Dreyfus, Alois. "Contributions à la vérification et à la validation efficaces fondées sur des modèles." Thesis, Besançon, 2014. http://www.theses.fr/2014BESA2076/document.
Анотація:
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-YardThe 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
43
Kmimech, Mourad. "Vérification d’assemblages de composants logiciels : Application aux modèles de composants UML2.0 et Ugatze." Pau, 2010. http://www.theses.fr/2010PAUU3017.
Анотація:
L'approche par composants vise la réutilisation par assemblage aisé et cohérent des composants. Mais l’obtention d’un assemblage de composants cohérent n’est pas un exercice facile. Pour y parvenir, nous préconisons une approche contractuelle distinguant divers contrats syntaxiques, structurels, sémantiques, de synchronisation et de qualité de services. Nous avons appliqué avec succès cette approche contractuelle sur deux modèles de composants semi-formels : UML2. 0 et Ugatze. En effet, nous proposons deux démarches VerifComponentUML2. 0 et VerifComponentUgatze. La démarche VerifComponentUML2. 0 vise la vérification des contrats syntaxiques, structurels, de synchronisation et de qualité de services sur une assemblage de composants UML2. 0 en passant par les deux modèles de composants formels Acme/Armani et Wright. VerifComponentUML2. 0 est équipé de deux outils : Wr2fdr et Wright2Ada. L’outil Wr2fdr permet de traduire des Wright vers CSP afin de vérifier les contrats de synchronisation en utilisant le model-checker FDR. L’outil Wright2Ada est un outil IDM permettant de transformer de Wright en Ada afin d’ouvrir UML2. 0 sur les outils d’analyse statique et dynamique associés à Ada. La démarche VerifComponentUgatze offre un cadre permettant de vérifier les contrats syntaxiques et structurels d’un assemblage de composant Ugatze en passant par Acme/ArmaniThe component approach aims for the reuse by a coherent and easy components assembly. But obtaining a coherent components assembly is not an easy exercise. To achieve this, we advocate a contractual approach distinguishing different syntactic, structural, semantic, synchronization and service quality contracts. We have successfully applied this approach on two models of semi-formal contractual components: UML2. 0 and Ugatze. Indeed, we propose two approaches: VerifComponentUML2. 0 and VerifComponentUgatze. The VerifComponentUML2. 0 approach aims the verification of syntactic, structural, synchronization and quality service contracts on a UML2. 0 component assembly through two formal component models Acme/Armani and Wright. VerifComponentUML2. 0 has two tools: Wr2fdr and Wright2Ada. The tool Wr2fdr allows translating Wright to CSP contracts in order to verify synchronization using the model checker FDR. It is a IDM tool Wright2Ada which allow is transforming Wright to Ada, in order to open UML2. 0 on static analysis and dynamic tools associated with Ada. VerifComponentUgatze approach provides a frame allowing to check syntactic and structural contracts of an Ugatze component assembly through Acme/Armani
44
Lewicki, Alexandre. "Conception de modèles haut niveau pour l'optimisation et la vérification de systèmes Bluetooth." Nice, 2008. http://www.theses.fr/2008NICE4110.
Анотація:
Les différents travaux de recherche présentés dans cette thèse portent sur la conception de modèles fonctionnels à haut niveau d’abstraction ainsi que leur utilisation dans un flot de conception de systèmes sans fil. La Méthodologie de Conception des Systèmes Embarqués (MCSE) a été expérimentée pour la conception des circuits et systèmes dédiés à la technologie Bluetooth. La première partie de la thèse présente la méthodologie MCSE et son application dans la conception d’un système comportant un capteur de température distant et relié par Bluetooth. A partir des spécifications de l’application, les modèles fonctionnels ont été élaborés et raffinés après différentes étapes successives. Les modèles ont ensuite été traduits à l’aide de SystemC, une librairie C++ permettant de décrire les systèmes aux niveaux matériels et logiciels. Les modèles ont ensuite été exploités dans le cadre de simulation de réseaux sans fil. Ces résultats peuvent être utilisés suivant 3 différents axes : l’analyse de protocole, l’analyse de performances et l’exploration d’architecture. La deuxième partie du travail a été d’introduire les modèles fonctionnels dans le cadre d’un environnement de vérification matérielle avant fabrication. Deux environnements ont été mis en place pour les concepteurs du circuit ainsi que pour les ingénieurs de vérification. Cette technique permet de simuler et stresser le circuit de manière plus avancée, notamment grâce à la possibilité d’écrire des tests plus completsThe different works conducted in this thesis were to design high level functional models that were used in a wireless system design flow. The MCSE methodology was followed to design those models and the results have been used for Bluetooth technology system design and verification. The first part of the work presents the MCSE methodology that has been used for the design of the models. Starting from the specification of a concrete use case, a temperature sensor, we designed a functional model of the system with successive refinement steps. The models were then translated in SystemC, a C++ library that allows describing both hardware and software parts of a system. The results of the exploitation of the models in a wireless network simulation can be used for protocol analysis, performance analysis and performance exploration. The second part of the work was to introduce the functional models in a hardware verification environment. Two different techniques for design engineers and verification engineers have been settled. This technique brings enhanced verification features with the possibility to write complex tests
45
Rousset, Nicolas. "Automatisation de la Spécification et de la Vérification d'applications Java Card." Paris 11, 2008. http://www.theses.fr/2008PA112065.
Анотація:
Ce travail concerne la vérification statique de programmes Java Card annotés formellement, par des méthodes déductives. Il contribue à rendre cette approche praticable dans un contexte industriel. Ce travail a donné lieu à des implantations au sein du prototype Krakatoa, et des expérimentations sur des applets industrielles. La première partie concerne le renforcement du degré d'automatisation de l'étape de vérification. La première contribution est l'interprétation fine de traits de la sémantique du langage Java Card: transactions et arrachage de la carte. La deuxième contribution propose une politique de références non-null par défaut qui permet de vérifier la validité des accès mémoire par typage statique. La troisième contribution est une analyse inter-procédurale d'inférence d'annotations par interprétation abstraite, qui permet d'obtenir des invariants de boucle, ainsi que des préconditions et des postconditions de méthodes. La seconde partie concerne la phase amont c'est-à-dire la conception des spécifications. La première contribution propose des liens entre les annotations à la JML et des spécifications abstraites. Des propriétés fonctionnelles sont exprimées à l'aide de spécifications algébriques, dont le lien avec un programme annoté est défini par une relation de raffinement. La deuxième contribution propose une utilisation structurée de diagrammes UML permettant d'engendrer des annotations, pour vérifier des propriétés de sûreté spécifiques (e. G. Invariants de structure, utilisation de protocoles). Enfin, une perspective est ouverte sur la définition et la propagation automatique d'annotations pour aider à l'audit de sécurité des applets Java CardThis work is about static verification of formally-annotated Java Card programs, by deductive methods. It aims at making such an approach practicable in an industrial setting. Implementations have been performed inside the Krakatoa prototype, and experiments were conducted on industrial applets. The first part concerns the improvement of the automation in the verification step. The first contribution is a precise interpretation of the semantics of the Java Card language: transactions and card tear. The second contribution proposes a policy of non-null references, allowing to verify the validity of memory accesses by static typing. The third contribution is an interprocedural analysis for inferring annotations, by abstract interpretation, allowing to obtain loop invariants, and pre- and post-conditions for methods. The second part is about the design of specifications. The first contribution proposes links between JML-like annotations and abstract specifications. Functional properties are expressed using algebraic specifications, whose link with the program is defined by a refinement relation. The second contribution proposes a structured use of UML diagrams allowing to generate annotations, to verify specific safety properties (e. G. Structural invariants, protocol descriptions). Finally, a perspective is opened towards the definition and the automatic propagation of annotations to assist security audits of Java Card applets
46
Lazaar, Nadjib. "Méthodologie et outil de Test, de localisation de fautes et de correction automatique des programmes à contraintes." Rennes 1, 2011. http://www.theses.fr/2011REN1S115.
Анотація:
Le développement des langages de modélisation des programmes à contraintes a eu un grand impact dans le monde industriel. Des langages comme OPL (Optimization Programming Language) de IBM Ilog, Comet de Dynadec, Sicstus Prolog, Gecode, ainsi que d'autres, proposent des solutions robustes aux problèmes du monde réel. De plus, ces langages commencent à être utilisés dans des applications critiques comme la gestion et le contrôle du trafic aérien, le e-commerce et le développement de programmes critiques. D'autre part, il est connu que tout processus de développement logiciel effectué dans un cadre industriel inclut impérativement une phase de test, de vérification formelle et/ou de validation. Par ailleurs, les langages de programmation par contraintes (PPC) ne connaissent pas d'innovations majeures en termes de vérification et de mise au point. Ceci ouvre la voie à des recherches orientées vers les aspects génie logiciel dédiés à la PPC. Notre travail vise à poser les jalons d'une théorie du test des programmes à contraintes pour fournir des outils conceptuels et des outils pratiques d'aide à cette vérification. Notre approche repose sur des hypothèses quant au développement et au raffinement dans un langage de PPC. Il est usuel de démarrer à partir d'un modèle simple et très déclaratif, une traduction fidèle de la spécification du problème, sans accorder un intérêt à ses performances. Par la suite, ce modèle est raffiné par l'introduction de contraintes redondantes ou reformulées, l'utilisation de structures de données optimisées, de contraintes globales, de contraintes qui cassent les symétries, etc. Nous pensons que l'essentiel des fautes introduites est compris dans ce processus de raffinement. Le travail majeur présenté dans la présente thèse est la définition d'un cadre de test qui établit des règles de conformité entre le modèle initial déclaratif et le programme optimisé dédié à la résolution d'instances de grande taille. Par la suite, nous proposons un cadre conceptuel pour la mise-au-point de ce type de programmes avec une méthodologie pour la localisation et la correction automatique des fautes. Nous avons développé un environnement de test, nommé CPTEST, pour valider les solutions proposées, sur des problèmes académiques du monde de la PPC ainsi qu'un problème du monde réel qui est le problème d'ordonnancement des véhiculesThe success of several constraint-based modelling languages such as OPL (Optimization programming Language) of IBM Ilog, COMET of Dynadec, Sicstus Prolog, Gecode, appeals for better software engineering practices, particularly in the testing phase. These languages aim at solving industrial combinatorial problems that arise in optimization, planning, or scheduling. Recently, a new trend has emerged that propose also to use CP programs to address critical applications in e-Commerce, air-traffic control and management, or critical software development that must be thoroughly verified before being used in applications. While constraint program debugging drew the attention of many researchers, few supports in terms of software engineering and testing have been proposed to help verify this kind of programs. In the present thesis, we define a testing theory for constraint programming. For that, we propose a general framework of constraint program development which supposes that a first declarative and simple constraint model is available from the problem specifications analysis. Then, this model is refined using classical techniques such as constraint reformulation, surrogate, redundant, implied and global constraint addition, or symmetry-breaking to form an improved constraint model that must be tested before being used to address real-sized problems. We think that most of the faults are introduced in this refinement step and propose a process which takes the first declarative model as an oracle for detecting non-conformities and derive practical test purposes from this process. Therefore, we enhance the proposed testing framework to introduce a methodology for an automatic tuning with fault localization and correction in constraint programs. We implemented these approaches in a new tool called CPTEST that was used to automatically detect, localize and correct faults on classical benchmark programs and real-world CP problem: the car-sequencing problem
47
Girard, Pierre. "Formalisation et mise en œuvre d'une analyse statique de code en vue de la vérification d'applications sécurisées." Toulouse, ENSAE, 1996. http://www.theses.fr/1996ESAE0010.
Анотація:
Dans le domaine de la sécurité informatique, de nombreux travaux théoriques concernent les modèles et les règlements de sécurité en se situant très en amont des systèmes réellement implémentés. Cette thèse s'appuie sur les bases théoriques offertes par ces travaux pour fonder une méthode de vérification statique de logiciels applicatifs. Nous proposons pour cela des algorithmes d'analyse qui s'appliquent aux programmes sources et nous démontrons qu'ils sont corrects en les dérivant d'un modèle de sécurité formel. Ils sont utilisés concrètement pour analyser des programmes écrits en langage C. Après une présentation de la problématique de sécurité informatique, nous effectuons un inventaire des menaces et des attaques récemment constatées et nous montrons qu'il existe un besoin en matière de validation statique de logiciels existants. Nous proposons ensuite une méthodologie de vérification de programmes écrits en langage C par annotation de leur code source puis analyse automatique de celui-ci. Dans une seconde partie, nous cherchons à démontrer la correction des algorithmes d'analyse. Pour cela, nous partons d'un modèle formel de sécurité : le modèle de la causalité. Nous le modifions pour en faire un modèle calculatoire, puis nous l'appliquons à la sémantique opérationnelle d'un langage impératif. Nous démontrons alors que l'analyse de la sécurité, exprimée comme une sémantique non standard du langage, est correcte par rapport au modèle de sécurité. Nous examinons enfin les difficultés pratiques posées par l'analyse statique du langage C. Nous nous attachons à analyser ses particularités en termes de structures de donnée et de structures de contôle. Nous proposons des techniques pour résoudre les problèmes posés, en particulier par les variables de type pointeur et les instructions déstructurantes de type saut inconditionnel.
48
Benmerzoug, Djamel. "Modèles et outils formels pour l'intégration d'applications d'entreprises." Paris 6, 2009. http://www.theses.fr/2009PA066344.
Анотація:
L'intégration d'applications dépeint les interactions dans lesquelles les processus engagés participent afin d'atteindre un objectif commun, ainsi que les dépendances entre les interactions. En conséquence, cette thèse concerne l'intégration des applications par les processus à l'aide des systèmes multi-agents dits communiquants, c'est-à-dire dont les agents interagissent par l'envoi de messages, en utilisant un langage de communication de haut niveau. Dans ce travail de recherche, nous proposons un cadre conceptuel et une démarche méthodologique couvrant les principales phases pour la modélisation de l'intégration d'applications basée sur les protocoles d'interaction. Cette démarche est basée conjointement sur l'utilisation de la notation AUML, et aussi sur le langage BPEL4WS. Nous définissons par la suite un guide permettant de passer à partir de descriptions semi-formelles des protocoles d'interaction, vers des spécifications formelles de réseaux de Petri colorés (RdPC) tout en mettant l'accent sur le contrôle et la dynamicité des interactions. Le modèle de RdPC permet de couvrir les aspects de modélisation et de validation des protocoles.
49
Schrammel, Peter. "Méthodes logico-numériques pour la vérification des systèmes discrets et hybrides." Phd thesis, Université de Grenoble, 2012. http://tel.archives-ouvertes.fr/tel-00809357.
Анотація:
Cette thèse étudie la vérification automatique de propriétés de sûreté de systèmes logico-numériques discrets ou hybrides. Ce sont des systèmes ayant des variables booléennes et numériques et des comportements discrets et continus. Notre approche est fondée sur l'analyse statique par interprétation abstraite. Nous adressons les problèmes suivants : les méthodes d'interprétation abstraite numériques exigent l'énumération des états booléens, et par conséquent, ils souffrent du probléme d'explosion d'espace d'états. En outre, il y a une perte de précision due à l'utilisation d'un opérateur d'élargissement afin de garantir la terminaison de l'analyse. Par ailleurs, nous voulons rendre les méthodes d'interprétation abstraite accessibles à des langages de simulation hybrides. Dans cette thèse, nous généralisons d'abord l'accélération abstraite, une méthode qui améliore la précision des invariants numériques inférés. Ensuite, nous montrons comment étendre l'accélération abstraite et l'itération de max-stratégies à des programmes logico-numériques, ce qui aide à améliorer le compromis entre l'efficacité et la précision. En ce qui concerne les systèmes hybrides, nous traduisons le langage de programmation synchrone et hybride Zelus vers les automates hybrides logico-numériques, et nous étendons les méthodes d'analyse logico-numérique aux systèmes hybrides. Enfin, nous avons mis en oeuvre les méthodes proposées dans un outil nommé ReaVer et nous fournissons des résultats expérimentaux. En conclusion, cette thèse propose une approche unifiée à la vérification de systèmes logico-numériques discrets et hybrides fondée sur l'interprétation abstraite qui est capable d'intégrer des méthodes d'interprétation abstraite numériques sophistiquées tout en améliorant le compromis entre l'efficacité et la précision.
50
Kamsu-Foguem, Bernard. "Modélisation et vérification des propriétés de systèmes complexes : Application aux processus d'entreprise." Montpellier 2, 2004. http://www.theses.fr/2004MON20050.