Gestion Du Temps Par Le Raffinement

Dans les domaines critiques d'application de l'informatique, il peut tre vital de disposer d'un gnie logiciel qui soit capable de garantir le bon fonctionnement des systmes produits. Dans ce contexte particulier, la mthode "B vnementielle" promeut le dveloppement de modles abstraits du systme concevoir et l'utilisation de dmonstrations formelles ainsi que de la relation de raffinement entre les modles. Notre but est de pouvoir travailler sur des systmes 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 mthode B et de systmatiser cette approche par la formalisation de patrons de raffinement. Nos diffrentes modlisations du temps sont proposes sous la forme de patron r-appliquer sur le systme tudier.