Université de Rennes 1 Rare event simulation for statistical model checking Simulation d'événements rares pour le model checking statistique Ingénierie des systèmesVérification formelleModel Checking statistiqueMéthodes de Monte-CarloSimulation d'événements rareséchantillonnage statistiqueMéthodes de Monte-Carlo multi-niveaux System EngineeringFormal VerificationStatistical Model CheckingMonte-Carlo methodsRare Event SimulationImportant SamplingImportant Splitting Ingénierie des systèmes Thèses et écrits académiques Monte-Carlo, Méthode de Thèses et écrits académiques Échantillonnage (statistique) Thèses et écrits académiques Dans cette thèse, nous considérons deux problèmes auxquels le model checking statistique doit faire face. Le premier concerne les systèmes hétérogènes qui introduisent complexité et non-déterminisme dans l'analyse. Le second problème est celui des propriétés rares, difficiles à observer et donc à quantifier. Pour le premier point, nous présentons des contributions originales pour le formalisme des systèmes composites dans le langage BIP. Nous en proposons une extension stochastique, SBIP, qui permet le recours à l'abstraction stochastique de composants et d'éliminer le non-déterminisme. Ce double effet a pour avantage de réduire la taille du système initial en le remplaçant par un système dont la sémantique est purement stochastique sur lequel les algorithmes de model checking statistique sont définis. La deuxième partie de cette thèse est consacrée à la vérification de propriétés rares. Nous avons proposé le recours à un algorithme original d'échantillonnage préférentiel pour les modèles dont le comportement est décrit à travers un ensemble de commandes. Nous avons également introduit les méthodes multi-niveaux pour la vérification de propriétés rares et nous avons justifié et mis en place l'utilisation d'un algorithme multi-niveau optimal. Ces deux méthodes poursuivent le même objectif de réduire la variance de l'estimateur et le nombre de simulations. Néanmoins, elles sont fondamentalement différentes, la première attaquant le problème au travers du modèle et la seconde au travers des propriétés. In this thesis, we consider two problems that statistical model checking must cope. The first problem concerns heterogeneous systems, that naturally introduce complexity and non-determinism into the analysis. The second problem concerns rare properties, difficult to observe, and so to quantify. About the first point, we present original contributions for the formalism of composite systems in BIP language. We propose SBIP, a stochastic extension and define its semantics. SBIP allows the recourse to the stochastic abstraction of components and eliminate the non-determinism. This double effect has the advantage of reducing the size of the initial system by replacing it by a system whose semantics is purely stochastic, a necessary requirement for standard statistical model checking algorithms to be applicable. The second part of this thesis is devoted to the verification of rare properties in statistical model checking. We present a state-of-the-art algorithm for models described by a set of guarded commands. Lastly, we motivate the use of importance splitting for statistical model checking and set up an optimal splitting algorithm. Both methods pursue a common goal to reduce the variance of the estimator and the number of simulations. Nevertheless, they are fundamentally different, the first tackling the problem through the model and the second through the properties. Electronic Thesis or DissertationText en application/pdf1 : 2187 Kohttps://ecm.univ-rennes1.fr/nuxeo/site/esupversions/b47d2091-5cf7-4ce9-9eb4-8ae96cc122a8 Jegourel Cyrille 1984-10-22 FR 183874005 jegourelcyrille@yahoo.fr 2014REN1S084 http://www.theses.fr/2014REN1S084 2014-11-19 Informatique Université de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiLegayAxelintervenant_1183874129 Mathématiques, informatique, signal, électronique et télécommunicationsecoleDoctorale_1 139007164 IRISApartenaireRecherche_1 026386909 Université européenne de BretagnepartenaireRecherche_2 139075119 ddc:004 LegayAxelUniversité de Rennes 1Sciences et technologie, médecine, pharmacie, odontologie, droit, économie, gestion, philosophieMathématiques, informatique, signal, électronique et télécommunicationsÉcole doctorale Mathématiques, informatique, signal, électronique et télécommunications (Rennes)IRISAUniversité européenne de Bretagne ASCII PDF 2239251