Formal methods offer a way to deal with the complexity of information systems. They are adapted to a variety of domains like design, verification, model-checking, test and supervision. But information systems are also more and more often distributed, first because of the generalization of information networks, but also because inside a single device, like a computer, the numerous components run concurrently. The problem is that concurrency is known to be a major difficulty for the use of formal methods because it causes a combinatorial explosion of the state space of the systems. This difficulty comes sometimes with another one due to time when it plays an important role in the behaviour of the systems, for instance when the execution time is a critical parameter. These two difficulties, concurrency and real-time, have guided my research works. Sometimes I have tackled one of these two aspects separately, but in many of my works, I have dealt with the problems that arise when one studies systems that are both concurrent and real-time. In my habilitation thesis, I give an overview of my recent research works on dependencies between events in real-time distributed systems and on implementability issues for these systems.

Cette thèse est en majeure partie dédiée au calcul rapide de remontée p-adique par des algorithmes détendus. Dans une première partie, nous présentons le cadre général des algorithmes détendus et de leur application au calcul de p-adiques récursifs. Pour appliquer ce cadre à la remontée p-adique de divers systèmes d'équations, il reste à transformer ces équations implicites en équations récursives. Ainsi, la seconde partie traite des systèmes d'équations linéaires, éventuellement différentiels. La remontée de résolutions de systèmes polynomiaux se trouve en troisième partie. Dans tous les cas, les nouveaux algorithmes détendus sont comparés, en théorie comme en pratique, aux algorithmes existants. En quatrième partie, nous étudions l'algèbre de décomposition universelle d'un polynôme. Nous développons un algorithme rapide pour calculer une représentation adéquate de cette algèbre et l'utilisons pour manipuler efficacement les éléments de l'algèbre. Finalement, nous montrons en annexe que la recherche d'invariants fondamentaux d'algèbres d'invariants sous un groupe fini peut se faire directement modulo p, facilitant ainsi leur calcul.

