Logic programming is appealing since it allows the programmer to concentrate on the meaning of the problem to be solved. Unfortunately, for efficiency reasons, the declarative and operational natures of Prolog do not coincide. Prolog uses an incomplete depth-first search rule, unifications and negations may be unsound, and there are extralogical features like the cut or dynamic predicates. Methodologies have been proposed to construct operationally correct and efficient Prolog code. Researchers have designed methods to automate the verification of operational properties on which optimisation of logic programs can be based. A few tools have been implemented but there is a lack of a unified framework. <P> The goal and topic of this thesis is the design, implementation and evaluation of an abstract interpretation framework of Prolog to integrate state-of-the-art techniques. The analyser is based on an original proposal that defines the notion of abstract sequence, which allows one to verify many desirable operational properties of a logic procedure. The properties include types, modes, sharing of terms, proving termination, linear relations between the size of input/output terms and the number of solutions to a call. A single global analysis is performed, and abstract sequences are derived at each program point. <P> In this thesis, we implement and evaluate the original framework, and, more importantly, we overcome its limitations to make it accurate and usable in practice: the improved framework accepts any Prolog code with modules, new abstract domains and operations are added, and the language of specifications is more expressive. We also design and implement an optimiser that generates specialised code. The optimiser uses the abstract information to safely apply source-to-source transformations. Code transformations include clause and literal reordering, introduction of cuts, and removal of redundant literals. The optimiser follows a precise strategy to choose the most rewarding transformations in best order.

