Notre thèse traite la complétive objet et ses prédicats introducteurs en chinois. Nous adoptons, dans l’ensemble, le cadre théorique du lexique-grammaire de Gross (1984) et dans l’analyse concrète, celle de la structure prédicative de Muller (2001). Elle est divisée en cinq chapitres. Dans le premier « Etat des lieux », nous présentons la conception de la complétive en tant qu’un type de subordonnée et nous adoptons l’analyse de la dépendance énonciative de Muller (1996). Ensuite nous présentons quelques analyses qui intègre la sémantique dans l’analyse de la complétive. Le chapitre 2 a pour objectif de délimiter notre objet d’étude, qui inclut trois sous-types : la complétive propositionnelle, le complément verbal sans sujet syntaxique (l’équivalent de la complétive infinitive du français) et l’interrogative indirecte dont la spécificité sémantique est bien prise en compte.Dans le troisième chapitre nous étudions les propriétés de sélection des prédicats introducteurs de la complétive en chinois : celles concernant le complément nominal et verbal sans sujet syntaxique d’une part, et celle entre la complétive déclarative et l’II d’autre part, à propos de laquelle nous étudions aussi les éléments qui la modifient. Dans le chapitre 4 la complétive objet est mise en parallèles avec trois autre types de constructions qui partagent le même schéma de construction [(SN1) +SV1+SN2+SV2] avec elle et qui impliquent aussi une relation de dépendance entre deux prédicats, ce sont la construction à double complément, la construction à 2nd complément et la construction à contrôle objet. Nous tenterons de fournir quelques outils de distinction d’ordre lexical ou contextuel.Le chapitre 5 concerne les propriétés syntaxiques de la complétive objet. Nous discuterons d’abord du morphème ‘shuo’ à propos de son statut de ‘conjonction émergente’ et de quelques caractéristiques d’intégration sous le terme de « main clause phenomena ». Ensuite seront scrutés les verbes « recteurs faibles » dans les termes de Blanche-Benveniste (1988) qui s’avéreront assez similaires à leurs équivalents en français et en anglais. Enfin nous analyserons les références temporelles dans la construction complétive. Nous postulerons qu’elles se basent principalement sur la télicité des prédicats matrice et la sémantique de leurs arguments ; les marqueurs aspectuels –le, -guo et –zhe modifient cette interprétation par défaut selon leur sémantique propre. Et nous donnerons une analyse détaillée des contraintes de différents degrés imposées sur les différents types de prédicats. / Our thesis deals with the clausal object in Chinese and the predicats which select this type of complementation. In general we adopt the theoretical framework of the lexicon-grammar (Gross 1984) ; in concrete analysis, we adopte the analysis of the predicative structure (Muller 2001). It is divided into five chapters.In the first chaptre, we present the general conception of the clausal object as a type of propositional complement and we adopt the analysis of the dependence enunciative (Muller 1996). Then we present several articles which integrate the semantic aspect in the analysis of the clausal object.Chapter 2 aims to delimitate our object of study, which includes three subtypes: the propositional complement with that, the verbal complement without syntactic subject (the equivalent of the infinitive construction in French) and the embedded questions whose semantic specificity is taken into account.In the third chapter we study the other selectional properties of the prédicats compatible with that clause, firstly with regard to noun complement and verbal complement without syntactic subject, secondly with regard to that clause and the embedded questions. We also study the elements which can change the second type of selection.In Chapter 4 the completive object is placed in parallel with three other types of constructions that share the same construction scheme [(SN1) + SV1 + SV2 + SN2] with that clause and also imply a relationship of dependence between two predicates. They are : construction with double complement, construction with 2nd complement and construction of object control. We will try to provide some lexical or contextual parameters in order to distinguish them.In Chapter 5 we study the syntactic properties of the clausal object. We first discuss the morpheme 'shuo' about his status of 'emerging conjunction' and some characteristics of integration under the term of "main clause phenomena." Then are scrutinized the verbs of assertion under the name of ‘recteur faible’ (Blanche-Benveniste 1988) ; they are proved to be quite similar to their equivalents in French and English. Finally, we analyze the temporal references in the construction with clausal object. We postulate that it relies primarily on the telicity of matrix predicates and the semantics of their arguments ; the aspectual markers -le,-guo and –zhe can modify this interpretation by defaut according to their semantics. And we give a detailed analysis of constraints of different degrees imposed on different types of predicates.

