Dans le cadre de son offre de serveurs haut de gamme, la société Bull conçoit des multiprocesseurs à mémoire distribuée partagée avec un protocole de cohérence de cache CC-DSM (Cache-Coherent Distibuted Shared Memory), et fournit une implémentation de la bibliothèque MPI (Message Passing Interface) pour la programmation parallèle. L'évaluation des performances de cette implémentation permettra, d'une part, de faire les bons choix d'architecture matérielle et de la couche logicielle au moment de la conception et, d'autre part, fournira des éléments d'analyse nécessaires pour comprendre les mesures faites au moment de la validation de la machine réelle. Nous proposons et mettons en œuvre dans ce travail de thèse une méthodologie permettant d'évaluer les performances des algorithmes de la bibliothèque MPI (ping-pong et barrières) en tenant compte de l'architecture matérielle. Cette approche est basée sur l'utilisation des méthodes formelles, elle consiste en 3 étapes principales : 1) la modélisation en langage LOTOS des aspects matériels (topologie d'interconnexion et protocole de cohérence de cache) et logiciels (algorithmes MPI) ; 2) la vérification formelle de la correction fonctionnelle du modèle obtenu ; 3) l'évaluation des performances après l'extension du modèle par des informations quantitatives (latences des transferts des données) en utilisant des méthodes numériques et de la simulation.

L'implémenation distribuée des systèmes temps-réel a été toujous une tâche non-triviale. La coordination des composants s'exécutant sur une plate-forme distribuée doit être assurée par des protocoles de communication complexes en tenant compte de leurs contraintes de temps. Dans cette thèse, nous proposons un flot de conception rigoureux à partir d'un modèle de haut niveau d'un logiciel d'application décrit en BIP (Behavior, Interaction, Priority) et conduisant à une implémenation distribuée. Le flot de conception implique l'utilisation de transformations de modèles tout en conservant les propriétés fonctionnelles des modèles originaux de BIP. Un modèle BIP se compose d'un ensemble de composants qui se synchronisent à travers les interactions et les priorités. Notre méthode transforme les modèles BIP en un modéle Send/Receive qui fonctionnent en utilisant le passage de messages asynchrones. Les modèles obtenus sont directement implémenté sur une plate-forme donnée. Nous présentons trois solutions pour obtenir un modéle Send/Receive. Dans la première solution, nous proposons des modéles Send/Receive qui fonctionnent avec un engin centralisé qui implémente les interactions et les priorités. Les composants atomiques des modèles originaux sont transformés en composants Send/Receive qui communiquent avec l'engin centralisé via des interactions Send/Receive. L'engin centralisé exécute les interactions sous certaines conditions définies par les modèles à états partiels. Ces modèles représentent une déscription haut niveau de l'exécution parallèle de modèles BIP. Dans la deuxième solution, nous proposons de décentraliser l'engin. Les modéles Send/Receive obtenus sont structurées en trois couches: (1) les composants Send/Receive (2) un ensemble d'engin, chacun exécutant un sous-ensemble d'interactions, et (3) un ensemble de composants implémentant un protocole de résolution des conflits. Avec les solutions décrites ci-dessus, nous supposons que les latences de communication sont négligeables. Ceci est du au fait que les modéles Send/Receive sont concu de telle sorte qu'il n'y ait pas retard entre la décision d'exécuter une interaction dans un engin et son exécution dans les composants participant. Dans la troisième solution, nous proposons des modéles Send/ Receive qui exécutent correctement même en présence de latences de communication. Cette solution est basée sur le fait que les engin planifient l'exécution des interactions et notifient les composants à l'avance. Afin de planifier correctement les interactions, nous montrons que les engins sont tenus à observer des composants supplémentaires, en plus de ceux qui participent aux interactions. Nous présentons également une méthode pour optimiser le nombre de composants observés, en se basant sur l'utilisation de techniques d'analyse statique. A partir d'un modéle Send/Receive donné, nous générons une application distribuée où les interactions Send/Receive sont implémentées par les sockets TCP. Les résultats expérimentaux sur des exemples non triviaux et des études de cas montrent l'efficacité de notre méthode. / Correct distributed implementation of real-time systems has always been a challenging task. The coordination of components executing on a distributed platform has to be ensured by complex communication protocols taking into account their timing constraints. In this thesis, we propose rigorous design flow starting from a high-level model of an application software in BIP (Behavior, Interaction, Priority) and leading to a distributed implementation. The design flow involves the use of model transformations while preserving the functional properties of the original BIP models. A BIP model consists of a set of components synchronizing through multiparty interactions and priorities. Our method transforms high-level BIP models into Send/Receive models that operate using asynchronous message passing. The obtained models are directly implementable on a given platform. We present three solutions for obtaining Send/Receive BIP models. -In the first solution, we propose Send/Receive models with a centralized scheduler that implements interactions and priorities. Atomic components of the original models are transformed into Send/Receive components that communicate with the centralized scheduler via Send/Receive interactions. The centralized scheduler is required to schedule interactions under some conditions defined by partial state models. Those models represent high-level representation of parallel execution of BIP models. - In the second solution, we propose to decentralize the scheduler. The obtained Send/Receive models are structured in 3 layers: (1) Send/Receive atomic components, (2) a set of schedulers each one handling a subset of interactions, and (3) a set of components implementing a conflict resolution protocol. With the above solutions, we assume that the obtained Send/Receive models are implemented on platforms that provide fast communications (e.g. multi-process platforms) to meet perfect synchronization in components. This is because the obtained schedulers are modeled such that interactions scheduling corresponds exactly to execution in components. - In the third solution, we propose Send/Receive models that execute correctly even if communications are not fast enough. This solution is based on the fact that schedulers plan interactions execution and notify components in advance. In order to plan correctly the interactions, we show that the schedulers are required to observe additional components, in addition to the ones participating in the interactions. We present also a method to optimize the number of observed components, based on the use of static analysis techniques. From a given Send/Receive model, we generate a distributed implementation where Send/Receive interactions are implemented by TCP sockets. The experimental results on non trivial examples and case studies show the efficiency of our design flow.

Cette thèse propose un cadre afin de modéliser, vérifier et générer des allocations de fonctions d'un système embarqué sur des ressources avioniques. Ce cadre est fondé sur l'utilisation du langage Altarica pour décrire formellement la propagation des défaillances au sein d'un système embarqué, sur l'utilisation de techniques de vérification tel que le "model-checking" et la génération d'arbre de défaillances et sur les techniques de résolution de contraintes. Les travaux sont illustrés par deux études de cas: l'allocation de ressources de calcul et de communication à une fonction de "suivi de terrain" d'un avion de chasse, le placement des équipements d'un système hydraulique au sein d'un avion en tenant compte de risques tels que l'éclatement d'un pneu ou d'un réacteur.

L'implémenation distribuée des systèmes temps-réel a été toujous une tâche non-triviale. La coordination des composants s'exécutant sur une plate-forme distribuée doit être assurée par des protocoles de communication complexes en tenant compte de leurs contraintes de temps. Dans cette thèse, nous proposons un flot de conception rigoureux à partir d'un modèle de haut niveau d'un logiciel d'application décrit en BIP (Behavior, Interaction, Priority) et conduisant à une implémenation distribuée. Le flot de conception implique l'utilisation de transformations de modèles tout en conservant les propriétés fonctionnelles des modèles originaux de BIP. Un modèle BIP se compose d'un ensemble de composants qui se synchronisent à travers les interactions et les priorités. Notre méthode transforme les modèles BIP en un modéle Send/Receive qui fonctionnent en utilisant le passage de messages asynchrones. Les modèles obtenus sont directement implémenté sur une plate-forme donnée. Nous présentons trois solutions pour obtenir un modéle Send/Receive. Dans la première solution, nous proposons des modéles Send/Receive qui fonctionnent avec un engin centralisé qui implémente les interactions et les priorités. Les composants atomiques des modèles originaux sont transformés en composants Send/Receive qui communiquent avec l'engin centralisé via des interactions Send/Receive. L'engin centralisé exécute les interactions sous certaines conditions définies par les modèles à états partiels. Ces modèles représentent une déscription haut niveau de l'exécution parallèle de modèles BIP. Dans la deuxième solution, nous proposons de décentraliser l'engin. Les modéles Send/Receive obtenus sont structurées en trois couches: (1) les composants Send/Receive (2) un ensemble d'engin, chacun exécutant un sous-ensemble d'interactions, et (3) un ensemble de composants implémentant un protocole de résolution des conflits. Avec les solutions décrites ci-dessus, nous supposons que les latences de communication sont négligeables. Ceci est du au fait que les modéles Send/Receive sont concu de telle sorte qu'il n'y ait pas retard entre la décision d'exécuter une interaction dans un engin et son exécution dans les composants participant. Dans la troisième solution, nous proposons des modéles Send/ Receive qui exécutent correctement même en présence de latences de communication. Cette solution est basée sur le fait que les engin planifient l'exécution des interactions et notifient les composants à l'avance. Afin de planifier correctement les interactions, nous montrons que les engins sont tenus à observer des composants supplémentaires, en plus de ceux qui participent aux interactions. Nous présentons également une méthode pour optimiser le nombre de composants observés, en se basant sur l'utilisation de techniques d'analyse statique. A partir d'un modéle Send/Receive donné, nous générons une application distribuée où les interactions Send/Receive sont implémentées par les sockets TCP. Les résultats expérimentaux sur des exemples non triviaux et des études de cas montrent l'efficacité de notre méthode. / Correct distributed implementation of real-time systems has always been a challenging task. The coordination of components executing on a distributed platform has to be ensured by complex communication protocols taking into account their timing constraints. In this thesis, we propose rigorous design flow starting from a high-level model of an application software in BIP (Behavior, Interaction, Priority) and leading to a distributed implementation. The design flow involves the use of model transformations while preserving the functional properties of the original BIP models. A BIP model consists of a set of components synchronizing through multiparty interactions and priorities. Our method transforms high-level BIP models into Send/Receive models that operate using asynchronous message passing. The obtained models are directly implementable on a given platform. We present three solutions for obtaining Send/Receive BIP models. -In the first solution, we propose Send/Receive models with a centralized scheduler that implements interactions and priorities. Atomic components of the original models are transformed into Send/Receive components that communicate with the centralized scheduler via Send/Receive interactions. The centralized scheduler is required to schedule interactions under some conditions defined by partial state models. Those models represent high-level representation of parallel execution of BIP models. - In the second solution, we propose to decentralize the scheduler. The obtained Send/Receive models are structured in 3 layers: (1) Send/Receive atomic components, (2) a set of schedulers each one handling a subset of interactions, and (3) a set of components implementing a conflict resolution protocol. With the above solutions, we assume that the obtained Send/Receive models are implemented on platforms that provide fast communications (e.g. multi-process platforms) to meet perfect synchronization in components. This is because the obtained schedulers are modeled such that interactions scheduling corresponds exactly to execution in components. - In the third solution, we propose Send/Receive models that execute correctly even if communications are not fast enough. This solution is based on the fact that schedulers plan interactions execution and notify components in advance. In order to plan correctly the interactions, we show that the schedulers are required to observe additional components, in addition to the ones participating in the interactions. We present also a method to optimize the number of observed components, based on the use of static analysis techniques. From a given Send/Receive model, we generate a distributed implementation where Send/Receive interactions are implemented by TCP sockets. The experimental results on non trivial examples and case studies show the efficiency of our design flow.

LNT est un langage formel de spécification récent, basé sur les algèbres de processus, où plusieurs processus concurrents et asynchrones peuvent interagir par rendez-vous multiple, c'est-à-dire à deux ou plus, avec échange de données. La boite à outils CADP (Construction and Analysis of Distributed Processes) offre plusieurs techniques relatives à l'exploration d'espace d'états, comme le model checking, pour vérifier formellement une spécification LNT. Cette thèse présente une méthode de génération d'implémentation distribuée à partir d'un modèle formel LNT décrivant une composition parallèle de processus. En s'appuyant sur CADP, nous avons mis au point le nouvel outil DLC (Distributed LNT Compiler), capable de générer, à partir d'une spécification LNT, une implémentation distribuée en C qui peut ensuite être déployée sur plusieurs machines distinctes reliées par un réseau. Pour implémenter de manière correcte et efficace les rendez-vous multiples avec échange de données entre processus distants, nous avons élaboré un protocole de synchronisation qui regroupe différentes approches proposées par le passé. Nous avons mis au point une méthode de vérification de ce type de protocole qui, en utilisant LNT et CADP, permet de détecter des boucles infinies ou des interblocages dus au protocole, et de vérifier que le protocole réalise des rendez-vous cohérents par rapport à une spécification donnée. Cette méthode nous a permis d'identifier de possibles interblocages dans un protocole de la littérature, et de vérifier le bon comportement de notre propre protocole. Nous avons aussi développé un mécanisme qui permet, en embarquant au sein d'une implémentation des procédures C librement définies par l'utilisateur, de mettre en place des interactions entre une implémentation générée et d'autres systèmes de son environnement. Enfin, nous avons appliqué DLC au nouvel algorithme de consensus Raft, qui nous sert de cas d'étude, notamment pour mesurer les performances d'une implémentation générée par DLC. / LNT is a recent formal specification language, based on process algebras, where several concurrent asynchronous processes can interact by multiway rendezvous (i.e., involving two or more processes), with data exchange. The CADP (Construction and Analysis of Distributed Processes) toolbox offers several techniques related to state space exploration, like model checking, to formally verify an LNT specification. This thesis introduces a distributed implementation generation method, starting from an LNT formal model of a parallel composition of processes. Taking advantage of CADP, we developed the new DLC (Distributed LNT Compiler) tool, which is able to generate, from an LNT specification, a distributed implementation in C that can be deployed on several distinct machines linked by a network. In order to handle multiway rendezvous with data exchange between distant processes in a correct and efficient manner, we designed a synchronization protocol that gathers different approaches suggested in the past. We set up a verification method for this kind of protocol, which, using LNT and CADP, can detect livelocks or deadlocks due to the protocol, and also check that the protocol leads to valid interactions with respect to a given specification. This method allowed us to identify possible deadlocks in a protocol from the literature, and to verify the good behavior of our own protocol. We also designed a mechanism that enables the final user, by embedding user-defined C procedures into the implementation, to set up interactions between the generated implementation and other systems in the environment. Finally, we used the new consensus algorithm Raft as a case study, in particular to measure the performances of an implementation generated by DLC.

La miniaturisation de la gravure et l'ajustement dynamique du voltage augmentent le risque de fautes dans les circuits intégrés. Pour pallier cet inconvénient, les ingénieurs utilisent des techniques de tolérance aux fautes pour masquer ou, au moins, détecter les fautes. Ces techniques sont particulièrement utilisées dans les domaines critiques (aérospatial, médical, nucléaire, etc.) où les garanties de bon fonctionnement des circuits et leurs tolérance aux fautes sont cruciales. Cependant, la vérification de propriétés fonctionnelles et de tolérance aux fautes est un problème complexe qui ne peut être résolu par simulation en raison du grand nombre d'exécutions possibles et de scénarios d'occurrence des fautes. De même, l'optimisation des surcoûts matériels ou temporels imposés par ces techniques demande de garantir que le circuit conserve ses propriétés de tolérance aux fautes après optimisation.Dans cette thèse, nous décrivons une optimisation de techniques de tolérance aux fautes classiques basée sur des analyses statiques, ainsi que de nouvelles techniques basées sur la redondance temporelle. Nous présentons comment leur correction peut être vérifiée formellement à l'aide d'un assistant de preuves.Nous étudions d'abord comment certains voteurs majoritaires peuvent être supprimés des circuits basés sur la redondance matérielle triple (TMR) sans violer leurs propriétés de tolérance. La méthodologie développée prend en compte les particularités des circuits (par ex. masquage logique d'erreurs) et des entrées/sorties pour optimiser la technique TMR.Deuxièmement, nous proposons une famille de techniques utilisant la redondance temporelle comme des transformations automatiques de circuits. Elles demandent moins de ressources matérielles que TMR et peuvent être facilement intégrés dans les outils de CAO. Les transformations sont basées sur une nouvelle idée de redondance temporelle dynamique qui permet de modifier le niveau de redondance «à la volée» sans interrompre le calcul. Le niveau de redondance peut être augmenté uniquement dans les situations critiques (par exemple, au-dessus des pôles où le niveau de rayonnement est élevé), lors du traitement de données cruciales (par exemple, le cryptage de données sensibles), ou pendant des processus critiques (par exemple, le redémarrage de l'ordinateur d'un satellite).Troisièmement, en associant la redondance temporelle dynamique avec un mécanisme de micro-points de reprise, nous proposons une transformation avec redondance temporelle double capable de masquer les fautes transitoires. La procédure de recouvrement est transparente et le comportement entrée/sortie du circuit reste identique même lors d'occurrences de fautes. En raison de la complexité de cette méthode, la garantie totale de sa correction a nécessité une certification formelle en utilisant l'assistant de preuves Coq. La méthodologie développée peut être appliquée pour certifier d'autres techniques de tolérance aux fautes exprimées comme des transformations de circuits. / Technology shrinking and voltage scaling increase the risk of fault occurrences in digital circuits. To address this challenge, engineers use fault-tolerance techniques to mask or, at least, to detect faults. These techniques are especially needed in safety critical domains (e.g., aerospace, medical, nuclear, etc.), where ensuring the circuit functionality and fault-tolerance is crucial. However, the verification of functional and fault-tolerance properties is a complex problem that cannot be solved with simulation-based methodologies due to the need to check a huge number of executions and fault occurrence scenarios. The optimization of the overheads imposed by fault-tolerance techniques also requires the proof that the circuit keeps its fault-tolerance properties after the optimization.In this work, we propose a verification-based optimization of existing fault-tolerance techniques as well as the design of new techniques and their formal verification using theorem proving. We first investigate how some majority voters can be removed from Triple-Modular Redundant (TMR) circuits without violating their fault-tolerance properties. The developed methodology clarifies how to take into account circuit native error-masking capabilities that may exist due to the structure of the combinational part or due to the way the circuit is used and communicates with the surrounding device.Second, we propose a family of time-redundant fault-tolerance techniques as automatic circuit transformations. They require less hardware resources than TMR alternatives and could be easily integrated in EDA tools. The transformations are based on the novel idea of dynamic time redundancy that allows the redundancy level to be changed "on-the-fly" without interrupting the computation. Therefore, time-redundancy can be used only in critical situations (e.g., above Earth poles where the radiation level is increased), during the processing of crucial data (e.g., the encryption of selected data), or during critical processes (e.g., a satellite computer reboot).Third, merging dynamic time redundancy with a micro-checkpointing mechanism, we have created a double-time redundancy transformation capable of masking transient faults. Our technique makes the recovery procedure transparent and the circuit input/output behavior remains unchanged even under faults. Due to the complexity of that method and the need to provide full assurance of its fault-tolerance capabilities, we have formally certified the technique using the Coq proof assistant. The developed proof methodology can be applied to certify other fault-tolerance techniques implemented through circuit transformations at the netlist level.

