Texte remanié de: Thèse de doctorat--Droit--Paris 1, 2005. / Bibliogr. p. 567-623. Index.

Comme les syst`emes mat´eriels et logiciels grandissent de fa¸con continue en ´echelle et fonctionnalit´es, la probabilit´e d’erreurs subtiles de- vient toujours plus grande. Les techniques d’abstraction, souvent bas´ees sur l’interpr´etation abstraite de Cousot, fournissent une m´ethode pour ex´ecuter symboliquement les syst`emes en utilisant le domaine abstrait `a la place du domaine concret. Dans cette th`ese, on introduit des techniques d’abstraction pour les logiques sous des interpr´etations multi-valu´ees. Beaucoup d’applications des logiques multi-valu´ees ont ´et´e trouv´ees dans la v´erification du mat´eriel et du logiciel. Pour la v´erification du mat´eriel, des outils de simulation et des r´ealisations des circuits multi-valu´es v´eritables ont ´et´e propos´es, les risques dynamiques ont ´et´e model´es en introduisant des ´etats faux pour trouver des r´egions chevauchantes des signaux en concurrence, etc. Pour la v´erification du logiciel on a besoin d’incertitude parce qu’on ne peut savoir si certains comportements devraient ˆetre possibles et on a besoin du d´esaccord parce que l’on peut avoir des acteurs diff´erents qui sont en d´esaccord pour la mani`ere dont les syst`emes devraient se comporter. Les abstractions sont obtenues en appliquant des relations d’´equivalence et apr`es, les symboles pr´edicatifs de la logique sont red´efinis `a s’appliquer cor- rectement aux classes d’´equivalence `a l’aide des politiques d’interpr´etation. On fournit des r´esultats de pr´eservation pour la logique de premier ordre, pour la logique temporelle et pour la logique temporelle de la connaissance. Avant de discuter les abstractions multi-valu´ees pour la logique temporelle, nous pr´esentons une ´etude de cas pour utiliser l’abstraction dans le contexte des mod`eles du contrˆole d’acc`es. Nous fournirons aussi une technique d’abstraction pour les types de do- nn´ees. Cette technique d’abstraction peut ˆetre ´elargie pour les types abstraits de donn´ees. Ici, les abstractions sont appliqu´ees aux sp´ecifications initiales au moyen des ´equations et ils sont appel´es des abstractions ´equationnelles. De plus, la technique d’abstraction pr´esent´ee g´en´eralise et clarifie la nature de beaucoup de techniques d’abstraction trouv´ees dans la litt´erature, telles: la technique de dupliquer les symboles pr´edicatifs, shape analysis, l’abstraction par pr´edicats, l’approche de McMillan, etc. Pour raisonner au sujet des syst`emes dynamiques, on introduit les types de donn´ees dynamiques et on ´etend la m´ethode d’abstraction ant´erieure `a ce cas. Le probl`eme principal qui survient quand on utilise les abstractions est de trouver l’abstraction convenable ou de raffiner une abstraction d´ej`a existante pour en obtenir une meilleure. On prouve que les techniques d’abstraction que nous avons introduites pour les types de donn´ees sous l’interpr´etation 3- valu´ee Kleene, peuvent ˆetre utilis´ees dans une proc´edure de raffinement. De plus, on montre que la proc´edure de raffinement guid´e par contre-exemple est plus efficace quand on l’utilise sous les abstractions ´equationnelles / As the hardware and software systems are growing continuously in scale and functionality, the likelihood of subtle errors becomes greater. Abstraction techniques, often based on abstract interpretation, provide a method for symbolically executing systems using the abstract instead of the concrete domain. In this thesis, we are concerned with abstractions for logics under multi-valued interpretations. Many applications of multi-valued logics have been found in hardware and software verification. For hardware verification, simulation tools and imple- mentations of genuinely multi-valued circuits have been proposed, dynamic hazards have been modeled by introducing pseudo states to find overlapping regions of competing signals, implementation of gates have been verified on the basis of switch level models, etc. For software verification, we need uncer- tainty because we may not know whether some behaviors should be possible, we need disagreement because we may have different stakeholders that dis- agree about how the systems should behave and we need to represent relative importance because some behaviors are essential and others may or may not be implemented. The abstractions are obtained by applying equivalence relations and then, the predicate symbols of the logic are re-defined to work properly on equiva- lence classes by using interpretation policies. We provide preservation results for first-order logic, temporal logic, and temporal logic of knowledge. As a case study, we show how abstraction can be used to solve the safety problem for protection systems which model access control policies. The use of abstraction in the context of data types, is also investigated. This technique scales well from data types to abstract data types. Here, abstractions are applied to initial specifications by means of equations and they are called equationally specified abstractions. Moreover, the abstraction technique we propose generalizes and clarifies the nature of many abstraction techniques found in the literature, such as the technique of duplicating pred- icate symbols, shape analysis, predicate abstraction, McMillan’s approach, etc. To reason about dynamic systems, we introduce dynamic data types and extend the previous abstraction technique to this case. The main problem that arises when using abstraction techniques is to find the suitable abstraction or to refine an already existing abstraction in order to obtain a better one. In this thesis, we prove that the abstraction techniques for data types, under Kleene’s three-valued interpretation, can be used in a refinement procedure. Moreover, we show that the counterexample guided abstraction refinement procedure (CEGAR) works better when used with equationally specified abstractions

.

La société moderne est de plus en plus dépendante de l'informatique dont le rôle est devenu tellement vital au point que tout dysfonctionnement peut engendrer des pertes considérables voire des conséquences irréversibles telles que la perte de vies humaines. Pour minimiser les dégâts, plusieurs techniques et outils ont été mis en place au cours des dernières années. Leur objectif est de faire en sorte que nos systèmes informatiques fonctionnent < < ~tout le temps~> > , et ce, tout en produisant les résultats escomptés. La duplication du matériel et les tests de logiciels sont parmi les techniques les plus utilisées. Cependant, sans méthodes formelles, rien n'est garanti et des problèmes peuvent surgir à tout moment. En contrepartie, l'utilisation de méthodes formelles n'est pas à la portée de tout le monde y compris les programmeurs chevronnés et la tâche reste subtile et complexe même pour les spécialistes. Quelques lignes de code nécessitent parfois des centaines de lignes de preuve difficiles à lire et à comprendre. Malgré tout, leur utilisation n'est plus un luxe, mais plutôt nécessaire afin d'éviter les dégâts engendrés par les mauvais fonctionnements de nos systèmes critiques. Le principal objectif de notre recherche est de développer un cadre formel et automatique pour le renforcement de politique de sécurité sur des systèmes concurrents. Plus précisément, l'idée consiste à ajouter dans un programme des tests à des endroits soigneusement calculés pour qu'une politique de sécurité soit respectée. La nouvelle version du programme préserve toutes les traces de la version originale respectant la politique de sécurité et bloque les traces qui ne peuvent plus respecter la politique de sécurité même si elles sont complétées par certains suffixes. Les principaux résultats ayant contribué à l'atteinte de cet objectif sont : 1. La définition d'une algèbre de processus [symbol] offrant un cadre purement algébrique pour le renforcement de politique de sécurité sur des systèmes concurrents. Plus précisément, nous avons défini un nouvel opérateur qui permet de renforcer, d'une manière intuitive, une politique de sécurité sur un système concurrent. 2. La définition d'une logique, dénotée par [symbol], inspirée des expressions régulières étendues. En effet, [symbol] est une logique linéaire qui exprime la classe de langage régulier, mais avec la possibilité d'exprimer des propriétés infinies. 3. La définition d'une algèbre [symbol] basée sur l'algèbre [symbol]. [symbol] définit un nouvel opérateur de renforcement qui tient compte de l'introduction de la logique. 4. Le développement d'une technique d'optimisation qui, pour une certaine classe de propriétés de sécurité, permet de réduire le nombre de tests insérés dans le programme renforcé. / One of the important goals of the software development process is proving that the produced systems always meet their requirements. However, establishing this goal is not only subtle and complex, but also requires high qualified persons. In addition, this operation is mostly omitted due to its high cost and the system is tested while trying to reduce the risk of errors as much as possible. The cost is, nevertheless, paid when this operation is required in order to avoid catastrophic consequences and major errors. In these cases, tools like theorem prover and those used for automatic generation of software are helpful to significantly reduce the cost of proof. Our aim is that this tool proves to be powerful and simple enough to generate benefits even to small companies and individuals with scarce budgets and limited theoretical skills . Many promising formal frameworks for automatic enforcement of security policies in programs have been proposed during the last years. Their goal is to ensure that a program respects a given security policy which generally specifies acceptable executions of the program and can be expressed in terms of access control problems, information flow, availability of resources, confidentiality, etc. The literature records various techniques for enforcing security policies belonging to mainly two principal classes: static approaches including typing theory, Proof Carrying Code, and dynamic approaches including reference monitors, Java stack inspection. Static analysis aims at enforcing properties before program execution. In dynamic analysis, however, the enforcement takes place at runtime by intercepting critical events during the program execution and halting the latter whenever an action is attempting to violate the property being enforced. Recently, several researchers have explored rewriting techniques in order to gather advantages of both static and dynamic methods. The idea consists in modifying a program statically, so that the produced version respects the requested requirements. The rewritten program is generated from the original one by adding, when necessary, some tests at some critical points to obtain the desired behaviors. This thesis aims to propose an algebraic and automatic approach that could generate from a given program, and a security policy, a new version of this program that respects the requested security policy. More precisely, we define an operator [symbol] that takes as input a process [symbol] and a security policy [symbol] and generates [symbol], a new process that respects the following conditions: [symbol] "satisfies" the security policy [symbol]. [symbol], behaviours of [symbol] are also behaviours of [symbol]. [symbol], all good behaviours of [symbol] are also behaviours [symbol]. The main results of our research are the following~: 1. The definition of a process algebra [symbol] offering an algebraic framework for the enforcement of security policies on concurrent systems. 2. The definition of a logic, denoted by [symbol], inspired from Kleene algebras and regular expressions. Basically, it allows to specify properties that can be checked on a trace-based model and properties related to infinite behavior (e.g. a server should not send the password of users). The choice of this logic is motivated by its syntax that is close to the one chosen for processes. In fact, this similarity is helpful to simplify the definition of our formal monitor. 3. The development of an optimization technique which, for a certain class of security properties, reduces the number of tests added in the target.

Thèse en cotutelle, doctorat en droit : Université Laval, Québec, Canada, docteur en droit (LL.D.) et Université Toulouse 1 Capitole, Toulouse, France, docteur. / Comment vivre ensemble dans la diversité ? Le Canada et l’Europe sont deux ordres juridiques présentant ce même type de problématique : la gestion de la diversité juridique. La réponse se présente en un système de droit où il apparaît nécessaire de conjuguer l’un et le multiple. Dans le cas européen, il s'agit d'une conjugaison entre les ordres de gouvernement supranational et national, tandis qu'au Canada, il s'agit des ordres fédéral et provincial. Un élément de cette réponse apparaît dans l’organisation des rapports entre ces ordres juridiques. Plus précisément, un éclairage particulier ressort de l'évolution du partage des compétences, par l'intermédiaire de l'articulation des normes issues de ces différents niveaux. Le domaine de la protection de la qualité des eaux douces au Canada et dans l’Union européenne a été choisi pour révéler les enjeux de ces relations dans une perspective globale. L’objectif est de dépasser l’analyse du droit tel qu’il devrait être, pour le faire ressortir tel qu’il est. Plus précisément, il s’agit de faire ressortir comment s’articulent réellement les différents ordres de gouvernement au sein du Canada et de l’Union européenne. Seule une combinaison des normes du partage des compétences permet une telle entreprise. La démarche comparative est centrale puisqu’elle permet de mettre en perspective ces dispositifs entre deux ordres juridiques n’étant pas au même stade de leur construction. L'exemple de la protection de la qualité des eaux douces nous apprend qu'il existe des ressemblances fonctionnelles au Canada et en Europe au sujet de l'équilibre de la répartition des compétences. Cet équilibre semble entamé dans les deux régions, ce qui serait dû à une centralisation extensive des compétences et une uniformisation du droit, phénomènes progressifs engendrés par l'importance du principe d'efficacité dans ce domaine. / How living together in diversity ? Canada and European Union are two legal systems presenting this type of question : the legal diversity management. The answer to this question is composed of the alignment of the one and the multiple. In Europe, it is achieved in the allocation of powers between european and national legal orders ; in Canada, between federal and provincial legal orders. Fresh waters quality protection in Canada and EU has been chosen in order to reveal the allocation of powers issues from a global perspective. The aim of this research is to go beyond an analysis on how are legal systems supposed to work, to emphasize their real way of functioning. The combination of the allocation of powers rules allows this approach in water quality protection. This concrete example reveals that there are similarities between canadian and european allocation of powers. The balance of these distributions of powers has been eroded, because of powers centralization caused by an effectiveness principle in this field.

La sémantique des jeux est une approche pour modéliser les langages de programmation dans laquelle les types sont interprétés par des jeux et les programmes par des stratégies. Ces modèles de jeux ont couvert des constructions fonctionnelles et impératives, des opérateurs de contrôle, etc. L'approche a récemment été étendue aux langages non-déterministes et concurrents, provoquant au passage un changement de perspective profond~: les parties sont maintenant organisées en une catégorie, sur laquelle les stratégies sont des préfaisceaux. La notion fondamentale d'innocence a aussi été caractérisée comme une condition de faisceau. Cette thèse s'attache à l'étude de quelques constructions apparaissant dans ces nouveaux modèles de jeux.D'abord, constatant que, dans plusieurs de ces modèles, l'étape cruciale consiste à définir une catégorie double de jeux et de parties, nous proposons une construction abstraite d'une telle catégorie double à partir de données de base, puis nous démontrons que, sous des hypothèses adéquates, le résultat obtenu permet en effet la construction des stratégies.Dans un second temps, nous établissons un lien entre deux techniques existantes pour définir les parties~: la technique standard, fondée sur les séquences justifiées, et une autre plus récente utilisant les diagrammes de cordes. Nous définissons un plongement (plein) de la première dans la seconde et prouvons qu'elles induisent essentiellement le même modèle.Enfin, nous proposons une axiomatisation des notions de jeu et de partie, de laquelle nous tirons une catégorie de jeux et stratégies. Nous raffinons ensuite les axiomes pour traiter l'innocence et nous démontrons que, sous des hypothèses adéquates, les stratégies innocentes sont stables par composition. / Game semantics is a class of models of programming languages in which types are interpreted as games and programs as strategies. Such game models have successfully covered diverse features, such as functional and imperative programming, or control operators. They have recently been extended to non-deterministic and concurrent languages, which generated an in-depth recasting of the standard approach: plays are now organised into a category, on which strategies are presheaves. The fundamental notion of innocence has also been recast as a sheaf condition. This thesis is a study of various constructions appearing in this new approach to game semantics.We first consider a pattern common to several game models of concurrent languages, in which games and plays are first organised into a double category, from which strategies are then derived. We provide an abstract construction of such a double category from more basic data, and prove that, under suitable hypotheses, the result allows the construction of strategies.Our second contribution is to relate two established techniques for defining plays: the standard one, based on justified sequences, and a more recent one, based on string diagrams. We (fully) embed the former into the latter and prove that they induce essentially the same model.Finally, we propose an axiomatisation of the notions of game and play, from which we formally derive a category of games and strategies. We also refine the axioms to deal with innocence, and prove that, under suitable hypotheses, innocent strategies are stable under composition.

La vérification formelle de systèmes concurrents temps réels se heurte au problème de l'explosion du nombre d'états à explorer. Ce problème connu sous le nom ``d'explosion combinatoire'' à plusieurs causes. Cette thèse s'intéresse à deux d'entre-elles. · Pour lutter contre l'explosion due à la représentation du parallélisme par l'entrelacement d'actions, cette thèse propose des techniques basées sur l'approche des ordres-partiels pour construire un graphe réduit. Pour exploiter les ordres-partiels, les techniques proposées utilisent la construction de « pas de transitions » afin de limiter le nombre d'états explorés. Différentes constructions des « pas de transitions » sont proposées en fonction de la classe de propriétés que l'on souhaite préserver (Blocages, Équivalence de traces, LTL). · Pour lutter contre l'explosion due aux contraintes temporelles, cette thèse propose une approche par sur-approximation du comportement. L'objectif est d'avoir un graphe abstrait du comportement de la sur-approximation plus petit que celui du système. Comme classiquement, les techniques d'abstractions permettent d'obtenir une procédure de décision semi-effective. Lorsque l'analyse de la sur-approximation ne permet pas de conclure, la thèse propose une méthode effective permettant de conclure pour les formules de LTL: le système est analysé, guidé par les résultats obtenus sur la sur-approximation. Cette thèse présente les algorithmes de ces différentes techniques de réduction et l'outil tina (http://www.laas.fr/tina) dans lequel ils ont été implémentés.

Comme les systèmes matériels et logiciels grandissent de façon continue en échelle et fonctionnalités, la probabilité d'erreurs subtiles de- vient toujours plus grande. Les techniques d'abstraction, souvent basées sur l'interprétation abstraite de Cousot, fournissent une méthode pour exécuter symboliquement les systèmes en utilisant le domaine abstrait 'a la place du domaine concret. Dans cette thèse, on introduit des techniques d'abstraction pour les logiques sous des interprétations multivaluées. Beaucoup d'applications des logiques multivaluées ont été trouvées dans la vérification du matériel et du logiciel. Pour la vérification du matériel, des outils de simulation et des réalisations des circuits multivaluées véritables ont été proposés, les risques dynamiques ont été modelés en introduisant des 'états faux pour trouver des régions chevauchantes des signaux en concurrence, etc. Pour la vérification du logiciel on a besoin d'incertitude parce qu'on ne peut savoir si certains comportements devraient être possibles et on a besoin du désaccord parce que l'on peut avoir des acteurs différents qui sont en désaccord pour la manière dont les systèmes devraient se comporter. Les abstractions sont obtenues en appliquant des relations d''équivalence et après, les symboles prédicatifs de la logique sont redéfinis 'a s'appliquer cor- correctement aux classes d''équivalence 'a l'aide des politiques d'interprétation. On fournit des résultats de préservation pour la logique de premier ordre, pour la logique temporelle et pour la logique temporelle de la connaissance. Avant de discuter les abstractions multivaluées pour la logique temporelle, nous présentons une 'étude de cas pour utiliser l'abstraction dans le contexte des modèles du contrôle d'accès. Nous fournirons aussi une technique d'abstraction pour les types de données. Cette technique d'abstraction peut être 'élargie pour les types abstraits de données. Ici, les abstractions sont appliquées aux spécifications initiales au moyen des 'équations et ils sont appelés des abstractions 'équationnelles. De plus, la technique d'abstraction présentée généralise et clarifie la nature de beaucoup de techniques d'abstraction trouvées dans la littérature, telles: la technique de dupliquer les symboles prédicatifs, shape analysis, l'abstraction par prédicats, l'approche de McMillan, etc. Pour raisonner au sujet des systèmes dynamiques, on introduit les types de données dynamiques et on étend la méthode d'abstraction antérieure 'a ce cas. Le problème principal qui survient quand on utilise les abstractions est de trouver l'abstraction convenable ou de raffiner une abstraction déjà existante pour en obtenir une meilleure. On prouve que les techniques d'abstraction que nous avons introduites pour les types de données sous interprétation 3- valu'ee Kleene, peuvent être utilisées dans une procédure de raffinement. De plus, on montre que la procédure de raffinement guide par contre-exemple est plus efficace quand on l'utilise sous les abstractions 'équationnelles.

Contexte : Dans les analyses de survie, un risque concurrent est un événement qui empêche l'observation de l'événement d'intérêt (le décès le plus souvent). Si la probabilité de survenue d'un risque concurrent dépend de la probabilité de l'événement d'intérêt, alors il ne peut pas être traité comme une censure. Les patients ayant une insuffisance rénale chronique terminale peuvent être traités par hémodialyse, dialyse péritonéale et greffe rénale. Ces traitements sont complémentaire et les patients peuvent passer d'une modalité de traitement à une autre au cours de leur prise en charge. La dépendance entre les changements de traitement et la probabilité de décès n'a pas été étudiée et ces changements sont traités comme des censures dans les analyses de survie.Objectifs : Analyser la dépendance entre les probabilités de décès en dialyse et de greffe rénale, et entre les probabilités de décès en dialyse péritonéale et de transfert en hémodialyse. Nous démontrerons les conséquences néfastes de la non-prise en compte de cette dépendance dans les analyses de survie en dialyse. Méthodes : (1) Nous avons comparé les estimations de probabilité d'événement obtenues par la méthode de Kaplan-Meier et la méthode de Kalbfleisch et Prentice sur 383 patient indicent consécutifs traités par dialyse péritonéale à Lille. (2) Nous avons analysé les données de 7318 patients incidents traités par hémodialyse en France grâce au registre national REIN. Nous avons utilisé un modèle multi-états pour analyse l'influence de l'inscription sur liste d'attente de greffe sur la probabilité de décès en dialyse. (3) Sur une cohorte de 2790 patients âgés de plus de 65 ans et traités par dialyse péritonéale issus du Registre de Dialyse Péritonéale de Langue Française (RDPLF), nous avons analysé les facteurs de contre-indication au transfert en HD en prenant en compte le décès comme risque concurrent à l’aide du modèle de Fine et Gray. Cette analyse a été complétée par un questionnaire réalisé auprès 55 des néphrologues pratiquant la dialyse péritonéale en France. Résultats : (1) La méthode de Kaplan Meier surestimait systématiquement la probabilité de décès du fait de la violation de l'hypothèse d'indépendance entre le décès et les risques concurrents. Cette méthode n'apparaît donc pas valide dans les analyses de survie en dialyse. La méthode de Kalbfleisch et Prentice était valide mais l'interprétation des incidences cumulées doit prendre en compte tous les risques concurrents. (2) La greffe rénale est un risque concurrent dépendant de la probabilité de décès des patients. Les patients inscrits sur liste d'attente de greffe avaient un risque de décès significativement plus bas que les autres patients, après ajustement sur l'âge et la présence de comorbidités. (3) Le transfert en hémodialyse est un risque concurrent qui semble dépendre de la probabilité de décès des patients. En effet, l'âge et la présence de comorbidités étaient à la fois des facteurs de risque de décès et des facteurs de contre-indications au transfert en hémodialyse. De plus, la plupart des néphrologues ayant répondu à notre enquête ont déclaré qu'une espérance de vie limitée pouvait constituer une contre-indication au transfert. Conclusion : Dans les études de cohorte de patients en insuffisance rénale chronique terminale, les analyses de survie devraient prendre en compte les changements de traitement car ce sont des risques concurrents dépendants de la probabilité de décès. Notre travail a montré que les modèles multi-états sont des outils statistiques flexibles qui permettent de bien représenter l'inter-dépendance entre les différentes modalités de traitement entre dialyse péritonéale, hémodialyse, greffe rénale et décès. / In survival analysis, a competing risk is an event that hinders the observation of the event of interest (usually death). If the probability of a competing risk depends on the probability of the event of interest, then it can not be treated as censoring. Patients with ESRD can be treated with hemodialysis, peritoneal dialysis and renal transplantation. These treatments are complementary and patients can move from one treatment modality to another. The dependence between changes in treatment modality and the probability of death has not been studied and these changes are censored in survival analysis.Objectives: To analyze the dependence between the probability of death in dialysis and kidney transplant, and the probability of death on peritoneal dialysis and transfer to hemodialysis. We demonstrate the negative consequences if this dependence is not taken into account in the survival analysis. Methods: (1) We compared estimates of event probability obtained by the Kaplan-Meier method and Kalbfleisch and Prentice on 383 consecutive indicent patients treated by peritoneal dialysis in Lille. (2) We analyzed data on 7318 incident patients undergoing hemodialysis in France from the national registry REIN. We used a multistate model to analyze the influence of inclusion on the transplant waiting list on the probability of death on dialysis. (3) In a cohort of 2790 patients aged over 65 and treated with peritoneal dialysis from the registry of the French Language Peritoneal Dialysis (RDPLF), we analyzed the factors against transfer-indication in HD taking into account death as competing risk using the Fine and Gray model. This analysis was complemented by a survey conducted among 55 nephrologists practicing Peritoneal dialysis in France.Results: (1) The Kaplan-Meier method systematically overestimated the probability of death due to violation of the assumption of independence between death and competing risks. This method does not appear valid in the analyzes of survival on dialysis. The method of Kalbfleisch and Prentice was valid but the interpretation of cumulative impacts must take into account all the competing risks. (2) Kidney transplantation is a competing risk depending on the probability of dying patients. Patients on the transplant waiting list had a risk of death significantly lower than other patients, after adjustment for age and comorbidity. (3) The transfer is a risk in hemodialysis competitor who seems to depend on the probability of dying patients. Indeed, age and comorbidities were both risk factors and death factors against transfer-indications for hemodialysis. Moreover, most nephrologists who responded to our survey reported that limited life expectancy could be an indication to the transfer-cons.Conclusion: In cohort studies of patients with ESRD, the survival analyzes should take into account changes in treatment because they are competing risks dependent on the probability of death. Our work has shown that multi-state models are statistical tools that enable flexible to adequately represent the interdependence between the different modalities of treatment for peritoneal dialysis, hemodialysis, kidney transplantation and death.

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 de haut-niveau. Nous nous attachons à combattre le phénomène d'explosion combinatoire lié à l'exploration explicite de l'ensemble des entrelacements possibles du système. Pour cela, nous nous proposons de tirer profit de la quantité de mémoire et de la puissance de calcul offerte par un réseau local de machines travaillant de manière coopérative. Par le biais d'une analyse structurelle, nous cherchons à répartir efficacement le graphe d'accessibilité du système. Nous nous attachons ensuite à conserver l'efficacité des techniques visant à limiter l'explosion combinatoire dans cet environnement réparti en relâchant notamment les contraintes de cohérence sur l'exploration du graphe. Nous avons alors validé ces approches à l'aide d'un vérifieur réparti et multithreadé dans lequel nous avons implémenté nos algorithmes.