LOGIN TO YOUR ACCOUNT

Username
Password
Remember Me
Or use your Academic/Social account:

CREATE AN ACCOUNT

Or use your Academic/Social account:

Congratulations!

You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.

Important!

Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message

CREATE AN ACCOUNT

Name:
Username:
Password:
Verify Password:
E-mail:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Languages: French
Types: Article
Subjects: Simulation distribuée, Model checking probabiliste, Chaînes de Markov, Algorithme EM, Algèbre stochastique PEPA, 000
L'objectif défini dans cette thèse est d’utiliser les récentes techniques de model checking probabiliste afin de vérifier des contraintes de performances sur des architectures de simulations distribuées. L'aspect probabiliste de l'approche permet à la fois de réduire la complexité du modèle et d’exprimer des contraintes de performances plus souples. Dans cette thèse nous avons dans un premier temps tenté d’utiliser le model checking probabiliste afin de formuler et de vérifier de telles contraintes de performances. Nous avons utilisé le model checker PRISM et confronté les résultats obtenus avec des données réelles provenant de simulations distribuées. Ceci a permis de révéler une difficulté fondamentale de cette démarche : il est difficile de choisir les coefficients du modèle pour que les résultats obtenus par le model checker coïncident avec la réalité. En clair, le modèle doit être réaliste. Afin de surmonter cette difficulté nous avons d’abord utilisé des algorithmes d'approximation qui ont permis d’obtenir des modèles plus réalistes mais sans structure, les rendant difficilement compréhensibles et manipulables. Afin de remédier à ce problème nous avons adapté un de ces algorithmes d’approximation, permettant d’induire des distributions de type phase à partir d’un ensemble de temps d’absorption, pour lui permettre d’opérer sur des modèles décrit dans l’algébre PEPA, un langage de modélisation basé sur une approche compositionnelle. L'algorithme a ensuite été étendu afin de fonctionner avec des exécutions partiellement observables au lieu de temps d’absorption, permettant ainsi de travailler sur des modèles PEPA sans état absorbant. Les expérimentations s’appuient sur le logiciel EMPEPA, distribué librement en Open-source, développé dans le cadre des travaux de thèse, et implantant en particulier ces deux algorithmes. The goal defined in this thesis is to use the recent techniques of probabilistic model checking in order to check performances constraints over distributed simulation architecture. The probabilistic aspect of this approach allows both to reduce the complexity of the model and to express finer performance constraints. In this thesis We firstly attempt to use probabilistic model checking to formalize and verify such a constraints. The probabilistic model checker PRISM has been used and its results have been compared to real data coming from distributed simulations. This permitted to reveal a fundamental difiiculty of this approach : it is difficult to choose the coefficients of the model so that the results obtained by the model checker coincide with reality. Clearly, the model has to be realistic. To overcome this difficulty we have firstly used fitting algorithms allowing to obtain more realistic model but without structure, making them hard to understand and to handle. To remedy this problem we have adapt one fitting algorithm, permitting to induce phase type distributions according to absorption times, to make it operate on PEPA, a modeling language based on a compositional approach. Secondly, the algorithm has been extended to operate with partially observable executions instead of absorption times, allowing to work on non-absorbing PEPA model. Experimentation has been driven using the tool EMPEPA, an Open-source program, developed in the context of the thesis work, and implementing these two algorithms.
  • No references.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article