Spécification Modulaire et Analyse Compositionnelle de Systèmes Stochastiques

This thesis presents new contributions in the design and verification of systems mixing both non-deterministic and stochastic aspects. Our results can be divided into three main contributions. First, we generalize interface theories to the stochastic setting. We build upon the known formalism of Interval Markov Chains to develop Constraint Markov Chains, the first fully compositional specification theory for stochastic systems. Second, we extend the notion of assume-guarantee contracts and develop a contract-based theory for stochastic systems, proposing quantitative notions for satisfaction and refinement. Finally, we propose a methodology for the verification of complex systems. This methodology is based on a stochastic abstraction of the environment where two components are working, allowing to verify the components individually. Combined with statistical model checking, this methodology is successfully applied to the verification of an industrial case study.Cette thèse présente des contributions originales pour la conception et la vérification de systèmes non-déterministes et stochastiques. Nos résultats sont divisés selon trois lignes directrices. Premièrement, nous généralisons la théorie des interfaces au cas stochastique, en s'appuyant sur le formalisme classique des chaînes de Markov à intervalles pour construire la première théorie de spécification compositionnelle pour systèmes stochastiques : les chaînes de Markov à contraintes. Deuxièmement, nous étendons la notion de contrats hypothèse-garantie et développons une théorie compositionnelle à base de contrats pour systèmes stochastiques, pour laquelle nous proposons des notions quantitatives de raffinement et de satisfaction. Finalement, nous proposons une méthodologie pour la vérification de systèmes complexes, basée sur une abstraction stochastique. Cette méthodologie, combinée avec le model-checking statistique, est appliquée avec succès à un cas d'étude industriel