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

La complexité et l'hétérogènité des MPSoC sont accentuées par l'émergence de nouvelles applications multimédia. Pour ce genre d'architectures MPSoC, les environnements de programmation classiques ne sont pas adaptés. Cette thèse propose un flot de conception du logiciel pour MPSoC. Le flot commence par un modèle de haut niveau de l'application et de l'architecture en Simulink. La génération et la validation du logiciel sont effectuées graduellement en partant de ce premier modèle, correspondant à différents niveaux d'abstraction. Des plateformes spécifiques de développement sont employées pour permettre le débogage des différents composants logiciels. Le flot proposé a été appliqué pour la génération et validation du logiciel pour plusieurs architectures MPSoC, qui contiennent plusieurs processeurs interconnectés par un bus ou un réseau sur puce, et exécutent des applications, comme l'encodeur H.264, le décodeur M-JPEG et le décodeur MP3.

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

Cette thèse présente un schéma formel et efficace pour la vérification de systèmes temps-réel. Ce schéma repose sur la combinaison par abstraction de techniques déductives et de model checking, et cette combinaison permet de contourner les limites de chacune de ces techniques. La méthode utilise le raffinement itératif abstrait (IAR) pour le calcul d'abstractions finies. Etant donné un système de transitions et un ensemble fini de prédicats, la méthode détermine une abstraction booléenne dont les états correspondent à des ensembles de prédicats. La correction de l'abstraction par rapport au système d'origine est garantie en établissant un ensemble de conditions de vérification, issues de la procédure IAR. Ces conditions sont à démontrer à l'aide d'un prouveur de théorèmes. Les propriétés de sûreté et de vivacité sont ensuite vérifiées par rapport au modèle abstrait. La procédure IAR termine lorsque toutes les conditions sont vérifiées. Dans le cas contraire, une analyse plus fine détermine si le modèle abstrait doit être affiné en considérant davantage de prédicats. Nous identifions une classe de diagrammes de prédicats appelés PDT (Predicate Diagram for Timed system) qui décrivent l'abstraction et qui peuvent être utilisés pour la vérification de systèmes temporisés et paramétrés.

EB-3 est un langage de spécification développé pour la spécification des systèmes d'information. Le noyau du langage EB-3comprend des spécifications d'algèbre de processus afin de décrire le comportement des entités du système et des fonctions d'attributs qui sont des fonctions récursives dont l'évaluation se fait sur la trace d'exécution du système décrivant les attributs des entités. La vérification de propriétés temporelles en EB-3 est un sujet de grande importance pour des utilisateurs de EB-3. Dans cette thèse, on se focalise sur les propriétés de vivacité concernant des systèmes d'information exprimant l'éventualité que certaines actions puissent s'exécuter. La vérification des propriétés de vivacité se fait à l'aide de model checking. Dans un premier temps, on présente une sémantique opérationnelle deEB-3, selon laquelle les fonctions d'attributs sont évaluées pendant l'exécution du programme puis stockées. Cette sémantique nous permet de définir une traduction automatique de EB-3 vers LNT, qui est un langage simultané enrichi d'une algèbre de processus. Notre traduction assure la correspondance un à un entre les états et les transitions des systèmes étiquetés de transition correspondent respectivement à des spécifications EB-3 et LNT. Ensuite, on automatise la traduction grâce à l'outil EB3toLNT fournissant aux utilisateurs de EB-3 une tous les outils de vérification fonctionnelle disponible dans CADP. Dans le but d'améliorer les résultats de notre approche concernant le model checking, on explore des techniques d'abstraction dédiées aux systèmes d'information spécifiées en EB-3. En particulier, on se focalise sur une famille spécifique de systèmes qui s'appellent paramétriques dont le comportement varie en fonction de la valeur prédéfinie d'un paramètre du système. Enfin, on applique cette méthode dans le contexte de EB-3 / EB-3 is a specification language for information systems. The core of the EB-3 language consists of process algebraic specifications describing the behaviour of entities in a system, and attribute functions that are recursive functions evaluated on the system execution trace describing entity attributes. The verification ofEB-3 specifications against temporal properties is of great interest to users of EB-3. In this thesis, we focus on liveness properties of information systems, which express the eventuality that certain actions take place. The verification of liveness properties can beachieved with model checking. First, we present an operational semantics for EB-3 programs, in which attribute functions are computed during program evolution and their values are stored into program memory. This semantics permits us to define an automatic translation from EB-3 to LNT, a value-passing concurrent language with classical process algebra features. Our translation ensures the one-to-one correspondence between states and transitions of the labelled transition systems corresponding to theEB-3 and LNT specifications. Then, we automate this translation with the EB-3toLNT tool, thus equipping the EB-3 method with the functional verification features available in the model checking toolbox CADP. With the aim of improving the model checking results of this approach, we explore abstraction techniques for information systems specified inEB-3. In particular, we concentrate on a specific family of systems called parametric, whose behaviour is scaled in keeping with the predefined value of a system parameter. Finally, we apply this method on the EB-3 context