Les systèmes critiques dépendent du fait que leurs composants logiciels fournissent des services aux comportements corrects (c'est-à-dire satisfaisant leurs exigences). De plus, dans de nombreux cas, ces systèmes doivent être adaptés ou reconfigurés en cas de pannes ou quand des évolutions d'exigences ou de qualité de service se produisent. Quand ces évolutions peuvent être capturées au niveau logiciel, il devient possible de les traiter en utilisant la notion de substitution. En effet, le composant logiciel du système source peut être substitué par un autre composant logiciel pour construire un nouveau système cible. Dans le cas de systèmes critiques, cette opération impose que le nouveau système cible se comporte correctement en préservant, autant que possible, les propriétés de sécurité et de sûreté du système source pendant et après l'opération de substitution. Dans cette thèse, les systèmes étudiés sont modélisés par des systèmes états-transitions. Pour modéliser la substitution de systèmes, la méthode Event-B a été choisie car elle est adaptée à la modélisation de systèmes états-transitions et permet de bénéficier des avantages du raffinement, de la preuve et de la disponibilité d'un outil puissant avec la plate-forme Rodin.Cette thèse fournit un modèle générique pour la substitution de systèmes qui inclut différentes situations comme le démarrage à froid et le démarrage à chaud, mais aussi la possibilité de dégradation ou d'extension de systèmes ou de substitution équivalente. Cette approche est d'abord utilisée pour formaliser la substitution dans le cas de systèmes discrets appliqués à la compensation de Services Web. Elle permet de modéliser la compensation correcte. Par la suite, cette approche est mise en œuvre dans le cas des systèmes caractérisés par des comportements continus comme les systèmes hybrides. Pour modéliser des comportements continus avec Event-B, le plug-in Theory pour Rodin est examiné et s'avère performant pour modéliser des systèmes hybrides. Cela nous permet de proposer un mécanisme de substitution correct pour des systèmes avec des comportements continus. L'exigence de sûreté devient alors le maintien de la sortie du système dans une enveloppe de sûreté. Pour finir, l'approche proposée est généralisée, permettant la dérivation des modèles précédemment définis pour la compensation de Services Web par le raffinement et la réutilisation de preuves entre des modèles de systèmes. / Safety-critical systems depend on the fact that their software components provide services that behave correctly (i.e. satisfy their requirements). Additionally, in many cases, these systems have to be adapted or reconfigured in case of failures or when changes in requirements or in quality of service occur. When these changes appear at the software level, they can be handled by the notion of substitution. Indeed, the software component of the source system can be substituted by another software component to build a new target system. In the case of safety-critical systems, it is mandatory that this operation enforces that the new target system behaves correctly by preserving the safety properties of the source system during and after the substitution operation.In this thesis, the studied systems are modeled as state-transition systems. In order to model system substitution, the Event-B method has been selected as it is well suited to model such state-transition systems and it provides the benefits of refinement, proof and the availability of a strong tooling with the Rodin Platform.This thesis provides a generic model for system substitution that entails different situations like cold start and warm start as well as the possibility of system degradation, upgrade or equivalence substitutions. This proposal is first used to formalize substitution in the case of discrete systems applied to web services compensation and allowed modeling correct compensation. Then, it is also used for systems characterized by continuous behaviors like hybrid systems. To model continuous behaviors with Event-B, the Theory plugin for Rodin is investigated and proved successful for modeling hybrid systems. Afterwards, a correct substitution mechanism for systems with continuous behaviors is proposed. A safety envelope for the output of the system is taken as the safety requirement. Finally, the proposed approach is generalized, enabling the derivation of the previously defined models for web services compensation through refinement, and the reuse of proofs across system models.

Au-delà de la formidable évolution en termes de complexité du circuit électronique en soi, son adoption et sa diffusion ont connu, au fil des dernières années, une explosion dans un très grand nombre de domaines distincts. Un système sur puce peut incorporer une combinaison de composants aux fonctionnalités très différentes. S'assurer du bon fonctionnement de chaque composant, et du système complet, est une tâche primordiale et épineuse. Dans ce contexte, l'Assertion-Based Verification (ABV) a considérablement gagné en popularité ces dernières années : il s'agit d'une démarche de vérification où des propriétés logico-temporelles, exprimées dans des langages tels que PSL ou SVA, spécifient le comportement attendu du design. Alors que la plupart des solutions d'ABV existantes se limitent au niveau transfert de registres (RTL), la contribution décrite dans cette thèse s'efforce de résoudre un certain nombre de limitations et vise ainsi une solution mature pour le niveau transactionnel (TLM) de SystemC. Une technique efficace de construction de moniteurs de surveillance à partir de propriétés PSL est proposée : cette technique, inspirée d'une approche originale existante pour le niveau RTL, est ici adaptée à SystemC TLM. Une méthode spécifique de surveillance des actions de communication à haut niveau d'abstraction est également détaillée. Les possibilités offertes par la technique présentée sont significativement étendues en proposant, pour les propriétés écrites en langage PSL, à la fois un support formel et une mise en oeuvre pratique pour des variables auxiliaires globales et locales, qui constituent un élément essentiel lors des spécifications à haut niveau d'abstraction. Tous ces concepts sont également implémentés dans un outil prototype. Afin d'illustrer l'intérêt de la solution proposée, diverses expérimentations sont effectuées avec des designs aux dimensions et complexités différentes. Les résultats obtenus permettent de souligner le fait que la méthode de vérification dynamique suggérée reste applicable pour des designs de taille réaliste. / Over the last years, the growing of electronic circuit complexity has experienced a tremendous evolution. Moreover, electronic circuits have become widespread elements in many different areas. This development leads to Systems-on-Chip incorporating a combination of components with highly heterogeneous features. Ensuring the correct behavior of each component, as well as validating the behavior of the whole system, is both a compelling and painful task. In this context, Assertion-Based Verification (ABV) has widely gained acceptance over the recent years : following this approach, temporal properties expressed using languages such as PSL or SVA specify the expected behavior of the design. While most existing ABV solutions are restricted to the register transfer level (RTL), the work of this thesis attempts to overcome some limitations by developing an actual ABV solution for the transaction level modeling (TLM) in SystemC. An effective technique for the construction of checker modules from PSL properties is proposed : this technique for SystemC TLM is inspired from a pioneering approach for RTL. A specific method for monitoring communication activities at a high level of abstraction is also described. The scope of the proposed technique is significantly improved by adding to PSL both a formal and a practical support for auxiliary global and local variables, which are compelling in higher level specifications. All these concepts are implemented in a prototype tool. In order to present the applicability of the proposed solution, we performed various experiments using designs of different sizes and complexities. The experimental results show that this dynamic verification methodology is also suitable for real-world designs.

Cette thèse cherche à résoudre en pratique le problème de couverture dans les réseaux de Petri et les systèmes de canaux à pertes (LCS). Ces systèmes sont intéressants à étudier car ils permettent de modéliser facilement les systèmes concurrents et les systèmes distribués. Le problème de couverture dans un système de transitions consiste à savoir si on peut, à partir d’un état initial arriver à un état plus grand qu’un état cible. La résolution de ce problème dans les systèmes de transitions bien structurés (WSTS) sera le sujet d’études de la première partie. Les réseaux de Petri et les LCS sont des WSTS. On donnera dans la première partie une méthode générale pour le résoudre rapidement en pratique. Cette méthode utilise des invariants de couverture, qui sont des sur-approximations de l’ensemble des états couvrables. La seconde partie sera consacrée aux réseaux de Petri. Elle présentera diverses comparaisons théoriques et pratiques de différents invariants de couverture. Nous nous intéresserons notamment à la combinaison de l’invariant classique de l’inéquation d’état avec une analyse de signe simple. Les LCS seront le sujet d’études de la troisième partie. On présentera une variante de l’inéquation d’état adaptée aux LCS ainsi que deux invariants qui retiennent des propriétés sur l’ordre dans lequel les messages sont envoyés. La thèse a mené à la création de deux outils, ICover et BML, pour résoudre le problème de couverture respectivement dans les réseaux de Petri et dans les LCS. / The goal of this thesis is to solve in practice the coverability problem in Petri nets and lossy channel systems (LCS). These systems are interesting to study because they can be used to model concurrent and distributed systems. The coverability problem in a transition system is to decide whether it is possible, from an initial state, to reach a greater state than a target state. In the first part, we discuss how to solve this problem for well-structured transition systems (WSTS). Petri nets and LCS are WSTS. In the first part, we present a general method to solve this problem quickly in practice. This method uses coverability invariants, which are over-approximations of the set of coverable states. The second part studies Petri nets.We present comparisons of coverability invariants, both in theory and in practice. A particular attention will be paid on the combination of the classical state inequation and a simple sign analysis. LCS are the focus of the third part. We present a variant of the state inequation for LCS and two invariants that compute properties for the order in which messages are sent. Two tools, ICover and BML, were developed to solve the coverability problem in Petri nets and LCS respectively.

La vérification de logiciels repose le plus souvent sur une spécification formelle encodant les propriétés du programme à vérifier. La tâche de spécification et de vérification déductive des programmes est longue et difficile et nécessite une connaissance des outils de preuve de programmes. En effet, un échec de preuve de programme peut être dû à une non-conformité du code par rapport à sa spécification, à un contrat de boucle ou de fonction appelée trop faible pour prouver une autre propriété, ou à une incapacité du prouveur. Il est souvent difficile pour l’utilisateur de décider laquelle de ces trois raisons est la cause de l’échec de la preuve car cette information n’est pas (ou rarement) donnée par le prouveur et requiert donc une revue approfondie du code et de la spécification. L’objectif de cette thèse est de fournir une méthode de diagnostic automatique des échecs de preuve afin d’améliorer le processus de spécification et de preuve des programmes C. Nous nous plaçons dans le cadre de la plate-forme d’analyse des programmes C FRAMA-C, qui fournit un langage de spécification unique ACSL, un greffon de vérification déductive WP et un générateur de tests structurels PATHCRAWLER. La méthode que nous proposons consiste à diagnostiquer les échecs de preuve en utilisant la génération de tests structurels sur une version instrumentée du programme d’origine / Software verification often relies on a formal specification encoding the program properties to check. Formally specifying and deductively verifying programs is difficult and time consuming and requires some knowledge about theorem provers. Indeed, a proof failure for a program can be due to a noncompliance between the code and its specification, a loop or callee contrat being insufficient to prove another property, or a prover incapacity. It is often difficult for the user to decide which one of these three reasons causes a given proof failure. Indeed, this feedback is not (or rarely) provided by the theorem prover thus requires a thorough review of the code and the specification. This thesis develops a method to automatically diagnose proof failures and facilitate the specification and verification task. This work takes place within the analysis framework for C programs FRAMAC, that provides the specification language ACSL, the deductive verification plugin WP, and the structural test generator PATHCRAWLER. The proposed method consists in diagnosing proof failures using structural test generation on an instrumented version of the program under verification.