Le sujet de ma thèse consiste à analyser la sécurité d'un système de stockage pair à pair. Durant la première phase j'ai commencé par me familiariser avec le système existant (que du code), par la suite j'ai analysé la résistance du système en la présence d'attaques internes (que j'ai implémenté) en utilisant la simulation (travaux publiés dans HPCS'11). Le simulateur utilisé est un simulateur propriétaire qui reprend le code initial du système et modulable. Les résultats de cette analyse (perte de données) m'ont conduit à mettre en place un mécanisme de détection pour détecter ces attaques avant qu'elles ne causent la perte des données. Ce mécanisme de détection consiste à mettre en place un système de notation à deux niveaux : niveau 1:notation des échanges entre pair, niveau 2: notation des notes accordées à chaque pair (confiance en ces notes). Le principe de ce système est basé sur l'historique des échanges et la diffusion des notes entre les pairs. Dans un premier temps un système de notation à un niveau à été modélisé, implémenté et son efficacité analysée en utilisant deux méthodes (simulation pour les résultats quantitatifs et le model-checking pour les résultats qualitatifs. Pour la partie modélisation et vérification j'ai utilisé le formalisme ABCD [1], et les compilateurs SNAKES[2] et NICO[3,4]. Les résultats ont montrés la limite de ce système de notation à un seul niveau. (Travaux publiés dans TMS'12). A noter que jusque là seulement quelques attaques ont été détectées. En parallèle de tout ça un travail de modélisation dans un contexte de génie logiciel à été fait. Modélisation de l'application (Java) en utilisant le formalisme ABCD.

Les outils présentés dans ce mémoire ont pour but d'améliorer, par l'apport de méthodes et de techniques de calcul formel, les performances et les capacités de calcul des logiciels qui modélisent et le comportement dynamique de systèmes de corps mécaniques reliés entre eux. On s'intéresse à la possibilité d'écrire de manière automatique un ensemble d'équations différentielles régissant la dynamique de tels systèmes à partir de leurs descriptions physiques. Dans le premier chapitre, on décrit soigneusement les objets mécaniques et mathématiques qui interviennent dans l'étude dynamique des systèmes multicorps, et on met en évidence un problème fondamental : la nature de l'ensemble des configurations admissibles des mécanismes à structures bouclées. Le deuxième chapitre est une étude détaillée, sur un exemple, des différentes méthodes de génération des équations du mouvement de systèmes multicorps, dans l'optique de leur implémentation dans un logiciel de calcul symbolique. Il montre l'intérêt des techniques formelles et permet de spécifier les outils qui doivent être créés pour mener à bien cette implémentation. Dans le troisième chapitre, on présente les outils formels qui ont été développés pour aider à construire un générateur automatique des équations de la dynamique de systèmes polyarticulés. On se consacre, dans le quatrième chapitre, à apporter des éléments de solutions au problème de la détermination de la dimension des variétés de configurations de mécanismes à structures bouclées. Plusieurs méthodes faisant appel à des techniques algébriques, probabilistes et géométriques sont exposées, ainsi que leurs implémentations, et leurs expérimentations.

Les travaux présentés ici s'intéressent aux coloriages du plan discret. Ce modèle d'inspiration géométrique est intrinsèquement lié aux modèles de calcul, et son étude se décline ici suivant deux axes complémentaires: calculabilité et combinatoire. Nous montrons en particulier ici comment de nombreux résultats récents s'expriment naturellement à travers le concept de bases, propriétés vérifiées par au moins un point de tout ensemble de coloriages, et d'antibases, contre-exemples à ce concept. Nous examinons ensuite les différents codages du calcul par des jeux de tuiles et exhibons en particulier un nouveau codage épars, permettant de caractériser les degrés Turing des ensembles de coloriages. Enfin nous revenons aux origines en étudiant les pavages du point de vue de la logique. Nous caractérisons ainsi les grandes familles d'ensembles de coloriages par des fragments de la logique monadique du second ordre.

Dans les années 80, Shimomura a déterminé les groupes d'homotopie du spectre de Moore V(0) localisé par rapport à K(2) la deuxième K-théorie de Morava. Plus tard, avec les travaux de Devinatz et Hopkins est apparu une autre suite spectrale convergeant vers les précédents groupes d'homotopies. Lorsque le paramètre premier p de la théorie K(2) est supérieur ou égal à cinq, la précédente suite spectrale dégénère. Ainsi, déterminer ces groupes d'homotopie revient à calculer les groupes de cohomologie du groupe stabilisateur de Morava à coefficients dans l'anneau de Lubin-Tate modulo p. En 2007, Henn a démontré l'existence, lorsque p > 3, d'une résolution projective du groupe de Morava de longueur quatre. Dans cette thèse, nous précisons une telle résolution projective. On l'applique ensuite au calcul effectif des groupes de cohomologie à coefficients dans l'anneau de Lubin-Tate modulo p. Enfin, on donne une seconde application, en redémontrant un résultat de Hopkins non publié sur le groupe de Picard de la catégorie des spectres K(2)-locaux.

Humans make mistakes, especially when faced to complex tasks, such as the construction of modern hardware or software. This thesis focuses on machine-assisted techniques to guarantee that computers behave correctly. Modern computer systems are large and complex. Automated formal verification stands as an alternative to testing or simulation to ensuring their reliability. It essentially proposes to employ computers to exhaustively check the system behavior. Unfortunately, automated verification suffers from the state-space explosion problem: even relatively small systems can reach a huge number of states. Using the right representation for the system behavior seems to be a key step to tackle the inherent complexity of the problems that automated verification solves. The verification of concurrent systems poses additional issues, as their analysis requires to evaluate, conceptually, all possible execution orders of their concurrent actions. Petri net unfoldings are a well-established verification technique for concurrent systems. They represent behavior by partial orders, which not only is natural but also efficient for automatic verification. This dissertation focuses on the verification of concurrent systems, employing Petri nets to formalize them, and studies two prominent verification techniques: model checking and fault diagnosis. We investigate the unfoldings of Petri nets extended with read arcs. The unfoldings of these so-called contextual nets seem to be a better representation for systems exhibiting concurrent read access to shared resources: they can be exponentially smaller than conventional unfoldings on these cases. Theoretical and practical contributions are made. We first study the construction of contextual unfoldings, introducing algorithms and data structures that enable their efficient computation. We integrate contextual unfoldings with merged processes, another representation of concurrent behavior that alleviates the explosion caused by non-determinism. The resulting structure, called contextual merged processes, is often orders of magnitude smaller than unfoldings, as we experimentally demonstrate. Next, we develop verification techniques based on unfoldings. We define SAT encodings for the reachability problem in contextual unfoldings, thus solving the problem of detecting cycles of asymmetric conflict. Also, an unfolding-based decision procedure for fault diagnosis under fairness constraints is presented, in this case only for conventional unfoldings. Finally, we implement our verification algorithms, aiming at producing a competitive model checker intended to handle realistic benchmarks. We subsequently evaluate our methods over a standard set of benchmarks and compare them with existing unfolding-based techniques. The experiments demonstrate that reachability checking based on contextual unfoldings outperforms existing techniques on a wide number of cases. This suggests that contextual unfoldings, and asymmetric event structures in general, have a rightful place in research on concurrency, also from an efficiency point of view.

Thesis (doctoral)--Universität, Regensburg, 2009. / Includes bibliographical references.

Gérer l'évolution des logiciels est une tâche complexe mais nécessaire. Tout au long de son cycle de vie, un logiciel doit subir des changements, pour corriger des erreurs, améliorer ses performances et sa qualité, étendre ses fonctionnalités ou s’adapter à son environnement. A défaut d’évoluer, un logiciel se dégrade, devient obsolète ou inadapté et est remplacé. Cependant, sans évaluation de leurs impacts et contrôle de leur réalisation, les changements peuvent être sources d’incohérences et de dysfonctionnements, donc générateurs de dégradations du logiciel. Cette thèse propose une approche améliorant la gestion de l'évolution des logiciels dans les processus de développement orientés composants. Adoptant une démarche d’ingénierie dirigée par les modèles (IDM), cette approche s’appuie sur Dedal, un langage de description d’architecture (ADL) séparant explicitement trois niveaux d’abstraction dans la définition des architectures logicielles. Ces trois niveaux (spécification, configuration et assemblage) correspondent aux trois étapes principales du développement d’une architecture (conception, implémentation, déploiement) et gardent la trace des décisions architecturales prises au fil du développement. Ces informations sont un support efficace à la gestion de l’évolution : elles permettent de déterminer le niveau d’un changement, d’analyser son impact et de planifier sa réalisation afin d’éviter la survenue d’incohérences dans la définition de l’architecture (érosion, dérive, etc.). Une gestion rigoureuse de l’évolution nécessite la formalisation, d’une part, des relations intra-niveau liant les composants au sein des modèles correspondant aux différents niveaux de définition d’une architecture et, d’autre part, des relations inter-niveaux liant les modèles décrivant une même architecture aux différents niveaux d’abstraction. Ces relations permettent la définition des propriétés de consistance et de cohérence servant à vérifier la correction d’une architecture. Le processus d’évolution est ainsi décomposé en trois phases : initier le changement de la définition de l’architecture à un niveau d’abstraction donné ; vérifier et rétablir la consistance de cette définition en induisant des changements complémentaires ; vérifier et rétablir la cohérence globale de la définition de l’architecture en propageant éventuellement les changements aux autres niveaux d’abstraction.Ces relations et propriétés sont décrites en B, un langage de modélisation formel basé sur la théorie des ensembles et la logique du premier ordre. Elles s’appliquent à des architectures définies avec un adl formel écrit en B dont le méta-modèle, aligné avec celui de Dedal, permet d’outiller la transformation de modèles entre les deux langages. Cette intégration permet de proposer un environnement de développement conjuguant les avantages des approches IDM et formelle : la conception d’architectures avec l’outillage de Dedal (modeleur graphique); la vérification des architectures et la gestion de l’évolution avec l’outillage de B (animateur, model-checker, solver). Nous proposons en particulier d’utiliser un solver B pour calculer automatiquement des plans d’évolution conformes à notre proposition et avons ainsi défini l’ensemble des règles d’évolution décrivant les opérations de modification applicables à la définition d’une architecture. Le solver recherche alors automatiquement une séquence de modifications permettant la réalisation d’un changement cible tout en préservant les propriétés de consistance et de cohérence de l’architecture. Nous avons validé la faisabilité de cette gestion de l’évolution par une implémentation mêlant optimisation et génie logiciel (search-based software engineering), intégrant notre propre solver pourvu d’heuristiques spécifiques qui améliorent significativement les temps de calcul, pour expérimenter trois scénarios d’évolution permettant de tester la réalisation d’un changement à chacun des trois niveaux d’abstraction. / Managing software evolution is a complex task. Indeed, throughout their whole lifecycle, software systems are subject to changes to extend their functionalities, correct bugs, improve performance and quality, or adapt to their environment. If not evolved, software systems degrade, become obsolete or inadequate and are replaced. While unavoidable, software changes may engender several inconsistencies and system dysfunction if not analyzed and handled carefully hence leading to software degradation and phase-out.This thesis proposes an approach to improve the evolution management activity in component-based software development processes. The solution adopts a Model-Driven Engineering (MDE) approach. It is based on Dedal, an Architecture Description Language (ADL) that explicitly separates software architecture descriptions into three abstraction levels: specification, configuration and assembly. These abstraction levels respectively correspond to the three major steps of component-based development (design, implementation and deployment) and trace architectural decisions all along development. Dedal hence efficiently supports evolution management: It enables to determine the level of change, analyze its impact and plan its execution in order to prevent architecture inconsistencies (erosion, drift, etc.). Rigorous evolution management requires the formalization, on the one hand, of intra-level relations linking components within models corresponding to different architecture abstraction levels and on the other hand, of the formalization of inter-level relations linking models describing the same architecture at different abstraction levels. These relations enable the definition of the consistency and coherence properties that prove necessary for architecture correctness analysis. The evolution process therefore consists of three steps: First, change is initiated on an architecture description at a given abstraction level; then, the consistency of the impacted description is checked out and restored by triggering additional changes; finally, the global coherence of the architecture definitions is verified and restored by propagating changes to other abstraction levels.Relations and properties are expressed in B, a set-theoretic and first-order logic language. They are applied on B formal ADL, the meta-model of which is mapped to Dedal's and helps automatic model transformations. This integration enables to implement a development environment that combines the benefits of both MDE and formal approaches: Software architecture design using Dedal tools (graphical modeler) and architecture analysis and evolution management using B tools (animator, model-checker, solver).In particular, we propose to use a B solver to automatically calculate evolution plans according to our approach. The solver explores a set of defined evolution rules that describe the change operations that can apply on architecture definitions. It automatically searches for a sequence of operations that both changes the architecture as requested and preserves architecture consistency and coherence properties. The feasibility of the evolution management approach is demonstrated through the experimentation of three evolution scenarios, each addressing a change at different abstraction level. The experimentation relies on an implementation of a search-based software engineering approach mixing software engineering and optimization and integrates our own solver with specific heuristics that significantly improve calculation time.

Les modèles de systèmes complexes sont conçus dans différents contextes. Cependant, l'hétérogénéité induite par ces contextes n’est pas prise en compte lors de la description et de la validation de ces systèmes. De plus, ces systèmes impliquent généralement l’intervention deplusieurs experts du domaine et la réalisation de plusieurs modèles correspondant à différentes analyses (vues) de ce même système. Aucune information concernant les caractéristiques du domaine ni des analyses réalisées n'est explicitée. Nous proposons un cadre méthodologiquepermettant d’une part, de formaliser les connaissances de domaine à l’aide d’ontologies, et d’autre part d'enrichir les modèles à l’aide des connaissances de domaine en définissant des références explicites aux informations formalisées dans ces ontologies. Ce cadre permet également de rendre explicites les caractéristiques d'une analyse en les formalisant dans des modèles qualifiés de «points de vue». Nous avons réalisé deux déploiements de ce cadre méthodologique : un premier déploiement utilisant les techniques de l’Ingénierie Dirigée par les Modèles (IDM) et un second fondé sur les méthodes formelles basées sur des techniques de preuve et de raffinement. Ce cadre a été validé sur plusieurs cas d'études non triviaux issus de l'ingénierie système. / Complex systems models are designed in heterogeneous domains and this heterogeneity is rarely considered explicitly when describing and validating processes. Moreover, these systems usually involve several domain experts and several design models corresponding to different analyses (views) of the same system. However, no explicit information regarding the characteristics neither of the domain nor of the performed system analyses is given. In our thesis, we propose a general framework offering first, the formalization of domain knowledge using ontologies and second, the capability to strengthen design models by making explicit references to the domain knowledgeformalized in these ontology. This framework also provides resources for making explicit the features of an analysis by formalizing them within models qualified as ‘’points of view ‘’. We have set up two deployments of our approach: a Model Driven Engineering (MDE) based deployment and a formal methods one based on proof and refinement. This general framework has been validated on several no trivial case studies issued from system engineering.