Les mécanismes de décision impliqués dans le switching entre tâches à la base d'un indice a été étudié intensément, p.ex. la suspension de l'exécution d'une tâche pendant la réalisation d'une autre, avec une récompense fixe. Dans ce cas, le cortex frontopolaire (CFP) est impliqué quand les sujets doivent garder en tête un but principal pendant l'exécution de buts parallèles, et le cortex cingulaire antérieur (CCA) associerait les actions à leurs résultats. Pendant ma thèse, j'ai étudié le switching à différents niveaux d'abstraction de l'action dans la prise de décision fondée sur la valeur espérée: choisir librement d'un côté entre deux actions simples, de l'autre côté entre deux structures abstraites, i.e. des tâches. Les signaux BOLD ont été enregistrés en IRMf sur des sujets sains pendant une expérience d'apprentissage inversé probabiliste, avec des probabilités de récompenses stochastiques anti-corrélées. J'ai comparé des modèles d'apprentissage par renforcement et d'inférence bayésienne afin d'en déduire pour chaque sujet les valeurs des options, qui ont été régressées contre la réponse BOLD. Les résultats montrent une implication du cortex préfrontal ventromédian et du striatum au niveau des actions, et en contraste le CFP, le CCA et le cortex préfrontal dorsolatéral au niveau des tâches. Le CFP surveille les preuves en faveur de la tâche alternative, et le CCA témoigne d'un effet tâche, prédisant le switching entre tâches, mais pas entre actions. En outre, j'ai montré un engagement spécifique du réseau préfrontal dans la prise de décision fondée sur la valeur espérée de structures abstraites à travers des analyses de connectivité.

