Gestion du temps par le raffinement

Dans les domaines critiques d''application de l''informatique, il peut etre vital de disposer d''un genie logiciel qui soit capable de garantir le bon fonctionnement des systemes produits. Dans ce contexte particulier, la methode "B evenementielle" promeut le developpement de modeles abstraits du systeme a concevoir et l''utilisation de demonstrations formelles ainsi que de la relation de raffinement entre les modeles. Notre but est de pouvoir travailler sur des systemes ayant des aspects temporels quantitatifs. C''est ainsi que nous proposons l''introduction des contraintes de temps par le raffinement, ceci permet de respecter la philosophie de la methode B et de systematiser cette approche par la formalisation de patrons de raffinement. Nos differentes modelisations du temps sont proposees sous la forme de patron a re-appliquer sur le systeme a etudier.