Nous présentons une recherche en ingénierie des connaissances appliquée aux prédicats linguistiques et aux définitions lexicographiques de la théorie Sens-Texte (TST). Notre méthodologie comporte trois étapes. 1. Nous montrons en quoi la conceptualisation de la TST devrait être étendue pour faciliter sa formalisation. Nous justifions la nécessité de définir un niveau sémantique profond (SemP) à base de graphes. Nous y définissons la notion de type d'unité sémantique profonde et sa structure actancielle, de sorte que leur organisation hiérarchique puisse correspondre à une hiérarchie de sens au sein de laquelle ces structures actancielles sont héritées et spécialisées. Nous reconceptualisons les définitions lexicographiques au niveau SemP, et au niveau du dictionnaire. Finalement, nous présentons un prototype d'éditeur de définitions basé sur la manipulation directe de graphes. 2. Nous proposons un formalisme de représentation des connaissances adapté à cette conceptualisation. Nous démontrons que les logiques de description et le formalisme des Graphes Conceptuels ne sont pas adaptés, et nous construisons alors un nouveau formalisme, dit des Graphes d'Unités. 3. Nous étudions l'opérationnalisation du formalisme des Graphes d'Unités. Nous lui associons une sémantique formelle basée sur la théorie des modèles et l'algèbre relationnelle, et montrons que les conditions de décidabilité du raisonnement logique correspondent aux intuitions des lexicographes. Nous proposons également une implémentation du formalisme avec les standards du web sémantique, ce qui permet de profiter des architectures existantes pour l'interopérationnalisation sur le web des données lexicales liées. / We present our research in applying knowledge engineering to linguistic predicates and lexicographic definitions of the Meaning-Text Theory (MTT). We adopt a three-step methodology. 1. We first show how the MTT conceptualization should be extended to ease its formalization. We justify the need of defining a new graph-based deep semantic level. We define the notion of deep semantic unit types and its actantial structure, so that their hierarchical organization may correspond to a hierarchy of meanings, inside which actantial structures are inherited and specialized. We re-conceptualize lexicographic definitions at the deep semantic level, and at the level of dictionaries. Finally, we present a definition editor prototype based on graph direct manipulation, which will allow us, in future work, to integrate our formal model into explanatory combinatorial lexicographic projects. 2. We then propose a knowledge representation formalism (KR) adapted for this conceptualization. We demonstrate that Description Logics and the Conceptual Graphs formalism do not fit our needs. This leads us to construct a new knowledge representation formalism: the Unit Graphs formalism. 3. Finally, we operationalize the Unit Graphs formalism. We assign it a formal semantic model, which we create based on model theory and relational algebra. We then show that the reasoning decidability conditions match the intuitions that lexicographers have. We also provide an implementation using semantic web standards, which enable us to use existing architectures for sharing, interoperability, and knowledge querying over the web of lexical linked data.