Les systèmes sur puce sont de plus en plus complexes : ils intègrent des parties numériques, des parties analogiques et des capteurs ou actionneurs. SystemC et son extension SystemC AMS permettent aujourd'hui de modéliser à haut niveau d'abstraction de tels systèmes. Ces outils constituent de véritables atouts dans une optique d'étude de faisabilité, d'exploration architecturale et de vérification du fonctionnement global des systèmes complexes hétérogènes et multiphysiques. En effet, les durées de simulation deviennent trop importantes pour envisager les simulations globales à bas niveau d'abstraction. De plus, les simulations basées sur l'utilisation conjointe de différents outils provoquent des problèmes de synchronisation. Les modèles de bas niveau, une fois crées par les spécialistes des différents domaines peuvent toutefois être abstraits afin de générer des modèles de haut niveau simulables sous SystemC/SystemC AMS en des temps de simulations réduits. Une analyse des modèles de calcul et des styles de modélisation possibles est d'abord présentée afin d'établir un lien avec les durées de simulation, ceci pour proposer un style de modélisation en fonction du niveau d'abstraction souhaité et de la taille du modèle à simuler. Dans le cas des circuits analogiques linéaires, une méthode permettant de générer automatiquement des modèles de haut niveau d'abstraction à partir de modèles de bas niveau a été proposée. Afin d'évaluer très tôt dans le flot de conception la consommation d'un système, un moyen d'enrichir les modèles de haut niveau préalablement générés est présentée. L'attention a ensuite été portée sur la modélisation à haut niveau des systèmes multiphysiques. Deux méthodes y sont discutées : la méthode consistant à utiliser le circuit équivalent électrique puis la méthode basée sur les bond graphs. En particulier, nous proposons une méthode permettant de générer un modèle équivalent au bond graph à partir d'un modèle de bas niveau. Enfin, la modélisation d'un système éolien est étudiée afin d'illustrer les différents concepts présentés dans cette thèse.

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 systèmes hybrides sont au cœur des systèmes cyber-physiques. De tels systèmes représentent l’interaction de processus physiques continus modélisant généralement l'environnement avec des décisions discrètes issues d'un système de contrôle commande électronique. La vérification de ces systèmes est cruciale pour assurer leur sûreté dès la phase de modélisation. Les recherches sur les systèmes hybrides ont de nombreux domaines d’application, notamment le transport, l’aéronautique et la biologie. La thèse étudie des principes du raisonnement qualitatif et les applique à la vérification des systèmes hybrides. Le travail consiste à élaborer une méthode pour abstraire le système hybride en utilisant des principes qualitatifs. On recourt à une discrétisation finie de l'espace d'état tout en conservant des caractéristiques qualitatives du système. L'abstraction calculée permet de prouver des propriétés au niveau du système hybride concret et fournit une représentation du comportement global du système. Un outil développé en C++ permet de calculer l'abstraction d'un système hybride donné. Une évaluation de ses performances est établie. On s'intéresse particulièrement à une propriété de sûreté des systèmes appelée diagnosticabilité. Un modèle de système est dit diagnosticable s'il permet d'identifier sans ambiguïté la survenue de toute faute modélisée à partir des seules observations disponibles du système jusqu’à un certain délai après l’occurrence de la faute. Une méthode qui consiste à utiliser l'abstraction établie précédemment pour vérifier la diagnosticabilité d'un système hybride est proposée. / Hybrid systems are at the core of cyber-physical systems. Such systems represent the interaction between continuous physical processes generally modelling the environment with discrete decisions from control electronic signaling. The verification of these systems is crucial to ensure safety at the modeling stage. The application of hybrid systems is present in many fields such as transportation, biology and avionics. The thesis studies principals from the qualitative reasoning domain and applies them to the verification of hybrid systems. The accomplished work elaborates methods to abstract a hybrid system using qualitative principles. These methods consist in discretizing the state space to a finite number of states while conserving qualitative characteristics. The computed abstraction allows to prove properties at the level of the concrete hybrid system and presents a representation of the global behavior of the system. A tool developed in C++ computes the abstraction of a given hybrid system. An evaluation of its performance is performed. We are also interested in a particular property called diagnosability. The system is said to be diagnosable when it is capable to identify modeled faults using limited specified observations. A method that uses the computed abstraction to verify diagnosability of a given hybrid system is proposed.

