Return to search

Gestion du temps par le raffinement

Dans les domaines critiques d'application de l'informatique, il peut être vital de disposer d'un génie logiciel qui soit capable de garantir le bon fonctionnement des systèmes produits. Dans ce contexte, la méthode B évènementielle promeut le développement de modèles abstraits du système à concevoir et l'utilisation de démonstrations formelles ainsi que de la relation de raffinement entre les modèles. Notre but est de pouvoir travailler sur des systèmes ayant des aspects temporels quantitatifs (propriétés et contraintes de temps) en restant au sein du cadre défini par la méthode B qui a déjà montré son efficacité par ailleurs, mais qui ne dispose pas de concepts spécifiques pour le temps. C'est ainsi que nous proposons l'introduction des contraintes de temps par le raffinement, ceci permet de respecter la philosophie de la méthode B et de systématiser cette approche par la formalisation de patrons de raffinement. Nos différentes modélisations du temps sont proposées sous la forme de patron à réappliquer sur le système à étudier. Nous pouvons donc étudier progressivement le système à partir d'une abstraction non-temporelle afin de le valider progressivement et de distribuer la difficulté de la preuve en plusieurs étapes. L'introduction des aspects temporels ne se fait que lorsque cela est nécessaire lors du processus de développement prouvé. Nous avons validé cette approche sur des études de cas réalistes en utilisant les outils logiciels de démonstration formelle de la méthode B.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00441312
Date10 December 2009
CreatorsRehm, Joris
PublisherUniversité Henri Poincaré - Nancy I
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0019 seconds