Si la production de logiciel fiable est depuis longtemps la préoccupation d'ingénieurs, elle devient à ce jour une branche de sujets de recherche riche en applications, dont l'analyse statique. Ce travail a porté sur l'analyse statique de programmes et, plus précisément, sur l'analyse des propriétés numériques. Ces analyses sont traditionnellement basées sur le concept de domaine abstrait. Le problème est que, ce n'est pas évident d'étendre ces domaines dans le contexte de programmes avec pointeurs. Nous avons proposé une approche qui sait systématiquement combiner ces domaines avec l'information de l'analyse de points-to (une sorte d'analyse de pointeurs). L'approche est formalisée en théorie de l'interprétation abstraite, prouvée correct et prototypée avec une modular implémentation qui sait inférer des propriétés numériques des programmes de millions de lignes de codes. La deuxième partie de la thèse vise à améliorer la précision de l'analyse points-to. Nous avons découvert que l'analyse de must-alias (qui analyse si deux variables sont nécessairement égaux) peut servir à raffiner l'analyse points-to. Nous avons formalisé cette combinaison en s'appuyant sur la notion de bisimulation, bien connue en vérification de modèle ou théorie de jeu... Un algorithme de complexité quadruple est proposé et prouvé correct. / The fast and furious pace of change in computing technology has become an article of faith for many. The reliability of computer-based systems cru- cially depends on the correctness of its computing. Can man, who created the computer, be capable of preventing machine-made misfortune? The theory of static analysis strives to achieve this ambition. The analysis of numerical properties of programs has been an essential research topic for static analysis. These kinds of properties are commonly modeled and handled by the concept of numerical abstract domains. Unfor- tunately, lifting these domains to heap-manipulating programs is not obvious. On the other hand, points-to analyses have been intensively studied to an- alyze pointer behaviors and some scale to very large programs but without inferring any numerical properties. We propose a framework based on the theory of abstract interpretation that is able to combine existing numerical domains and points-to analyses in a modular way. The static numerical anal- ysis is prototyped using the SOOT framework for pointer analyses and the PPL library for numerical domains. The implementation is able to analyze large Java program within several minutes. The second part of this thesis consists of a theoretical study of the com- bination of the points-to analysis with another pointer analysis providing information called must-alias. Two pointer variables must alias at some pro- gram control point if they hold equal reference whenever the control point is reached. We have developed an algorithm of quadruple complexity that sharpens points-to analysis using must-alias information. The algorithm is proved correct following a semantics-based formalization and the concept of bisimulation borrowed from the game theory, model checking etc.

Les systèmes critiques basés sur l’arithmétique flottante exigent un processus rigoureux de vérification et de validation pour augmenter notre confiance en leur sureté et leur fiabilité. Malheureusement, les techniques existentes fournissent souvent une surestimation d’erreurs d’arrondi. Nous citons Arian 5 et le missile Patriot comme fameux exemples de désastres causés par les erreurs de calculs. Ces dernières années, plusieurs techniques concernant la transformation d’expressions arithmétiques pour améliorer la précision numérique ont été proposées. Dans ce travail, nous allons une étape plus loin en transformant automatiquement non seulement des expressions arithmétiques mais des programmes complets contenant des affectations, des structures de contrôle et des fonctions. Nous définissons un ensemble de règles de transformation permettant la génération, sous certaines conditions et en un temps polynômial, des expressions pluslarges en appliquant des calculs formels limités, au sein de plusieurs itérations d’une boucle. Par la suite, ces larges expressions sont re-parenthésées pour trouver la meilleure expression améliorant ainsi la précision numérique des calculs de programmes. Notre approche se base sur les techniques d’analyse statique par interprétation abstraite pour sur-rapprocher les erreurs d’arrondi dans les programmes et au moment de la transformation des expressions. Cette approche est implémenté dans notre outil et des résultats expérimentaux sur des algorithmes numériques classiques et des programmes venant du monde d’embarqués sont présentés. / Critical software based on floating-point arithmetic requires rigorous verification and validation process to improve our confidence in their reliability and their safety. Unfortunately available techniques for this task often provide overestimates of the round-off errors. We can cite Arian 5, Patriot rocket as well-known examples of disasters. These last years, several techniques have been proposed concerning the transformation of arithmetic expressions in order to improve their numerical accuracy and, in this work, we go one step further by automatically transforming larger pieces of code containing assignments, control structures and functions. We define a set of transformation rules allowing the generation, under certain conditions and in polynomial time, of larger expressions by performing limited formal computations, possibly among several iterations of a loop. These larger expressions are better suited to improve, by re-parsing, the numerical accuracy of the program results. We use abstract interpretation based static analysis techniques to over-approximate the round-off errors in programs and during the transformation of expressions. A tool has been implemented and experimental results are presented concerning classical numerical algorithms and algorithms for embedded systems.

A discrete event system is a system whose state space is given by a discrete set and whose state transition mechanism is event-driven i.e., its state evolution depends only on the occurrence of discrete events over the time. These systems are used in many fields of application (telecommunication networks, aeronautics, aerospace,...). The validity of these systems is then an important issue and to ensure it we can use supervisory control methods. These methods consist in imposing a given specification on a system by means of a controller which runs in parallel with the original system and which restricts its behavior. In this thesis, we develop supervisory control methods where the system can have an infinite state space and the controller has a partial observation of the system (this implies that the controller must define its control policy from an imperfect knowledge of the system). Unfortunately, this problem is generally undecidable. To overcome this negative result, we use abstract interpretation techniques which ensure the termination of our algorithms by overapproximating, however, some computations. The aim of this thesis is to provide the most complete contribution it is possible to bring to this topic. Hence, we consider more and more realistic problems. More precisely, we start our work by considering a centralized framework (i.e., the system is controlled by a single controller) and by synthesizing memoryless controllers (i.e., controllers that define their control policy from the current observation received from the system). Next, to obtain better solutions, we consider the synthesis of controllers that record a part or the whole of the execution of the system and use this information to define the control policy. Unfortunately, these methods cannot be used to control an interesting class of systems: the distributed systems. We have then defined methods that allow to control distributed systems with synchronous communications (decentralized and modular methods) and with asynchronous communications (distributed method). Moreover, we have implemented some of our algorithms to experimentally evaluate the quality of the synthesized controllers. / Un système à événements discrets est un système dont l'espace d'états est un ensemble discret et dont l'évolution de l'état courant dépend de l'occurrence d'événements discrets à travers le temps. Ces systèmes sont présents dans de nombreux domaines critiques tels les réseaux de communications, l'aéronautique, l'aérospatiale... La validité de ces systèmes est dès lors une question importante et une manière de l'assurer est d'utiliser des méthodes de contrôle supervisé. Ces méthodes associent au système un dispositif, appelé contrôleur, qui s'exécute en parrallèle et qui restreint le comportement du système de manière à empêcher qu'un comportement erroné ne se produise. Dans cette thèse, on s'intéresse au développement de méthodes de contrôle supervisé où le système peut avoir un espace d'états infini et où les contrôleurs ne sont pas toujours capables d'observer parfaitement le système; ce qui implique qu'ils doivent définir leur politique de contrôle à partir d'une connaissance imparfaite du système. Malheureusement, ce problème est généralement indécidable. Pour surmonter cette difficulté, nous utilisons alors des techniques d'interprétation abstraite qui assurent la terminaison de nos algorithmes au prix de certaines sur-approximations dans les calculs. Le but de notre thèse est de fournir la contribution la plus complète possible dans ce domaine et nous considèrons pour cela des problèmes de plus en plus réalistes. Plus précisement, nous avons commencé notre travail en définissant une méthode centralisée où le système est contrôlé par un seul contrôleur qui définit sa politique de contrôle à partir de la dernière information reçue du système. Ensuite, pour obtenir de meilleures solutions, nous avons défini des contrôleurs qui retiennent une partie ou la totalité de l'exécution du système et qui définissent leur politique de contrôle à partir de cette information. Malheureusement, ces méthodes ne peuvent pas être utilisées pour contrôler une classe intéressante de systèmes: les sytèmes distribués. Nous avons alors défini des méthodes permettant de contrôler des systèmes distribués dont les communications sont synchrones (méthodes décentralisées et modulaires) et asynchrones (méthodes distribuées). De plus, nous avons implémenté certains de nos algorithmes pour évaluer expérimentalement la qualité des contrôleurs qu'ils synthétisent.

Embedded systems are becoming ubiquitous in our daily life. Due to close interaction with physical world, embedded systems are typically subject to timing constraints. At design time, it must be ensured that the run-time behaviors of such systems satisfy the pre-specified timing constraints under any circumstance. In this thesis, we develop techniques to address the timing analysis problems brought by the increasing complexity of underlying hardware and software on different levels of abstraction in embedded systems design. On the program level, we develop quantitative analysis techniques to predict the cache hit/miss behaviors for tight WCET estimation, and study two commonly used replacement policies, MRU and FIFO, which cannot be analyzed adequately using the state-of-the-art qualitative cache analysis method. Our quantitative approach greatly improves the precision of WCET estimation and discloses interesting predictability properties of these replacement policies, which are concealed in the qualitative analysis framework. On the component level, we address the challenges raised by multi-core computing. Several fundamental problems in multiprocessor scheduling are investigated. In global scheduling, we propose an analysis method to rule out a great part of impossible system behaviors for better analysis precision, and establish conditions to guarantee the bounded responsiveness of computing tasks. In partitioned scheduling, we close a long standing open problem to generalize the famous Liu and Layland's utilization bound in uniprocessor real-time scheduling to multiprocessor systems. We also propose to use cache partitioning for multi-core systems to avoid contentions on shared caches, and solve the underlying schedulability analysis problem. On the system level, we present techniques to improve the Real-Time Calculus (RTC) analysis framework in both efficiency and precision. First, we have developed Finitary Real-Time Calculus to solve the scalability problem of the original RTC due to period explosion. The key idea is to only maintain and operate on a limited prefix of each curve that is relevant to the final results during the whole analysis procedure. We further improve the analysis precision of EDF components in RTC, by precisely bounding the response time of each computation request.

La recherche d'une borne supérieure au temps d'exécution d'un programme est une partie essentielle du processus de vérification de systèmes temps-réel critiques. Les programmes de tels systèmes ont généralement des temps d'exécution variables et il est difficile, voire impossible, de prédire l'ensemble de ces temps possibles. Au lieu de cela, il est préférable de rechercher une approximation du temps d'exécution pire-cas ou Worst-Case Execution Time (WCET). Une propriété cruciale de cette approximation est qu'elle doit être sûre, c'est-à-dire qu'elle doit être garantie de majorer le WCET. Parce que nous cherchons à prouver que le système en question se termine en un temps raisonnable, une surapproximation est le seul type d'approximation acceptable. La garantie de cette propriété de sûreté ne saurait raisonnablement se faire sans analyse statique, un résultat se basant sur une série de tests ne pouvant être sûr sans un traitement exhaustif des cas d'exécution. De plus, en l'absence de certification du processus de compilation (et de transfert des propriétés vers le binaire), l'extraction de propriétés doit se faire directement sur le code binaire pour garantir leur fiabilité. Toutefois, cette approximation a un coût : un pessimisme - écart entre le WCET estimé et le WCET réel - important entraîne des surcoûts superflus de matériel pour que le système respecte les contraintes temporelles qui lui sont imposées. Il s'agit donc ensuite, tout en maintenant la garantie de sécurité de l'estimation du WCET, d'améliorer sa précision en réduisant cet écart de telle sorte qu'il soit suffisamment faible pour ne pas entraîner des coûts supplémentaires démesurés. Un des principaux facteurs de surestimation est la prise en compte de chemins d'exécution sémantiquement impossibles, dits infaisables, dans le calcul du WCET. Ceci est dû à l'analyse par énumération implicite des chemins ou Implicit Path Enumeration Technique (IPET) qui raisonne sur un surensemble des chemins d'exécution. Lorsque le chemin d'exécution pire-cas ou Worst-Case Execution Path (WCEP), correspondant au WCET estimé, porte sur un chemin infaisable, la précision de cette estimation est négativement affectée. Afin de parer à cette perte de précision, cette thèse propose une technique de détection de chemins infaisables, permettant l'amélioration de la précision des analyses statiques (dont celles pour le WCET) en les informant de l'infaisabilité de certains chemins du programme. Cette information est passée sous la forme de propriétés de flot de données formatées dans un langage d'annotation portable, FFX, permettant la communication des résultats de notre analyse de chemins infaisables vers d'autres analyses. Les méthodes présentées dans cette thèse sont inclues dans le framework OTAWA, développé au sein de l'équipe TRACES à l'IRIT. Elles usent elles-mêmes d'approximations pour représenter les états possibles de la machine en différents points du programme. / The search for an upper bound of the execution time of a program is an essential part of the verification of real-time critical systems. The execution times of the programs of such systems generally vary a lot, and it is difficult, or impossible, to predict the range of the possible times. Instead, it is better to look for an approximation of the Worst-Case Execution Time (WCET). A crucial requirement of this estimate is that it must be safe, that is, it must be guaranteed above the real WCET. Because we are looking to prove that the system in question terminates reasonably quickly, an overapproximation is the only acceptable form of approximation. The guarantee of such a safety property could not sensibly be done without static analysis, as a result based on a battery of tests could not be safe without an exhaustive handling of test cases. Furthermore, in the absence of a certified compiler (and tech- nique for the safe transfer of properties to the binaries), the extraction of properties must be done directly on binary code to warrant their soundness. However, this approximation comes with a cost : an important pessimism, the gap between the estimated WCET and the real WCET, would lead to superfluous extra costs in hardware in order for the system to respect the imposed timing requirements. It is therefore important to improve the precision of the WCET by reducing this gap, while maintaining the safety property, as such that it is low enough to not lead to immoderate costs. A major cause of overestimation is the inclusion of semantically impossible paths, said infeasible paths, in the WCET computation. This is due to the use of the Implicit Path Enumeration Technique (IPET), which works on an superset of the possible execution paths. When the Worst-Case Execution Path (WCEP), corresponding to the estimated WCET, is infeasible, the precision of that estimation is negatively affected. In order to deal with this loss of precision, this thesis proposes an infeasible paths detection technique, enabling the improvement of the precision of static analyses (namely for WCET estimation) by notifying them of the infeasibility of some paths of the program. This information is then passed as data flow properties, formatted in the FFX portable annotation language, and allowing the communication of the results of our infeasible path analysis to other analyses.

Ce travail porte sur la vérification de composants logiciels dans les systèmes embarqués critiques avioniques. Les conséquences d’une erreur dans de tels systèmes pouvant s'avérer catastrophiques, il se doivent de respecter leur spécification. La vérification formelle tend à prouver cette adéquation si elle est vraie, ou à produire un contre-exemple si elle ne l’est pas. Les méthodes actuelles ne sont pas capable de traiter les les systèmes industriels. La découverte d’informations supplémentaires (invariants) sur le système permet de réduire l’espace de recherche afin de renforcer l’objectif de preuve: les informations découvertes sont suffisantes pour conclure “facilement”. Nous définissons une architecture parallèle permettant à des méthodes de découverte d’invariants de collaborer autour d’un moteur de kinduction. Dans ce contexte nous proposons HullQe, une nouvelle heuristique de génération d’invariants potentiels combinant un calcul de pré-image par élimination de quantificateurs et des calculs d’enveloppes convexes. Nous montrons que HullQe est capable, automatiquement, de renforcer des objectifs de preuve correspondant à la vérification de patrons de conception courants en avionique. Pour autant que nous sachions, les méthodes actuelles sont incapables de conclure sur ces problèmes. Nous détaillons nos améliorations de l’algorithme d’élimination de quantificateurs de Monniaux afin d’assurer le passage à l’échelle sur nos systèmes. Notre framework formel Stuff est une implémentation de notre architecture parallèle composée de HullQe, d'une technique de découverte d’invariants basée sur des templates, et d'une généralisation de PDR à l’arithmétique. / This work studies the verification of software components in avionics critical embedded systems. As the failure of suchsystems can have catastrophic consequences, it is mandatory to make sure they are consistent with their specification.Formal verification consists in proving that a system respects its specification if it does, or to produce a counterexample if itdoes not. Current methods are unable to handle the verification problems stemming from realistic systems. Discoveringadditional information (invariants) on the system can however restrict the search space enough to strengthen the proofobjective: the information discovered allow to "easily" reach a conclusion. We define a parallel architecture for invariantdiscovery methods allowing them to collaborate around a k-induction engine. In this context we propose a new heuristic forthe generation of potential invariants by combining an iterated preimage calculus by quantifier elimination with convexhull computations, called HullQe. We show that HullQe is able to automatically strengthen proof objectives correspondingto safety properties on widespread design patterns in our field. To the best of our knowledge, these systems elude currenttechniques. We also detail our improvements to the quantifier elimination algorithm by David Monniaux in 2008, so that itscales to computing preimages on our systems. Our formal framework Stuff is an implementation of the parallel architecturewe propose in which we implemented not only HullQe, but also a template-based invariant discovery technique, and ageneralisation to Property Directed Reachability to linear real arithmetic and integer octagons.

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. / This thesis studies the automatic verification of safety properties of logico-numerical discrete and hybrid systems. These systems have Boolean and numerical variables and exhibit discrete and continuous behavior. Our approach is based on static analysis using abstract interpretation. We address the following issues: Numerical abstract interpretation methods require the enumeration of the Boolean states, and hence, they suffer from the state space explosion problem. Moreover, there is a precision loss due to widening operators used to guarantee termination of the analysis. Furthermore, we want to make abstract interpretation-based analysis methods accessible to simulation languages for hybrid systems. In this thesis, we first generalize abstract acceleration, a method that improves the precision of the inferred numerical invariants. Then, we show how to extend abstract acceleration and max-strategy iteration to logico-numerical programs while improving the trade-off between efficiency and precision. Concerning hybrid systems, we translate the Zelus hybrid synchronous programming language to logico-numerical hybrid automata and extend logico-numerical analysis methods to hybrid systems. Finally, we implemented the proposed methods in ReaVer, a REActive System VERification tool, and provide experimental results. Concluding, this thesis proposes a unified approach to the verification of discrete and hybrid logico-numerical systems based on abstract interpretation, which is capable of integrating sophisticated numerical abstract interpretation methods while successfully trading precision for efficiency.

La programmation par contraintes offre des langages et des outils permettant de résoudre des problèmes à forte combinatoire et à la complexité élevée tels que ceux qui existent en vérification de programmes. Dans cette thèse nous résolvons deux familles de problèmes de la vérification de programmes. Dans chaque cas de figure nous commençons par une étude formelle du problème avant de proposer des modèles en contraintes puis de réaliser des expérimentations. La première contribution concerne un langage réactif synchrone représentable par une algèbre de diagramme de blocs. Les programmes utilisent des flux infinis et modélisent des systèmes temps réel. Nous proposons un modèle en contraintes muni d’une nouvelle contrainte globale ainsi que ses algorithmes de filtrage inspirés de l’interprétation abstraite. Cette contrainte permet de calculer des sur-approximations des valeurs des flux des diagrammes de blocs. Nous évaluons notre processus de vérification sur le langage FAUST, qui est un langage dédié à la génération de flux audio. La seconde contribution concerne les systèmes probabilistes représentés par des chaînes de Markov à intervalles paramétrés, un formalisme de spécification qui étend les chaînes de Markov. Nous proposons des modèles en contraintes pour vérifier des propriétés qualitatives et quantitatives. Nos modèles dans le cas qualitatif améliorent l’état de l’art tandis que ceux dans le cas quantitatif sont les premiers proposés à ce jour. Nous avons implémenté nos modèles en contraintes en problèmes de programmation linéaire en nombres entiers et en problèmes de satisfaction modulo des théories. Les expériences sont réalisées à partir d’un jeu d’essais de la bibliothèque PRISM. / Constraint programming offers efficient languages andtools for solving combinatorial and computationally hard problems such as the ones proposed in program verification. In this thesis, we tackle two families of program verification problems using constraint programming.In both contexts, we first propose a formal evaluation of our contributions before realizing some experiments.The first contribution is about a synchronous reactive language, represented by a block-diagram algebra. Such programs operate on infinite streams and model real-time processes. We propose a constraint model together with a new global constraint. Our new filtering algorithm is inspired from Abstract Interpretation. It computes over-approximations of the infinite stream values computed by the block-diagrams. We evaluated our verification process on the FAUST language (a language for processing real-time audio streams) and we tested it on examples from the FAUST standard library. The second contribution considers probabilistic processes represented by Parametric Interval Markov Chains, a specification formalism that extends Markov Chains. We propose constraint models for checking qualitative and quantitative reachability properties. Our models for the qualitative case improve the state of the art models, while for the quantitative case our models are the first ones. We implemented and evaluated our verification constraint models as mixed integer linear programs and satisfiability modulo theory programs. Experiments have been realized on a PRISM based benchmark.

Le comportement d'une cellule dépend de sa capacité à recevoir, propager et intégrer des signaux, constituant ainsi des voies de signalisations. Les protéines s'associent entre elles sur des sites de liaisons, puis modifient la structure spatiale des protéines voisines, ce qui a pour effet de cacher ou de découvrir leurs autres sites de liaisons, et donc d'empêcher ou de faciliter d'autres interactions. En raison du grand nombre de différents complexes bio-moléculaires, nous ne pouvons pas écrire ou générer les systèmes différentiels sous-jacents. Les langages de réécritures de graphes à sites offrent un bon moyen de décrire ces systèmes complexes. Néanmoins la complexité combinatoire resurgit lorsque l'on cherche à calculer de manière effective ce comportement. Ceci justifie l'utilisation d'abstractions. Nous proposons deux méthodes pour réduire la taille des modèles de voies de signalisation, décrits en Kappa. Ces méthodes utilisent respectivement la présence de symétries parmi certains sites et le fait que certaines corrélations entre l'état de différentes parties des complexes biomoléculaires n'ont pas d'impact sur la dynamique du système global. Des sites qui ont la même capacité d'interaction sont liés par une relation de symétrie. Nous montrons que cette relation induit une bisimulation qui peut être utilisée pour réduire la taille du modèle initial. L'analyse du flot d'information détecte les parties du système qui influencent le comportement de chaque site. Ceci nous autorise à couper les espèces moléculaires en petits morceaux pour écrire un nouveau système. Enfin, nous montrons comment raffiner cette analyse pour tenir compte d'information contextuelle. Les deux méthodes peuvent être combinées. La solution analytique du modèle réduit est la projection exacte de la solution originelle. Le calcul du modèle réduit se fait au niveau des règles, en évitant l'exécution du modèle initial. / The behaviour of a cell is driven by its capability to receive, propagate and communicate signals. Proteins can bind together on some binding sites. Post-translational modifications can reveal or hide some sites, so new interactions can be allowed or existing ones can be inhibited. Due to the huge number of different bio-molecular complexes, we can no longer derive or integrate ODE models. A compact way to describe these systems is supplied by rule-based languages. However combinatorial complexity raises again when one attempt to describe formally the behaviour of the models. This motivates the use of abstractions. We propose two methods to reduce the size of the models, that exploit respectively the presence of symmetries between sites and the lack of correlation between different parts of the system. The symmetries relates pairs of sites having the same capability of interactions. We show that this relation induces a bisimulation which can be used to reduce the size of the original model. The information flow analysis detects, for each site, which parts of the system influence its behaviour. This allows us to cut the molecular species in smaller pieces and to write a new system. Moreover we show how this analysis can be tuned with respect to a context. Both approaches can be combined. The analytical solution of the reduced model is the exact projection of the original one. The computation of the reduced model is performed at the level of rules, without the need of executing the original model.