Cette thèse est une investigation de la structure syntaxique et de l'interprétation modale des phrases impliquant le modal dénominal de nécessité behar ‘devoir, falloir, avoir besoin’ et un complément infinitif. La thèse analyse le statut syntaxique des compléments non finis du verbe modal denominal behar en examinant leur interaction avec des phénomènes syntaxiques sensibles à des conditions structurelles et de localité diverses, et conclut que les compléments d’infinitif de behar peuvent correspondre à différentes structures sous-jacentes. Le type d'infinitif le plus complexe du point de vue structurel est un infinitif non-restructurant qui projette une architecture de phrase complète (c.-à-d. une CP), et le plus petit est un infinitif réduit de restructuration qui projette une structure de phrase de niveau vP. Il y a des preuves pour l'existence des types intermédiaires projetant jusqu'au domaine flexionnel (IP / TP). D'autre part, la thèse examine les propriétés thématiques et de portée des sujets dans chacun des différents types structurels et l'interprétation modale à laquelle elles donnent cours. Sur la base de cette analyse, la thèse soutient que l'interprétation modale n'est déterminée par aucun facteur en particulier (la présence de la restructuration, le statut référentiel du sujet et sa portée relative vis-à-vis du prédicat modal, parmi d'autres fréquemment mentionnés), mais dépend de l'effet cumulatif de plusieurs facteurs travaillant ensemble. La thèse montre également la nécessité d'adopter une vision plus fine de la modalité radicale (root modality), qui permet une association plus simple entre structures syntaxiques et significations modales. / This dissertation is an investigation of the syntactic structure and modal interpretation of clauses involving the denominal necessity predicate behar ‘need’ and an infinitival complement. On the one hand, it analyses the syntactic status of non-finite complements of denominal behar by examining their interaction with syntactic phenomena sensitive to different structural and locality conditions, and concludes that the infinitival complements of behar can correspond to different underlying structures. The largest type of infinitive is a non-restructuring infinitive that projects a full clausal architecture (i.e. a CP), and the smallest one is a reduced restructuring infinitive that projects up to vP. There is evidence for intermediate types projecting up to the inflectional domain (IP/TP). On the other hand, the dissertation examines the thematic and scope properties of the subjects in each of the different structural types and the modal interpretation that they can give rise to. On the basis of this analysis it is argued that modal interpretation is not constrained by any single factor (the presence of restructuring, the referential status of the subject and its relative scope vis-à-vis the modal predicate, among other frequently mentioned ones), but depends on the cumulative effect of several factors working together. The dissertation also shows the necessity of adopting a more fine-grained view of root modality, one that allows a simpler mapping of syntactic structures into modal meanings.

Dans cette thèse nous proposons un modèle temporel dans le cadre des machines à états abstraits (ASM). Une extension du langage de spécification ASM est développé qui correspond à ce modéle temporel pour le temps continu. L'extension du langage avec des constructions de temps permet de diminuer la taille de la spécification et donc de réduire la probabilité d'erreurs. La sémantique de l'extension du langage ASM est fournie et prend en compte les définitions des fonctions externes, les valeurs des délais et les choix de résolution des non-déterminismes. Un sous-système de vérification des propriétés exprimées en logique FOTL (FirstOrder Timed Logic) est développé. Un simulateur d'ASMs temporisées est développé et implémenté, il comprend un analyseur syntaxique, un interprète du langage, un sous-système de vérification des propriétés ainsi qu'une interface graphique / In this thesis a temporal model for abstract state machines (ASM) method is pro- posed. An extension of ASM specification language on the base of the proposed temporal model with continuous time is developed. The language extension helps to reduce the size of the specification hence to diminish the probability of an error. The semantics of the extended ASM language is developed which takes into account the definitions of external functions, the values of time delays and the method of non-determinism resolving. A subsystem for verification of user properties in the FOTL language is developed. A simulator prototype for ASMs with time is developed and implemented. It includes the parser of the timed ASM language, the interpreter, the verification subsystem and the graphical user interface

Cette thèse analyse les propriétés sémantiques et discursives des prédicats d'état ('laid, généreux') ainsi que des prédicats causatifs et résultatifs, et plus particulièrement des verbes psychologiques à Expérienceur objet ('stimuler, encourager'). Le cadre adopté est celui de la sémantique néo-davidsonienne (Parsons, 1990) et de la sémantique du discours (Kamp & Reyle 1993, Asher 1993). La première partie (chap 1-7) est consacrée aux prédicats d'état, et la seconde aux prédicats causatifs et résultatifs (chap. 8-9). Dans le chapitre 1, on expose les arguments en faveur de l'idée que les verbes d'état ont un argument implicite davidsonien comme les verbes d'action. Abordant ensuite les constructions en 'by/in' ('by/in smoking, he broke his promise'), l'auteur propose de considérer, avec Goldman et contre Davidson, que celles-ci décrivent deux événements distincts, liés par une relation de génération. L'analyse goldmanienne de ces constructions est ensuite étendue aux prédicats d'état ('in doing this, he was clever'), ce qui permet de distinguer les prédicats qui dénotent un état dépendant d'une action, comme 'clever' en usage occurrentiel, des prédicats qui dénotent un état indépendant d'une action, comme beautiful (cf. '??in doing this, he was beautiful'). Le chapitre 2 fait le point sur les spécificités des prédicats d'état par rapport aux prédicats d'activité. Y est notamment montré que certains prédicats d'état acceptent le "progressif interprétatif" ('tu es en train de croire au Père Noël!'). Ce type de progressif est distingué du progressif standard et du progressif actif anglais ('he was being clever'); sont définis également les "prédicats interprétatifs" qui n'acceptent que ce progressif. Le chapitre 3 élabore une typologie aspectuelle des prédicats d'état. Sont d'abord distingués quatre types d'états en fonction de l'intervalle pendant lequel l'état en cause est vérifié. On montre que cette quadri-partition rend mieux compte des données linguistiques que la dichotomie classique en 'stage level predicates' et 'individual level predicates'. Ensuite sont définis les "prédicats d'état pur" comme beau, qui dénotent un état indépendant de toute action, et les "prédicats d'état endo-actionnel" comme 'généreux/bruyant' en usage occurrentiel, qui dénote un état généré par une action. On présente des arguments contre l'assimilation de ces derniers prédicats à des prédicats d'action. Est alors analysée l'ambiguïté des prédicats comme "généreux" dans l'emploi occurrentiel: 'Pierre m'a donné des bonbons. Il a été généreux' peut vouloir dire soit que Pierre a été généreux de (décider de) me donner des bonbons (lecture-d), soit qu'il a été généreux dans la manière de me les donner (lecture-m). Dans la foulée, on examine la relation temporelle qui prend place entre un état s et l'action e dont il dépend. Enfin, on montre que l'analyse proposée peut rendre compte de la concurrence entre passé composé et imparfait dans les phrases dénotant un état occurrentiel. A partir de la typologie aspectuelle élaborée au chapitre 3, le chapitre 4 revisite le problème que soulèvent certains prédicats d'état dans les constructions à prédicat second descriptif ('Pierre a donné des bonbons saoul/??généreux') et propose une nouvelle solution. On montre ensuite que cette solution peut être adaptée pour résoudre un problème moins étudié, à savoir celui que posent certains prédicats d'état dans les subordonnées temporelles en 'quand '(cf. 'Il était généreux, quand il a distribué les bonbons' versus '??Il a distribué des bonbons quand il était généreux'). Enfin, on fait le point sur la difficulté qu'éprouvent les prédicats évaluatifs à entrer dans les constructions présuppositionnelles, parmi lesquelles les subordonnées temporelles, mais les GN définis ('La femme rousse/??généreuse commanda une bière'). Le chapitre 5 est consacré aux relations rhétoriques qui s'établissent entre la description d'un état et la description d'un événement, aux combinaisons possibles entre ces relations rhétoriques, et à la manière dont tel ou tel prédicat d'état, vu ses propriétés sémantiques, contribue à établir telle ou telle relation rhétorique avec la description d'événement. Le chapitre 6 revient sur le problème que soulève l'indéfini des en lecture non générique avec certains prédicats d'état, notamment les prédicats évaluatifs ('Des livres étaient sales' versus '??Des livres étaient merveilleux'). En se fondant sur les outils de la 'Decision Theoretic Semantic's (Merin 1999), l'auteur fait l'hypothèse qu'un prédicat P n'accepte des que si la quantité des éléments satisfaisant P dans le contexte est non pertinente pour les fins du discours, et s'il est clair, par ailleurs, que les qualités implicites que peuvent instancier les dits éléments ne contribuent en aucune façon à expliquer qu'ils satisfont P. On montre que ces deux conditions sont respectées (resp. violées) avec les prédicats d'état compatibles (resp. incompatibles) avec des dans sa lecture non générique. Le chapitre 7 est consacré à la sémantique qu'il faut assigner aux prédicats d'état évaluatifs. On expose tout d'abord les arguments en faveur d'une sémantique "réaliste", qui analyse les prédicats évaluatifs comme des prédicats unaires dénotant de vraies propriétés. On distingue ensuite, dans le contenu informationnel des énoncés évaluatifs, un composant assertif et deux implicatures associées. On termine par l'analyse des prédicats évaluatifs superlatifs ('merveilleux'); est argumentée l'idée que ces prédicats ont un composant expressif, en ce sens que le locuteur, en les utilisant, implicite qu'une entité satisfaisant le prédicat a déclenché en lui une émotion, vécue ou rejouée lors de l'énonciation. On montre en quoi ce composant expressif contribue à expliquer pourquoi de tels prédicats sont difficilement utilisables à l'impératif ou dans certains types de questions. Le chapitre 8 répertorie trois classes parmi les verbes, dits "résultatifs", qui présupposent l'occurrence d'un événement e causant ou générant l'événement asserté e'. On présente d'abord le problème que pose la définition de cette présupposition, puis une nouvelle solution est exposée. On montre alors que la présupposition des verbes résultatifs -- achèvements droits et accomplissements strictement forts --- est de nature scalaire et peut s'expliquer par la Loi d'exhaustivité de Ducrot. Le chapitre 9 est consacré aux verbes psychologiques à Expérienceur objet (VPEO). Après avoir classé ces verbes en fonction de leur structure événementielle, on fait le point sur les différentes lectures qu'ils peuvent accepter. On montre ensuite qu'à la différence des VPEO acceptables dans les constructions agentives, les VPEO qui y sont peu acceptables exhibent deux propriétés cruciales. D'abord, ils présupposent toujours, à l'instar des verbes étudiés dans le chapitre 8, l'occurrence de l'événement impliquant le sujet; ensuite, certains d'entre eux sont "interprétatifs", en ce sens que l'assertion du changement d'état psychologique ne s'avère pertinente pour les fins du discours que si l'interprétant connaît, par ailleurs, l'événement qui cause ce changement. Cela permet d'expliquer pourquoi les verbes en question ne peuvent faire avancer la narration comme le ferait un prédicat d'action normal, et pourquoi ils sont peu compatibles avec les adverbes de manière orientés sur l'agent, les pseudo-clivées ou les compléments de lieu. On termine par l'analyse aspectuelle de la classe des VPEO, en montrant qu'on y trouve des membres des cinq classes aspectuelles distinguées dans le chapitre précédent.

Les systèmes embarqués sont de plus en plus intégrés dans les applications temps réel actuelles. Ils sont généralement constitués de composants matériels et logiciels profondément Intégrés mais hétérogènes. Ces composants sont développés sous des contraintes très strictes. En conséquence, le travail des ingénieurs de conception est devenu plus difficile. Pour répondre aux normes de haute qualité dans les systèmes embarqués de nos jours et pour satisfaire aux besoins quotidiens de l'industrie, l'automatisation du processus de développement de ces systèmes prend de plus en plus d'ampleur. Un défi majeur est de développer une approche automatisée qui peut être utilisée pour la vérification intégrée et la validation de systèmes complexes et hétérogènes.Dans le cadre de cette thèse, nous proposons une nouvelle approche compositionnelle pour la modélisation et la vérification des systèmes complexes décrits en langage SystemC. Cette approche est basée sur le modèle des SystemC Waiting State Automata (WSA). Les SystemC Waiting State Automata sont des automates permettant de modéliser le comportement abstrait des systèmes matériels et logiciels décrits en SystemC tout en préservant la sémantique de l'ordonnanceur SystemC au niveau des cycles temporels et au niveau des delta-cycles. Ce modèle permet de réduire la complexité de la modélisation des systèmes complexes due au problème de l'explosion combinatoire tout en restant fidèle au système initial. Ce modèle est compositionnel et supporte le rafinement. De plus, il est étendu par des paramètres temps ainsi que des compteurs afin de prendre en compte les aspects relatifs à la temporalité et aux propriétés fonctionnelles comme notamment la qualité de service. Nous proposons ensuite une chaîne de construction automatique des WSAs à partir de la description SystemC. Cette construction repose sur l'exécution symbolique et l'abstraction des prédicats. Nous proposons un ensemble d'algorithmes de composition et de réduction de ces automates afin de pouvoir étudier, analyser et vérifier les comportements concurrents des systèmes décrits ainsi que les échanges de données entre les différents composants. Nous proposons enfin d'appliquer notre approche dans le cadre de la modélisation et la simulation des systèmes complexes. Ensuite l'expérimenter pour donner une estimation du pire temps d'exécution (worst-case execution time (WCET)) en utilisant le modèle du Timed SystemC WSA. Enfin, on définit l'application des techniques du model checking pour prouver la correction de l'analyse abstraite de notre approche. / Embedded systems are increasingly integrated into existing real-time applications. They are usually composed of deeply integrated but heterogeneous hardware and software components. These components are developed under strict constraints. Accordingly, the work of design engineers became more tricky and challenging. To meet the high quality standards in nowadays embedded systems and to satisfy the rising industrial demands, the automatization of the developing process of those systems is gaining more and more importance. A major challenge is to develop an automated approach that can be used for the integrated verification and validation of complex and heterogeneous HW/SW systems.In this thesis, we propose a new compositional approach to model and verify hardware and software written in SystemC language. This approach is based on the SystemC Waiting State Automata (WSA). The SystemC Waiting State Automata are used to model the abstract behavior of hardware or software systems described in SystemC. They preserve the semantics of the SystemC scheduler at the temporal and the delta-cycle level. This model allows to reduce the complexity of the modeling process of complex systems due to the problem of state explosion during modeling while remaining faithful to the original system. The SystemC waiting state automaton is also compositional and supports refinement. In addition, this model is extended with parameters such as time and counters in order to take into account further aspects like temporality and other extra-functional properties such as QoS.In this thesis, we propose a stepwise approach on how to automatically extract the SystemC WSAs from SystemC descriptions. This construction is based on symbolic execution together with predicate abstraction. We propose a set of algorithms to symbolically compose and reduce the SystemC WSAs in order to study, analyze and verify concurrent behavior of systems as well as the data exchange between various components. We then propose to use the SystemC WSA to model and simulate hardware and software systems, and to compute the worst cas execution time (WCET) using the Timed SystemC WSA. Finally, we define how to apply model checking techniques to prove the correctness of the abstract analysis.

Les systèmes embarqués sont de plus en plus intégrés dans les applications temps réel actuelles. Ils sont généralement constitués de composants matériels et logiciels profondément Intégrés mais hétérogènes. Ces composants sont développés sous des contraintes très strictes. En conséquence, le travail des ingénieurs de conception est devenu plus difficile. Pour répondre aux normes de haute qualité dans les systèmes embarqués de nos jours et pour satisfaire aux besoins quotidiens de l'industrie, l'automatisation du processus de développement de ces systèmes prend de plus en plus d'ampleur. Un défi majeur est de développer une approche automatisée qui peut être utilisée pour la vérification intégrée et la validation de systèmes complexes et hétérogènes.Dans le cadre de cette thèse, nous proposons une nouvelle approche compositionnelle pour la modélisation et la vérification des systèmes complexes décrits en langage SystemC. Cette approche est basée sur le modèle des SystemC Waiting State Automata (WSA). Les SystemC Waiting State Automata sont des automates permettant de modéliser le comportement abstrait des systèmes matériels et logiciels décrits en SystemC tout en préservant la sémantique de l'ordonnanceur SystemC au niveau des cycles temporels et au niveau des delta-cycles. Ce modèle permet de réduire la complexité de la modélisation des systèmes complexes due au problème de l'explosion combinatoire tout en restant fidèle au système initial. Ce modèle est compositionnel et supporte le rafinement. De plus, il est étendu par des paramètres temps ainsi que des compteurs afin de prendre en compte les aspects relatifs à la temporalité et aux propriétés fonctionnelles comme notamment la qualité de service. Nous proposons ensuite une chaîne de construction automatique des WSAs à partir de la description SystemC. Cette construction repose sur l'exécution symbolique et l'abstraction des prédicats. Nous proposons un ensemble d'algorithmes de composition et de réduction de ces automates afin de pouvoir étudier, analyser et vérifier les comportements concurrents des systèmes décrits ainsi que les échanges de données entre les différents composants. Nous proposons enfin d'appliquer notre approche dans le cadre de la modélisation et la simulation des systèmes complexes. Ensuite l'expérimenter pour donner une estimation du pire temps d'exécution (worst-case execution time (WCET)) en utilisant le modèle du Timed SystemC WSA. Enfin, on définit l'application des techniques du model checking pour prouver la correction de l'analyse abstraite de notre approche. / Embedded systems are increasingly integrated into existing real-time applications. They are usually composed of deeply integrated but heterogeneous hardware and software components. These components are developed under strict constraints. Accordingly, the work of design engineers became more tricky and challenging. To meet the high quality standards in nowadays embedded systems and to satisfy the rising industrial demands, the automatization of the developing process of those systems is gaining more and more importance. A major challenge is to develop an automated approach that can be used for the integrated verification and validation of complex and heterogeneous HW/SW systems.In this thesis, we propose a new compositional approach to model and verify hardware and software written in SystemC language. This approach is based on the SystemC Waiting State Automata (WSA). The SystemC Waiting State Automata are used to model the abstract behavior of hardware or software systems described in SystemC. They preserve the semantics of the SystemC scheduler at the temporal and the delta-cycle level. This model allows to reduce the complexity of the modeling process of complex systems due to the problem of state explosion during modeling while remaining faithful to the original system. The SystemC waiting state automaton is also compositional and supports refinement. In addition, this model is extended with parameters such as time and counters in order to take into account further aspects like temporality and other extra-functional properties such as QoS.In this thesis, we propose a stepwise approach on how to automatically extract the SystemC WSAs from SystemC descriptions. This construction is based on symbolic execution together with predicate abstraction. We propose a set of algorithms to symbolically compose and reduce the SystemC WSAs in order to study, analyze and verify concurrent behavior of systems as well as the data exchange between various components. We then propose to use the SystemC WSA to model and simulate hardware and software systems, and to compute the worst cas execution time (WCET) using the Timed SystemC WSA. Finally, we define how to apply model checking techniques to prove the correctness of the abstract analysis.

Nous développons une méthode de modélisation et de validation adaptée aux système parallèles structurés en couches hiérarchiques. Nous définissons deux notions : la concordance de modèle prouve que le modèle possède bien les propriétés dégagées par les spécifications; l'adéquation de service valide le protocole par rapport à son service. Nous appliquons notre méthode à la modélisation du protocole de télécommunication de niveau Transport (la couche 4 d'après la norme ISO sur l'interconnexion des systèmes ouverts). Nous étudions tout particulièrement la gestion de désynchronisations du Service de la couche Réseau, et le contrôle de flux avec réquisition de crédit du protocole de la couche Transport. Nous utilisons les réseaux de Petri à prédicats pour décrire le modèle du service rendu par le couche Réseau sous-jacente et nous en servir pour construire le modèle du protocole de ma couche Transport. nous prouvons que la notion d'abstraction peut s'étendre aux réseaux de Petri à prédicats. La preuve du déroulement correct du protocole est apportée en utilisant les invariants issus du modèle.