Cette thèse porte sur la modélisation des systèmes-sur-puce au niveau transactionnel, une approche connue sous le nom de prototypage virtuel. Les prototypes virtuels sont d'un grand intérêt industriel parce qu'ils permettent de démarrer certaines activités (telles que le développement du logiciel embarqué) plus tôt dans le flot de conception. Du fait que cette approche est relativement nouvelle, un grand nombre de problèmes de modélisation sont encore ouverts. En particulier, il est essentiel de comprendre à quel point un modèle donné est proche du système hypothétique qu'il est sensé représenter. C'est un problème difficile car nous n'avons pas les moyens de réaliser une comparaison objective, vu que le système modélisé n'est pas disponible physiquement au moment de la modélisation. Nous avons besoin d'une méthodologie pour traiter ces difficultés, qui s'étendent au-delà de simples exigences objectives et de l'analyse de besoin fonctionnel. Dans ce contexte, l'industrie cherche des directives de modélisation claires, fondées sur l'expérience et l'identification des pratiques actuelles et des problèmes récurrents. Dans cette thèse, nous présentons une étude compréhensive d'un large éventail de considérations techniques impliquées dans le flot de conception du logiciel et du matériel qui constituent un système-sur-puce typique. Nous utilisons ces connaissances pour identifier une source particulière de divergence entre le modèle et le système modélisé. Nous montrons que cette divergence masque certains bogues du logiciel sur le prototype virtuel. Nous mettons en évidence la pratique de modélisation à l'origine de cette situation. Deuxièmement, nous essayons d'identifier des problèmes liés à l'utilisation du langage de modélisation dans les pratiques actuelles. Nous prétendons que, d'une part, ces problèmes sont dûs à la confusion entre les concepts de la modélisation transactionnelle et leur implémentation dans le langage standard de l'industrie ; et d'autre part que ce n'est qu'en menant des comparaisons avec un autre langage que l'on pourrait quantifier leur étendue. Pour ce faire, nous proposons un cadre d'application spécialement conçu pour guider l'étude des concepts fondamentaux de la modélisation transactionnelle. Entre autres, nous introduisons une nouvelle méthode pour la modélisation du temps dans les simulateurs à événements discrets. Cette méthode dévoile la différence entre une action instantanée et une tâche avec durée. Ensuite, elle l'exploite de plusieurs manières : pour enrichir les outils de visualisation de traces ; pour dériver une définition claire de chevauchement de tâches ; pour accélérer la simulation à moindre effort, en parallélisant l'exécution d'actions se déroulant à des temps simulés différents ; et pour révéler des bogues subtiles en tenant compte du fait que les actions à des temps simulés différents ne sont pas forcément synchronisées. / This thesis deals with modeling of Systems-on-a-Chip (SoC) at the Transactional Level (TLM), an approach also known as virtual prototyping. Virtual prototypes are of special industrial interest because they allow some activities (such as embedded software development) to start earlier in the design flow. Because this approach is relatively new, several modeling issues are still open. In particular, there is an increasing need for understanding how close a given model is to the hypothetical system it is intended to represent. This is a difficult problem specially because we lack a way to perform an objective comparison, since the modeling activity is prior to the physical existence of the modeled system. A methodology is required to address these concerns, going beyond classical objective and functional quality requirements. In this context, the industry searches for clear modeling guidelines based on experience and the identification of the current modeling practices and known recurring problems. In this thesis, we present a comprehensive study of a range of technical considerations involved in the design flow of the hardware and software that constitutes a typical SoC. We use this knowledge to identify one particular source of divergence between the model and the modeled system. We show that this divergence causes some software bugs to become hidden in the virtual prototype and we correlate this situation to the corresponding modeling practice. Secondly, we attempt to identify language-dependency issues in the modeling practices. We claim that it is only by confronting with an alternative language that we could measure the extent to which common modeling issues were caused by mixing up conceptual transaction-level modeling with its implementation in the current industry standard language. Therefore, we propose a complete experimentation framework specifically designed to help in the study of fundamental concepts beneath TLM. Amongst other features, this framework introduces a novel approach to modeling time in discrete-event simulators that distinguishes between instantaneous actions and tasks that take time. We show that this notion can be exploited to enrich trace visualization tools; to derive a clear definition of overlapping tasks; to effortlessly achieve an important simulation speedup by enabling parallel execution of actions occurring at different simulation times; and to expose subtle bugs by removing the constraint that actions at different simulation times are necessarily synchronized.