Verification is now a well-known branch in computer science. It is crucial when dealing with computer programs in automatic systems: we want to check if a given system is correct and satisfies some specifications that should be met. One way to analyse those systems is to model them mathematically. The question is then: can we check if the model satisfies the required specifications ? This is called the model-checking problem. Several models have been studied in the literature. We have an interest for models that can mix both timing and randomized aspects. In this thesis we thus study the stochastic timed automaton model (STA). The contributions of this document are twofold. First, we study the qualitative and quantitative model-checking problems of STA. STA are, in particular, general probabilistic systems and with such model, one is thus interested in questions like « Is a property satisfied, within a given model, with probability 1 ? » (qualitative) or « Can we compute an approximation of the probability that the model satisfies a given property ? » (quantitative).We study those questions for general stochastic systems using, amongst other, the notion of decisiveness used in infinite Markov chains in order to get strong qualitative and quantitative results, and that we extend here in or more general context. We prove several results for the qualitative and quantitative model-checking problems of those probabilistic systems, some of them being extensions of previous work on Markov chains, others being new, and we show how it can be applied to subclasses of STA. Then we study the compositional verification in STA. In general, a system is the result of several smaller systems working together. Compositional verification allows then one to reduce the analysis of a big system to the analyses of the smaller systems which compose it. It is then crucial to have a good compositional framework in mathematical models, and this lacks in STA. In this thesis, we define an operator of composition for STA. We first make the assumption that the STA composed run completely independently from each other, i.e. they do not communicate between them. We prove that our definition satisfies indeed this independence assumption. Such an operator of composition is not very interesting as in general, systems do communicate. But it is a necessary first step. We then introduce the new model of interactive STA (ISTA) that will allow for interactions between the systems. We define an operator of composition in ISTA that will make synchronisations possible between the systems and that is built on the previous composition in STA. We end this thesis with the identification of a subclass of ISTA in which all the qualitative and quantitative results provided in this thesis can be applied, and which thus comes with the nice compositional framework defined in the model.

La vĂ©rification est maintenant une branche très connue des sciences informatiques. Elle est cruciale lorsque l’on a affaire Ă  des programmes informatiques dans des systèmes automatiques : on veut vĂ©rifier si un système donnĂ© est correct et s’il satisfait des propriĂ©tĂ©s nĂ©cessaires Ă  son bon fonctionnement. Une façon d’analyser ces systèmes se fait par la modĂ©lisation mathĂ©matique. La question est alors : peut-on vĂ©rifier si le modèle satisfait les propriĂ©tĂ©s requises ? C’est ce que l’on appelle le problème du model-checking. Plusieurs modèles ont Ă©tĂ© Ă©tudiĂ©s dans la littĂ©rature. Nous portons notre intĂ©rĂŞt sur des modèles qui peuvent mĂŞler des aspects temporels et des aspects probabilistes. Dans cette thèse, nous Ă©tudions donc le modèle des automates temporisĂ©s et stochastiques (ATS). Les contributions de ce document sont divisĂ©es en deux parties. Tout d’abord, nous Ă©tudions les problèmes de model-checking qualitatifs et quantitatifs des ATS. Les ATS sont, en particulier, des systèmes probabilistes gĂ©nĂ©raux et avec de tels modèles, on est intĂ©ressĂ© par des questions du type : « Une propriĂ©tĂ© est-elle satisfaite, au sein d’un modèle donnĂ©, avec probabilitĂ© 1 ? » (qualitatif) ou bien « Peut-on calculer une approximation de la probabilitĂ© que le modèle satisfait une propriĂ©tĂ© donnĂ©e ? » (quantitatif).Nous Ă©tudions ces questions dans des systèmes probabilistes gĂ©nĂ©raux en utilisant, entre autres, la notion de decisiveness utilisĂ©e dans les chaĂ®nes de Markov infinie dans le but d’obtenir d’importants rĂ©sultats qualitatifs et que nous Ă©tendons ici dans notre contexte plus gĂ©nĂ©ral. Nous prouvons plusieurs rĂ©sultats pour les problèmes de model-checking qualitatifs et quantitatifs de ces systèmes probabilistes, certains d’entre eux Ă©tant des extensions de travaux antĂ©rieurs sur les chaĂ®nes de Markov, d’autres Ă©tant nouveaux, et nous montrons comment l’on peut appliquer ces rĂ©sultats sur des sous-classes des ATS. Nous Ă©tudions ensuite la vĂ©rification compositionnelle des ATS. En gĂ©nĂ©ral, un système est le rĂ©sultat de plusieurs plus petits systèmes fonctionnant ensemble. La vĂ©rification compositionnelle permet alors de rĂ©duire l’analyse de gros systèmes aux analyses des plus petits systèmes qui le composent. Il est donc crucial d’avoir une bonne structure compositionnelle au sein des modèles mathĂ©matiques, et cela manque aux ATS. Dans cette thèse, nous dĂ©finissons un opĂ©rateur de composition pour les ATS. Nous faisons d’abord l’hypothèse que les ATS composĂ©s fonctionnent complètement indĂ©pendamment l’un de l’autre, c’est-Ă -dire les ATS ne communiquent pas entre eux. Nous prouvons que notre dĂ©finition satisfait bien cette hypothèse d’indĂ©pendance. Un tel opĂ©rateur de composition n’est pas très intĂ©ressant puisque, gĂ©nĂ©ralement, les systèmes interagissent entre eux. Mais c’est une première Ă©tape nĂ©cessaire. Nous introduisons donc le nouveau modèle des ATS interactifs (ATSI) qui vont permettre des interactions entre les systèmes. Nous dĂ©finissons un opĂ©rateur de composition dans les ATSI qui va rendre possible des synchronisations entre les systèmes et qui est construit sur la prĂ©cĂ©dente composition dans les ATS. Nous finissons cette thèse par l’identification d’une sous-classe de ATSI dans laquelle tous les rĂ©sultats qualitatifs et quantitatifs fournis dans cette thèse peuvent ĂŞtre appliquĂ©s, et qui est donc accompagnĂ©e d’une bonne structure compositionnelle au sein du modèle.