Return to search

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

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.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00591609
Date08 October 2010
CreatorsDelahaye, Benoît
PublisherUniversité Rennes 1
Source SetsCCSD theses-EN-ligne, France
LanguageEnglish
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0018 seconds