L'objectif de cette thèse est d'explorer des descriptions formelles pour la structure et le fonctionnement des systèmes biologiques, ainsi que des outils formels pour raisonner au sujet de leur comportement. Cette thèse s'inscrit dans les travaux étudiant les modèles informatiques sûrs où les calculs sont exprimés par l'intermédiaire de la réécriture, et où nous pouvons compter sur la vérification formelle pour exprimer et valider les propriétés des modèles. Dans cette thèse nous développons un calcul de réécriture d'ordre supérieur pour décrire des molécules, des règles de réaction, et la génération des réseaux biochimiques. Le calcul est basé sur la métaphore chimique en décrivant les calculs en termes de solutions chimiques dans lesquelles les molécules représentant des données agissent l'une sur l'autre librement selon des règles de réaction. Ainsi nous avons obtenu un Calcul Biochimique Abstrait étendant le modèle chimique d'ordre supérieur en considérant des molécules structurées. Le calcul est équipé d'une spécification naturelle de la concurrence et des mécanismes de contrôle grâce à l'expression des stratégies de réécriture sous forme de molécules. La description des complexes moléculaires ou des réactifs chimiques appartient à une classe spécifique de graphes. Nous définissons la structure des graphes avec ports et nous montrons que les principes du calcul biochimique instanciés pour les graphes avec ports sont assez expressifs pour modéliser des systèmes autonomes et des réseaux biochimiques. En plus, les techniques de la réécriture stratégique ouvrent la voie au raisonnement basé sur les calculs et à la vérification des propriétés des systèmes modélisés.

L'objectif de cette thèse est d'explorer des descriptions formelles pour la structure et le fonctionnement des systèmes biologiques, ainsi que des outils formels pour raisonner au sujet de leur comportement. Cette thèse s'inscrit dans les travaux étudiant les modèles informatiques sûrs où les calculs sont exprimés par l'intermédiaire de la réécriture, et où nous pouvons compter sur la vérification formelle pour exprimer et valider les propriétés des modèles. Dans cette thèse nous développons un calcul de réécriture d'ordre supérieur pour décrire des molécules, des règles de réaction, et la génération des réseaux biochimiques. Le calcul est basé sur la métaphore chimique en décrivant les calculs en termes de solutions chimiques dans lesquelles les molécules représentant des données agissent l'une sur l'autre librement selon des règles de réaction. Ainsi nous avons obtenu un Calcul Biochimique Abstrait étendant le modèle chimique d'ordre supérieur en considérant des molécules structurées. Le calcul est équipé d'une spécification naturelle de la concurrence et des mécanismes de contrôle grâce à l'expression des stratégies de réécriture sous forme de molécules. La description des complexes moléculaires ou des réactifs chimiques appartient à une classe spécifique de graphes. Nous définissons la structure des graphes avec ports et nous montrons que les principes du calcul biochimique instanciés pour les graphes avec ports sont assez expressifs pour modéliser des systèmes autonomes et des réseaux biochimiques. En plus, les techniques de la réécriture stratégique ouvrent la voie au raisonnement basé sur les calculs et à la vérification des propriétés des systèmes modélisés / The objective of this thesis is to explore formal descriptions for the structure and functioning of biological systems, as well as formal tools for reasoning about their behavior. This work takes place in the overall prospective to study safe computational models where computations are expressed via rewriting, and where we can rely on formal verification to express and validate suitable properties. In this thesis we develop a higher-order calculus rewriting for describing molecules, reaction patterns, and biochemical network generation. The calculus is based on the chemical metaphor by describing the computations in terms of chemical solutions in which molecules representing data freely interact according to reaction rules. This way we obtained an Abstract Biochemical Calculus as an extension of the higher-order chemical model by considering structured molecules. The calculus is provided with a natural specification of concurrency and of controlling mechanisms by expressing rewrite strategies as molecules. The description of molecular complexes or chemical reactants belong to specific classes of graphs. We define the structure of port graphs and we show how the principles of the biochemical calculus instantiated for port graphs are expressive enough for modeling autonomous systems and biochemical networks. In addition, strategic rewriting techniques open the way to reason about the computations and to verify properties of the modeled systems

La plupart des processus informatiques mettent en jeu la notion de transformation, en particulier la compilation. Nous nous intéressons dans cette thèse à fournir des outils et des méthodes, utilisant la réécriture, permettant d'accroître la confiance que l'on peut placer dans ces processus. Nous développons dans un premier temps un cadre permettant de valider la compilation de constructions de filtrage, produisant une preuve formelle de la validité de la compilation, ainsi qu'un témoin de cette preuve, à chaque exécution du compilateur. Afin de permettre l'écriture sûre de transformations complexes, nous proposons un générateur de structures de données efficaces intégrant des invariants algébriques, et un langage de stratégies permettant de contrôler l'application des transformations. Ces résultats constituent donc une avancée vers la constitution de methodes génériques sûres pour le développement de transformations de confiance. / Most computer processes involve the notion of transformation, in particular the compilation processes. We interest in this thesis in providing tools and methods, based on rewriting, giving the opportunity to increase the confidence we can place into those processes. We develop first a framework used to validate the compilation of matching constructs, building a formal proof of the validity of the compilation process along with a witness of this proof, for each run of the compiler. Then, in order to allow one to write safely complex transformations, we propose a tool that generates an efficient data structure integrating algebraic invariants, as well as a strategy language that enables to control the application of transformations. Those results can be seen as a first step towards the constitution of generic and safe methods for the development of trustworthy transformations.